big_op.v 30.7 KB
 Robbert Krebbers committed Oct 25, 2016 1 2 ``````From iris.algebra Require Export list cmra_big_op. From iris.base_logic Require Export base_logic. `````` Robbert Krebbers committed Nov 19, 2016 3 ``````From iris.prelude Require Import gmap fin_collections gmultiset functions. `````` Ralf Jung committed Jan 03, 2017 4 ``````Set Default Proof Using "Type*". `````` Ralf Jung committed Feb 17, 2016 5 ``````Import uPred. `````` Robbert Krebbers committed Feb 14, 2016 6 `````` `````` Robbert Krebbers committed Oct 25, 2016 7 8 9 10 11 ``````(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc) CMRA structure on uPred. *) Section cmra. Context {M : ucmraT}. `````` 12 13 `````` Instance uPred_valid_inst : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x. Instance uPred_validN_inst : ValidN (uPred M) := λ n P, `````` Robbert Krebbers committed Oct 25, 2016 14 15 16 17 `````` ∀ n' x, n' ≤ n → ✓{n'} x → P n' x. Instance uPred_op : Op (uPred M) := uPred_sep. Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I. `````` 18 `````` Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n). `````` Robbert Krebbers committed Oct 25, 2016 19 20 21 22 23 24 25 26 `````` Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed. Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I. Proof. unseal=> HP; split=> n' x ??; split; [done|]. intros _. by apply HP. Qed. `````` Robbert Krebbers committed Nov 03, 2016 27 `````` Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ∗ Q)%I → ✓{n} P. `````` Robbert Krebbers committed Oct 25, 2016 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 `````` Proof. unseal. intros HPQ n' x ??. destruct (HPQ n' x) as (x1&x2&->&?&?); auto. eapply uPred_mono with x1; eauto using cmra_includedN_l. Qed. Lemma uPred_included P Q : P ≼ Q → Q ⊢ P. Proof. intros [P' ->]. apply sep_elim_l. Qed. Definition uPred_cmra_mixin : CMRAMixin (uPred M). Proof. apply cmra_total_mixin; try apply _ || by eauto. - intros n P Q ??. by cofe_subst. - intros P; split. + intros HP n n' x ?. apply HP. + intros HP n x. by apply (HP n). - intros n P HP n' x ?. apply HP; auto. - intros P. by rewrite left_id. - intros P Q _. exists True%I. by rewrite left_id. - intros n P Q. apply uPred_cmra_validN_op_l. - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!. + by rewrite left_id. + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt. + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->. by rewrite left_id. Qed. Canonical Structure uPredR := `````` Ralf Jung committed Nov 22, 2016 56 `````` CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 57 58 59 60 61 62 63 64 65 66 67 `````` Instance uPred_empty : Empty (uPred M) := True%I. Definition uPred_ucmra_mixin : UCMRAMixin (uPred M). Proof. split; last done. - by rewrite /empty /uPred_empty uPred_pure_eq. - intros P. by rewrite left_id. Qed. Canonical Structure uPredUR := `````` Ralf Jung committed Nov 22, 2016 68 `````` UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 69 70 71 72 73 74 75 76 `````` Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always. Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed. Global Instance uPred_always_if_homomorphism b : UCMRAHomomorphism (uPred_always_if b). Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed. Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later. Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed. `````` Robbert Krebbers committed Nov 27, 2016 77 78 `````` Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n). Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed. `````` Robbert Krebbers committed Oct 25, 2016 79 80 81 82 83 84 85 86 87 88 89 `````` Global Instance uPred_except_0_homomorphism : CMRAHomomorphism uPred_except_0. Proof. split. apply _. apply except_0_sep. Qed. Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM. Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed. End cmra. Arguments uPredR : clear implicits. Arguments uPredUR : clear implicits. (* Notations *) `````` Robbert Krebbers committed Nov 03, 2016 90 ``````Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Sep 28, 2016 91 `````` `````` Robbert Krebbers committed Nov 03, 2016 92 ``````Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P)) `````` Robbert Krebbers committed Aug 24, 2016 93 `````` (at level 200, l at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 94 95 `````` format "[∗ list ] k ↦ x ∈ l , P") : uPred_scope. Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P)) `````` Robbert Krebbers committed Aug 24, 2016 96 `````` (at level 200, l at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 97 `````` format "[∗ list ] x ∈ l , P") : uPred_scope. `````` Robbert Krebbers committed Aug 24, 2016 98 `````` `````` Robbert Krebbers committed Nov 03, 2016 99 ``````Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P)) `````` Robbert Krebbers committed May 24, 2016 100 `````` (at level 200, m at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 101 102 `````` format "[∗ map ] k ↦ x ∈ m , P") : uPred_scope. Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P)) `````` Robbert Krebbers committed Sep 28, 2016 103 `````` (at level 200, m at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 104 `````` format "[∗ map ] x ∈ m , P") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 105 `````` `````` Robbert Krebbers committed Nov 03, 2016 106 ``````Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P)) `````` Robbert Krebbers committed May 24, 2016 107 `````` (at level 200, X at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 108 `````` format "[∗ set ] x ∈ X , P") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 109 `````` `````` Robbert Krebbers committed Nov 19, 2016 110 111 112 113 ``````Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P)) (at level 200, X at level 10, x at level 1, right associativity, format "[∗ mset ] x ∈ X , P") : uPred_scope. `````` Robbert Krebbers committed Aug 24, 2016 114 ``````(** * Persistence and timelessness of lists of uPreds *) `````` Robbert Krebbers committed Mar 11, 2016 115 ``````Class PersistentL {M} (Ps : list (uPred M)) := `````` Robbert Krebbers committed Mar 15, 2016 116 `````` persistentL : Forall PersistentP Ps. `````` Robbert Krebbers committed Mar 11, 2016 117 ``````Arguments persistentL {_} _ {_}. `````` Robbert Krebbers committed Feb 14, 2016 118 `````` `````` Robbert Krebbers committed Aug 24, 2016 119 120 121 122 ``````Class TimelessL {M} (Ps : list (uPred M)) := timelessL : Forall TimelessP Ps. Arguments timelessL {_} _ {_}. `````` Robbert Krebbers committed Apr 08, 2016 123 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 124 ``````Section big_op. `````` Robbert Krebbers committed May 27, 2016 125 ``````Context {M : ucmraT}. `````` Robbert Krebbers committed Feb 14, 2016 126 127 128 ``````Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Sep 28, 2016 129 130 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)). `````` Robbert Krebbers committed Feb 17, 2016 131 132 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Nov 03, 2016 133 ``````Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 134 ``````Proof. by rewrite big_op_app. Qed. `````` Robbert Krebbers committed Feb 17, 2016 135 `````` `````` Robbert Krebbers committed Nov 03, 2016 136 ``````Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [∗] Ps ⊢ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 137 ``````Proof. intros. apply uPred_included. by apply: big_op_contains. Qed. `````` Robbert Krebbers committed Nov 03, 2016 138 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. `````` Robbert Krebbers committed Sep 28, 2016 139 ``````Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. `````` Robbert Krebbers committed Nov 24, 2016 140 ``````Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps). `````` Robbert Krebbers committed Dec 06, 2016 141 ``````Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Feb 14, 2016 142 `````` `````` Robbert Krebbers committed Aug 24, 2016 143 ``````(** ** Persistence *) `````` Robbert Krebbers committed Nov 03, 2016 144 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 145 146 147 148 149 150 151 152 153 154 155 156 157 ``````Proof. induction 1; apply _. Qed. Global Instance nil_persistent : PersistentL (@nil (uPred M)). Proof. constructor. Qed. Global Instance cons_persistent P Ps : PersistentP P → PersistentL Ps → PersistentL (P :: Ps). Proof. by constructor. Qed. Global Instance app_persistent Ps Ps' : PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps'). Proof. apply Forall_app_2. Qed. Global Instance fmap_persistent {A} (f : A → uPred M) xs : (∀ x, PersistentP (f x)) → PersistentL (f <\$> xs). `````` Robbert Krebbers committed Aug 24, 2016 158 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 159 160 161 162 163 ``````Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys : (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys). Proof. unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 164 165 166 167 168 ``````Global Instance imap_persistent {A} (f : nat → A → uPred M) xs : (∀ i x, PersistentP (f i x)) → PersistentL (imap f xs). Proof. rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 169 170 `````` (** ** Timelessness *) `````` Robbert Krebbers committed Nov 03, 2016 171 ``````Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 172 173 174 175 176 177 178 179 180 181 182 183 184 ``````Proof. induction 1; apply _. Qed. Global Instance nil_timeless : TimelessL (@nil (uPred M)). Proof. constructor. Qed. Global Instance cons_timeless P Ps : TimelessP P → TimelessL Ps → TimelessL (P :: Ps). Proof. by constructor. Qed. Global Instance app_timeless Ps Ps' : TimelessL Ps → TimelessL Ps' → TimelessL (Ps ++ Ps'). Proof. apply Forall_app_2. Qed. Global Instance fmap_timeless {A} (f : A → uPred M) xs : (∀ x, TimelessP (f x)) → TimelessL (f <\$> xs). `````` Robbert Krebbers committed Aug 24, 2016 185 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 186 187 188 189 190 ``````Global Instance zip_with_timeless {A B} (f : A → B → uPred M) xs ys : (∀ x y, TimelessP (f x y)) → TimelessL (zip_with f xs ys). Proof. unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 191 192 193 194 195 196 197 198 199 200 201 202 ``````Global Instance imap_timeless {A} (f : nat → A → uPred M) xs : (∀ i x, TimelessP (f i x)) → TimelessL (imap f xs). Proof. rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto. Qed. (** ** Big ops over lists *) Section list. Context {A : Type}. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → uPred M. `````` Robbert Krebbers committed Nov 03, 2016 203 `````` Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 204 205 `````` Proof. done. Qed. Lemma big_sepL_cons Φ x l : `````` Robbert Krebbers committed Nov 03, 2016 206 `````` ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y. `````` Robbert Krebbers committed Sep 28, 2016 207 `````` Proof. by rewrite big_opL_cons. Qed. `````` Robbert Krebbers committed Nov 03, 2016 208 `````` Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. `````` Robbert Krebbers committed Sep 28, 2016 209 210 `````` Proof. by rewrite big_opL_singleton. Qed. Lemma big_sepL_app Φ l1 l2 : `````` Robbert Krebbers committed Nov 03, 2016 211 212 `````` ([∗ list] k↦y ∈ l1 ++ l2, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l1, Φ k y) ∗ ([∗ list] k↦y ∈ l2, Φ (length l1 + k) y). `````` Robbert Krebbers committed Sep 28, 2016 213 214 `````` Proof. by rewrite big_opL_app. Qed. `````` Robbert Krebbers committed Aug 24, 2016 215 216 `````` Lemma big_sepL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 217 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y. `````` Robbert Krebbers committed Sep 28, 2016 218 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 219 220 `````` Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 221 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y). `````` Robbert Krebbers committed Sep 28, 2016 222 `````` Proof. apply big_opL_proper. Qed. `````` Jacques-Henri Jourdan committed Dec 09, 2016 223 224 225 `````` Lemma big_sepL_contains (Φ : A → uPred M) l1 l2 : l1 `contains` l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y. Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed. `````` Robbert Krebbers committed Aug 24, 2016 226 227 228 `````` Global Instance big_sepL_mono' l : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 229 230 `````` (big_opL (M:=uPredUR M) l). Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Aug 24, 2016 231 `````` `````` Jacques-Henri Jourdan committed Dec 05, 2016 232 233 234 235 `````` Lemma big_sepL_lookup_acc Φ l i x : l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)). Proof. `````` Robbert Krebbers committed Dec 06, 2016 236 237 `````` intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i). by rewrite list_lookup_imap Hli. `````` Jacques-Henri Jourdan committed Dec 05, 2016 238 239 `````` Qed. `````` Robbert Krebbers committed Aug 24, 2016 240 `````` Lemma big_sepL_lookup Φ l i x : `````` Robbert Krebbers committed Nov 03, 2016 241 `````` l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 242 `````` Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed. `````` Robbert Krebbers committed Aug 24, 2016 243 `````` `````` Robbert Krebbers committed Aug 28, 2016 244 `````` Lemma big_sepL_elem_of (Φ : A → uPred M) l x : `````` Robbert Krebbers committed Nov 03, 2016 245 `````` x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 246 `````` Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed. `````` Robbert Krebbers committed Aug 28, 2016 247 `````` `````` Robbert Krebbers committed Aug 24, 2016 248 `````` Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l : `````` Robbert Krebbers committed Nov 03, 2016 249 `````` ([∗ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 250 `````` Proof. by rewrite big_opL_fmap. Qed. `````` Robbert Krebbers committed Aug 24, 2016 251 252 `````` Lemma big_sepL_sepL Φ Ψ l : `````` Robbert Krebbers committed Nov 03, 2016 253 254 `````` ([∗ list] k↦x ∈ l, Φ k x ∗ Ψ k x) ⊣⊢ ([∗ list] k↦x ∈ l, Φ k x) ∗ ([∗ list] k↦x ∈ l, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 255 `````` Proof. by rewrite big_opL_opL. Qed. `````` Robbert Krebbers committed Sep 28, 2016 256 `````` `````` Robbert Krebbers committed Nov 27, 2016 257 258 259 260 261 `````` Lemma big_sepL_and Φ Ψ l : ([∗ list] k↦x ∈ l, Φ k x ∧ Ψ k x) ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x). Proof. auto using big_sepL_mono with I. Qed. `````` Robbert Krebbers committed Sep 28, 2016 262 `````` Lemma big_sepL_later Φ l : `````` Robbert Krebbers committed Nov 03, 2016 263 `````` ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 264 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 265 `````` `````` Robbert Krebbers committed Nov 27, 2016 266 267 268 269 `````` Lemma big_sepL_laterN Φ n l : ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x). Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 270 `````` Lemma big_sepL_always Φ l : `````` Robbert Krebbers committed Nov 03, 2016 271 `````` (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 272 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 273 274 `````` Lemma big_sepL_always_if p Φ l : `````` Robbert Krebbers committed Nov 03, 2016 275 `````` □?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 276 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 277 278 279 `````` Lemma big_sepL_forall Φ l : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 280 `````` ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 281 282 283 284 285 286 287 `````` Proof. intros HΦ. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. } revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ. { rewrite big_sepL_nil; auto with I. } rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 288 `````` - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. `````` Robbert Krebbers committed Aug 24, 2016 289 290 291 292 `````` - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. Lemma big_sepL_impl Φ Ψ l : `````` Ralf Jung committed Nov 22, 2016 293 `````` □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 294 `````` ⊢ [∗ list] k↦x ∈ l, Ψ k x. `````` Robbert Krebbers committed Aug 24, 2016 295 296 297 298 299 300 301 `````` Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. setoid_rewrite always_impl; setoid_rewrite always_pure. rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Aug 28, 2016 302 `````` Global Instance big_sepL_nil_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 303 `````` PersistentP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 304 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 305 `````` Global Instance big_sepL_persistent Φ l : `````` Robbert Krebbers committed Nov 03, 2016 306 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 307 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 308 `````` Global Instance big_sepL_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 309 `````` TimelessP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 310 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 311 `````` Global Instance big_sepL_timeless Φ l : `````` Robbert Krebbers committed Nov 03, 2016 312 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 313 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 314 315 ``````End list. `````` Ralf Jung committed Dec 20, 2016 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 ``````Section list2. Context {A : Type}. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → uPred M. (* Some lemmas depend on the generalized versions of the above ones. *) Lemma big_sepL_zip_with {B C} Φ f (l1 : list B) (l2 : list C) : ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)). Proof. revert Φ l2; induction l1; intros Φ l2; first by rewrite /= big_sepL_nil. destruct l2; simpl. { rewrite big_sepL_nil. apply (anti_symm _); last exact: True_intro. (* TODO: Can this be done simpler? *) rewrite -(big_sepL_mono (λ _ _, True%I)). - rewrite big_sepL_forall. apply forall_intro=>k. apply forall_intro=>b. apply impl_intro_r. apply True_intro. - intros k b _. apply forall_intro=>c. apply impl_intro_l. rewrite right_id. apply pure_elim'. done. } rewrite !big_sepL_cons. apply sep_proper; last exact: IHl1. apply (anti_symm _). - apply forall_intro=>c'. simpl. apply impl_intro_r. eapply pure_elim; first exact: and_elim_r. intros [=->]. apply and_elim_l. - rewrite (forall_elim c). simpl. eapply impl_elim; first done. apply pure_intro. done. Qed. End list2. `````` Robbert Krebbers committed Aug 24, 2016 344 `````` `````` Robbert Krebbers committed Apr 08, 2016 345 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 346 347 348 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 349 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 350 `````` `````` Robbert Krebbers committed Feb 18, 2016 351 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 352 `````` m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 353 `````` ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x. `````` Robbert Krebbers committed Feb 16, 2016 354 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 355 `````` intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I. `````` Robbert Krebbers committed Sep 28, 2016 356 357 358 `````` - apply uPred_included. apply: big_op_contains. by apply fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 16, 2016 359 `````` Qed. `````` Robbert Krebbers committed Jul 22, 2016 360 361 `````` Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 362 `````` ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 363 `````` Proof. apply big_opM_proper. Qed. `````` Robbert Krebbers committed Feb 17, 2016 364 365 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 366 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 367 368 `````` (big_opM (M:=uPredUR M) m). Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Feb 17, 2016 369 `````` `````` Robbert Krebbers committed Nov 03, 2016 370 `````` Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 371 `````` Proof. by rewrite big_opM_empty. Qed. `````` Robbert Krebbers committed May 30, 2016 372 `````` `````` Robbert Krebbers committed May 31, 2016 373 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 374 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 375 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 376 `````` Proof. apply: big_opM_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 377 `````` `````` Robbert Krebbers committed May 31, 2016 378 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 379 `````` m !! i = Some x → `````` Robbert Krebbers committed Nov 03, 2016 380 `````` ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 381 `````` Proof. apply: big_opM_delete. Qed. `````` Robbert Krebbers committed May 30, 2016 382 `````` `````` Robbert Krebbers committed Nov 24, 2016 383 384 385 386 387 388 389 `````` Lemma big_sepM_lookup_acc Φ m i x : m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y)). Proof. intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed May 31, 2016 390 `````` Lemma big_sepM_lookup Φ m i x : `````` Robbert Krebbers committed Nov 03, 2016 391 `````` m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Nov 24, 2016 392 393 `````` Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. `````` Robbert Krebbers committed Nov 20, 2016 394 395 396 `````` Lemma big_sepM_lookup_dom (Φ : K → uPred M) m i : is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i. Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed. `````` Robbert Krebbers committed May 31, 2016 397 `````` `````` Robbert Krebbers committed Nov 03, 2016 398 `````` Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 399 `````` Proof. by rewrite big_opM_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 400 `````` `````` Robbert Krebbers committed May 31, 2016 401 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : `````` Robbert Krebbers committed Nov 03, 2016 402 `````` ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 403 `````` Proof. by rewrite big_opM_fmap. Qed. `````` Robbert Krebbers committed May 31, 2016 404 `````` `````` Robbert Krebbers committed Dec 02, 2016 405 406 407 `````` Lemma big_sepM_insert_override Φ m i x x' : m !! i = Some x → (Φ i x ⊣⊢ Φ i x') → ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k y). `````` Robbert Krebbers committed Sep 28, 2016 408 `````` Proof. apply: big_opM_insert_override. Qed. `````` Robbert Krebbers committed May 31, 2016 409 `````` `````` Robbert Krebbers committed Dec 02, 2016 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 `````` Lemma big_sepM_insert_override_1 Φ m i x x' : m !! i = Some x → ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y) ⊢ (Φ i x' -∗ Φ i x) -∗ ([∗ map] k↦y ∈ m, Φ k y). Proof. intros ?. apply wand_intro_l. rewrite -insert_delete big_sepM_insert ?lookup_delete //. by rewrite assoc wand_elim_l -big_sepM_delete. Qed. Lemma big_sepM_insert_override_2 Φ m i x x' : m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ (Φ i x -∗ Φ i x') -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y). Proof. intros ?. apply wand_intro_l. rewrite {1}big_sepM_delete //; rewrite assoc wand_elim_l. rewrite -insert_delete big_sepM_insert ?lookup_delete //. Qed. `````` Robbert Krebbers committed Jun 01, 2016 430 `````` Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : `````` Robbert Krebbers committed May 31, 2016 431 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 432 433 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k)) ⊣⊢ (Ψ i x b ∗ [∗ map] k↦y ∈ m, Ψ k y (f k)). `````` Robbert Krebbers committed Sep 28, 2016 434 435 `````` Proof. apply: big_opM_fn_insert. Qed. `````` Robbert Krebbers committed May 31, 2016 436 437 `````` Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 438 `````` ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). `````` Robbert Krebbers committed Sep 28, 2016 439 `````` Proof. apply: big_opM_fn_insert'. Qed. `````` Robbert Krebbers committed May 31, 2016 440 `````` `````` Robbert Krebbers committed Feb 18, 2016 441 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Nov 27, 2016 442 `````` ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) `````` Robbert Krebbers committed Nov 03, 2016 443 `````` ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 444 `````` Proof. apply: big_opM_opM. Qed. `````` Robbert Krebbers committed May 31, 2016 445 `````` `````` Robbert Krebbers committed Nov 27, 2016 446 447 448 449 450 `````` Lemma big_sepM_and Φ Ψ m : ([∗ map] k↦x ∈ m, Φ k x ∧ Ψ k x) ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x). Proof. auto using big_sepM_mono with I. Qed. `````` Robbert Krebbers committed Sep 28, 2016 451 `````` Lemma big_sepM_later Φ m : `````` Robbert Krebbers committed Nov 03, 2016 452 `````` ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 453 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 454 `````` `````` Robbert Krebbers committed Nov 27, 2016 455 456 457 458 `````` Lemma big_sepM_laterN Φ n m : ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x). Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 459 `````` Lemma big_sepM_always Φ m : `````` Robbert Krebbers committed Nov 03, 2016 460 `````` (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 461 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 462 463 `````` Lemma big_sepM_always_if p Φ m : `````` Robbert Krebbers committed Nov 03, 2016 464 `````` □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 465 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 466 467 468 `````` Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 469 `````` ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed May 31, 2016 470 471 472 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 473 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. } `````` Robbert Krebbers committed Sep 28, 2016 474 475 476 `````` induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|]. rewrite big_sepM_insert // -always_and_sep_l. apply and_intro. - rewrite (forall_elim i) (forall_elim x) lookup_insert. `````` Robbert Krebbers committed Nov 21, 2016 477 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 478 `````` - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. `````` Robbert Krebbers committed Sep 28, 2016 479 480 `````` apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. `````` Robbert Krebbers committed Nov 21, 2016 481 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 482 483 484 `````` Qed. Lemma big_sepM_impl Φ Ψ m : `````` Ralf Jung committed Nov 22, 2016 485 `````` □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 486 `````` ⊢ [∗ map] k↦x ∈ m, Ψ k x. `````` Robbert Krebbers committed May 31, 2016 487 488 `````` Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. `````` Robbert Krebbers committed Jun 24, 2016 489 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 490 491 492 `````` rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Aug 24, 2016 493 `````` `````` Robbert Krebbers committed Aug 28, 2016 494 `````` Global Instance big_sepM_empty_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 495 `````` PersistentP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 496 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 497 `````` Global Instance big_sepM_persistent Φ m : `````` Robbert Krebbers committed Nov 03, 2016 498 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 499 `````` Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed. `````` Robbert Krebbers committed Aug 28, 2016 500 `````` Global Instance big_sepM_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 501 `````` TimelessP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 502 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 503 `````` Global Instance big_sepM_timeless Φ m : `````` Robbert Krebbers committed Nov 03, 2016 504 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 505 `````` Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed. `````` Robbert Krebbers committed Feb 17, 2016 506 507 ``````End gmap. `````` Robbert Krebbers committed Aug 24, 2016 508 `````` `````` Robbert Krebbers committed Apr 08, 2016 509 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 510 511 512 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 513 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 514 `````` `````` Robbert Krebbers committed Feb 18, 2016 515 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 516 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 517 `````` ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x. `````` Robbert Krebbers committed Feb 17, 2016 518 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 519 `````` intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Sep 28, 2016 520 521 522 `````` - apply uPred_included. apply: big_op_contains. by apply fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 17, 2016 523 `````` Qed. `````` Robbert Krebbers committed Oct 03, 2016 524 525 `````` Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 526 `````` ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). `````` Robbert Krebbers committed Oct 03, 2016 527 `````` Proof. apply: big_opS_proper. Qed. `````` Robbert Krebbers committed Sep 28, 2016 528 `````` `````` Robbert Krebbers committed Oct 03, 2016 529 `````` Global Instance big_sepS_mono' X : `````` Robbert Krebbers committed Sep 28, 2016 530 531 532 `````` Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X). Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Nov 03, 2016 533 `````` Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 534 `````` Proof. by rewrite big_opS_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 535 `````` `````` Robbert Krebbers committed Feb 18, 2016 536 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 537 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 538 539 `````` Proof. apply: big_opS_insert. Qed. `````` Robbert Krebbers committed Jun 01, 2016 540 `````` Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : `````` Robbert Krebbers committed Apr 11, 2016 541 `````` x ∉ X → `````` Robbert Krebbers committed Nov 03, 2016 542 543 `````` ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). `````` Robbert Krebbers committed Sep 28, 2016 544 545 `````` Proof. apply: big_opS_fn_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 546 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed Nov 03, 2016 547 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 548 `````` Proof. apply: big_opS_fn_insert'. Qed. `````` Robbert Krebbers committed Apr 11, 2016 549 `````` `````` Robbert Krebbers committed Nov 21, 2016 550 551 552 553 554 `````` Lemma big_sepS_union Φ X Y : X ⊥ Y → ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y). Proof. apply: big_opS_union. Qed. `````` Robbert Krebbers committed Feb 18, 2016 555 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 556 `````` x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Sep 28, 2016 557 `````` Proof. apply: big_opS_delete. Qed. `````` Robbert Krebbers committed Apr 11, 2016 558 `````` `````` Robbert Krebbers committed Nov 03, 2016 559 `````` Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. `````` 560 `````` Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. `````` Robbert Krebbers committed May 31, 2016 561 `````` `````` Robbert Krebbers committed Nov 24, 2016 562 563 564 565 566 567 568 `````` Lemma big_sepS_elem_of_acc Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ set] y ∈ X, Φ y)). Proof. intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 569 `````` Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 570 `````` Proof. apply: big_opS_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 571 `````` `````` Robbert Krebbers committed Nov 21, 2016 572 `````` Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X : `````` Ralf Jung committed Nov 22, 2016 573 `````` ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y). `````` Robbert Krebbers committed Nov 21, 2016 574 575 576 577 578 579 580 581 582 583 584 `````` Proof. induction X as [|x X ? IH] using collection_ind_L. { by rewrite filter_empty_L !big_sepS_empty. } destruct (decide (P x)). - rewrite filter_union_L filter_singleton_L //. rewrite !big_sepS_insert //; last set_solver. by rewrite IH pure_True // left_id. - rewrite filter_union_L filter_singleton_not_L // left_id_L. by rewrite !big_sepS_insert // IH pure_False // False_impl left_id. Qed. `````` Robbert Krebbers committed Nov 29, 2016 585 586 587 588 589 590 591 592 593 594 595 `````` Lemma big_sepS_filter_acc (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y : (∀ y, y ∈ Y → P y → y ∈ X) → ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) ∗ (([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y). Proof. intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X)) as (Z&->&?); first set_solver. rewrite big_sepS_union // big_sepS_filter. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Feb 18, 2016 596 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Nov 03, 2016 597 `````` ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Sep 28, 2016 598 `````` Proof. apply: big_opS_opS. Qed. `````` Robbert Krebbers committed May 31, 2016 599 `````` `````` Robbert Krebbers committed Nov 27, 2016 600 601 602 603 `````` Lemma big_sepS_and Φ Ψ X : ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y). Proof. auto using big_sepS_mono with I. Qed. `````` Robbert Krebbers committed Nov 03, 2016 604 `````` Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 605 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 606 `````` `````` Robbert Krebbers committed Nov 27, 2016 607 608 609 610 `````` Lemma big_sepS_laterN Φ n X : ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y). Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Nov 03, 2016 611 `````` Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 612 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 613 `````` `````` Robbert Krebbers committed May 31, 2016 614 `````` Lemma big_sepS_always_if q Φ X : `````` Robbert Krebbers committed Nov 03, 2016 615 `````` □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y). `````` Robbert Krebbers committed Sep 28, 2016 616 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 617 618 `````` Lemma big_sepS_forall Φ X : `````` Ralf Jung committed Nov 22, 2016 619 `````` (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). `````` Robbert Krebbers committed May 31, 2016 620 621 622 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 623 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. } `````` Robbert Krebbers committed Nov 21, 2016 624 `````` induction X as [|x X ? IH] using collection_ind_L. `````` Robbert Krebbers committed Sep 28, 2016 625 626 `````` { rewrite big_sepS_empty; auto. } rewrite big_sepS_insert // -always_and_sep_l. apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 627 `````` - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed Sep 28, 2016 628 `````` - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. `````` Robbert Krebbers committed Nov 21, 2016 629 `````` by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 630 631 632 `````` Qed. Lemma big_sepS_impl Φ Ψ X : `````` Ralf Jung committed Nov 22, 2016 633 `````` □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 634 635 `````` Proof. rewrite always_and_sep_l always_forall. `````` Robbert Krebbers committed Jun 24, 2016 636 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 637 638 639 `````` rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Feb 14, 2016 640 `````` `````` Robbert Krebbers committed Nov 03, 2016 641 `````` Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 642 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 643 `````` Global Instance big_sepS_persistent Φ X : `````` Robbert Krebbers committed Nov 03, 2016 644 `````` (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 645 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Nov 03, 2016 646 `````` Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 647 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 648 `````` Global Instance big_sepS_timeless Φ X : `````` Robbert Krebbers committed Nov 03, 2016 649 `````` (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 650 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 651 ``````End gset. `````` Robbert Krebbers committed Nov 19, 2016 652 `````` `````` Robbert Krebbers committed Dec 02, 2016 653 654 655 656 ``````Lemma big_sepM_dom `{Countable K} {A} (Φ : K → uPred M) (m : gmap K A) : ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k). Proof. apply: big_opM_dom. Qed. `````` Robbert Krebbers committed Nov 19, 2016 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 `````` (** ** Big ops over finite multisets *) Section gmultiset. Context `{Countable A}. Implicit Types X : gmultiset A. Implicit Types Φ : A → uPred M. Lemma big_sepMS_mono Φ Ψ X Y : Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Ψ x. Proof. intros HX HΦ. trans ([∗ mset] x ∈ Y, Φ x)%I. - apply uPred_included. apply: big_op_contains. by apply fmap_contains, gmultiset_elements_contains. - apply big_opMS_forall; apply _ || auto. Qed. Lemma big_sepMS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x). Proof. apply: big_opMS_proper. Qed. Global Instance big_sepMS_mono' X : Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opMS (M:=uPredUR M) X). Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ True. Proof. by rewrite big_opMS_empty. Qed. Lemma big_sepMS_union Φ X Y : ([∗ mset] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ [∗ mset] y ∈ Y, Φ y. Proof. apply: big_opMS_union. Qed. Lemma big_sepMS_delete Φ X x : x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[ x ]}, Φ y. Proof. apply: big_opMS_delete. Qed. Lemma big_sepMS_elem_of Φ X x : x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x. Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. `````` Robbert Krebbers committed Nov 24, 2016 696 697 698 699 700 701 702 `````` Lemma big_sepMS_elem_of_acc Φ X x : x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ mset] y ∈ X, Φ y)). Proof. intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Nov 19, 2016 703 704 705 706 707 708 709 `````` Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. Proof. apply: big_opMS_singleton. Qed. Lemma big_sepMS_sepMS Φ Ψ X : ([∗ mset] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ ([∗ mset] y ∈ X, Ψ y). Proof. apply: big_opMS_opMS. Qed. `````` Robbert Krebbers committed Nov 27, 2016 710 711