big_op.v 29 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 Feb 17, 2016 4 ``````Import uPred. `````` Robbert Krebbers committed Feb 14, 2016 5 `````` `````` Robbert Krebbers committed Oct 25, 2016 6 7 8 9 10 ``````(* 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}. `````` 11 12 `````` 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 13 14 15 16 `````` ∀ 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. `````` 17 `````` Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n). `````` Robbert Krebbers committed Oct 25, 2016 18 19 20 21 22 23 24 25 `````` 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 26 `````` Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ∗ Q)%I → ✓{n} P. `````` Robbert Krebbers committed Oct 25, 2016 27 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 `````` 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 55 `````` CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 56 57 58 59 60 61 62 63 64 65 66 `````` 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 67 `````` UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 68 69 70 71 72 73 74 75 `````` 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 76 77 `````` 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 78 79 80 81 82 83 84 85 86 87 88 `````` 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 89 ``````Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Sep 28, 2016 90 `````` `````` Robbert Krebbers committed Nov 03, 2016 91 ``````Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P)) `````` Robbert Krebbers committed Aug 24, 2016 92 `````` (at level 200, l at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 93 94 `````` 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 95 `````` (at level 200, l at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 96 `````` format "[∗ list ] x ∈ l , P") : uPred_scope. `````` Robbert Krebbers committed Aug 24, 2016 97 `````` `````` Robbert Krebbers committed Nov 03, 2016 98 ``````Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P)) `````` Robbert Krebbers committed May 24, 2016 99 `````` (at level 200, m at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 100 101 `````` 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 102 `````` (at level 200, m at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 103 `````` format "[∗ map ] x ∈ m , P") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 104 `````` `````` Robbert Krebbers committed Nov 03, 2016 105 ``````Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P)) `````` Robbert Krebbers committed May 24, 2016 106 `````` (at level 200, X at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 107 `````` format "[∗ set ] x ∈ X , P") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 108 `````` `````` Robbert Krebbers committed Nov 19, 2016 109 110 111 112 ``````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 113 ``````(** * Persistence and timelessness of lists of uPreds *) `````` Robbert Krebbers committed Mar 11, 2016 114 ``````Class PersistentL {M} (Ps : list (uPred M)) := `````` Robbert Krebbers committed Mar 15, 2016 115 `````` persistentL : Forall PersistentP Ps. `````` Robbert Krebbers committed Mar 11, 2016 116 ``````Arguments persistentL {_} _ {_}. `````` Robbert Krebbers committed Feb 14, 2016 117 `````` `````` Robbert Krebbers committed Aug 24, 2016 118 119 120 121 ``````Class TimelessL {M} (Ps : list (uPred M)) := timelessL : Forall TimelessP Ps. Arguments timelessL {_} _ {_}. `````` Robbert Krebbers committed Apr 08, 2016 122 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 123 ``````Section big_op. `````` Robbert Krebbers committed May 27, 2016 124 ``````Context {M : ucmraT}. `````` Robbert Krebbers committed Feb 14, 2016 125 126 127 ``````Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Sep 28, 2016 128 129 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)). `````` Robbert Krebbers committed Feb 17, 2016 130 131 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Nov 03, 2016 132 ``````Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 133 ``````Proof. by rewrite big_op_app. Qed. `````` Robbert Krebbers committed Feb 17, 2016 134 `````` `````` Robbert Krebbers committed Nov 03, 2016 135 ``````Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [∗] Ps ⊢ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 136 ``````Proof. intros. apply uPred_included. by apply: big_op_contains. Qed. `````` Robbert Krebbers committed Nov 03, 2016 137 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. `````` Robbert Krebbers committed Sep 28, 2016 138 ``````Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. `````` Robbert Krebbers committed Nov 24, 2016 139 140 141 142 143 144 ``````Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps). Proof. intros (Ps1&Ps2&->)%elem_of_list_split. rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Feb 14, 2016 145 `````` `````` Robbert Krebbers committed Aug 24, 2016 146 ``````(** ** Persistence *) `````` Robbert Krebbers committed Nov 03, 2016 147 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 148 149 150 151 152 153 154 155 156 157 158 159 160 ``````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 161 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 162 163 164 165 166 ``````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 167 168 169 170 171 ``````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 172 173 `````` (** ** Timelessness *) `````` Robbert Krebbers committed Nov 03, 2016 174 ``````Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 175 176 177 178 179 180 181 182 183 184 185 186 187 ``````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 188 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 189 190 191 192 193 ``````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 194 195 196 197 198 199 200 201 202 203 204 205 ``````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 206 `````` Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 207 208 `````` Proof. done. Qed. Lemma big_sepL_cons Φ x l : `````` Robbert Krebbers committed Nov 03, 2016 209 `````` ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y. `````` Robbert Krebbers committed Sep 28, 2016 210 `````` Proof. by rewrite big_opL_cons. Qed. `````` Robbert Krebbers committed Nov 03, 2016 211 `````` Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. `````` Robbert Krebbers committed Sep 28, 2016 212 213 `````` Proof. by rewrite big_opL_singleton. Qed. Lemma big_sepL_app Φ l1 l2 : `````` Robbert Krebbers committed Nov 03, 2016 214 215 `````` ([∗ 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 216 217 `````` Proof. by rewrite big_opL_app. Qed. `````` Robbert Krebbers committed Aug 24, 2016 218 219 `````` Lemma big_sepL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 220 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y. `````` Robbert Krebbers committed Sep 28, 2016 221 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 222 223 `````` Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 224 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y). `````` Robbert Krebbers committed Sep 28, 2016 225 `````` Proof. apply big_opL_proper. 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 232 `````` Lemma big_sepL_lookup Φ l i x : `````` Robbert Krebbers committed Nov 03, 2016 233 `````` l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 234 `````` Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed. `````` Robbert Krebbers committed Aug 24, 2016 235 `````` `````` Robbert Krebbers committed Aug 28, 2016 236 `````` Lemma big_sepL_elem_of (Φ : A → uPred M) l x : `````` Robbert Krebbers committed Nov 03, 2016 237 `````` x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 238 `````` Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed. `````` Robbert Krebbers committed Aug 28, 2016 239 `````` `````` Robbert Krebbers committed Aug 24, 2016 240 `````` Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l : `````` Robbert Krebbers committed Nov 03, 2016 241 `````` ([∗ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 242 `````` Proof. by rewrite big_opL_fmap. Qed. `````` Robbert Krebbers committed Aug 24, 2016 243 244 `````` Lemma big_sepL_sepL Φ Ψ l : `````` Robbert Krebbers committed Nov 03, 2016 245 246 `````` ([∗ 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 247 `````` Proof. by rewrite big_opL_opL. Qed. `````` Robbert Krebbers committed Sep 28, 2016 248 `````` `````` Robbert Krebbers committed Nov 27, 2016 249 250 251 252 253 `````` 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 254 `````` Lemma big_sepL_later Φ l : `````` Robbert Krebbers committed Nov 03, 2016 255 `````` ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 256 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 257 `````` `````` Robbert Krebbers committed Nov 27, 2016 258 259 260 261 `````` 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 262 `````` Lemma big_sepL_always Φ 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 266 `````` Lemma big_sepL_always_if p Φ l : `````` Robbert Krebbers committed Nov 03, 2016 267 `````` □?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 268 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 269 270 271 `````` Lemma big_sepL_forall Φ l : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 272 `````` ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 273 274 275 276 277 278 279 `````` 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 280 `````` - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. `````` Robbert Krebbers committed Aug 24, 2016 281 282 283 284 `````` - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. Lemma big_sepL_impl Φ Ψ l : `````` Ralf Jung committed Nov 22, 2016 285 `````` □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 286 `````` ⊢ [∗ list] k↦x ∈ l, Ψ k x. `````` Robbert Krebbers committed Aug 24, 2016 287 288 289 290 291 292 293 `````` 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 294 `````` Global Instance big_sepL_nil_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 295 `````` PersistentP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 296 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 297 `````` Global Instance big_sepL_persistent Φ l : `````` Robbert Krebbers committed Nov 03, 2016 298 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 299 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 300 `````` Global Instance big_sepL_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 301 `````` TimelessP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 302 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 303 `````` Global Instance big_sepL_timeless Φ l : `````` Robbert Krebbers committed Nov 03, 2016 304 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 305 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 306 307 ``````End list. `````` Robbert Krebbers committed Aug 24, 2016 308 `````` `````` Robbert Krebbers committed Apr 08, 2016 309 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 310 311 312 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 313 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 314 `````` `````` Robbert Krebbers committed Feb 18, 2016 315 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 316 `````` m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 317 `````` ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x. `````` Robbert Krebbers committed Feb 16, 2016 318 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 319 `````` intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I. `````` Robbert Krebbers committed Sep 28, 2016 320 321 322 `````` - 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 323 `````` Qed. `````` Robbert Krebbers committed Jul 22, 2016 324 325 `````` Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 326 `````` ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 327 `````` Proof. apply big_opM_proper. Qed. `````` Robbert Krebbers committed Feb 17, 2016 328 329 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 330 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 331 332 `````` (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 333 `````` `````` Robbert Krebbers committed Nov 03, 2016 334 `````` Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 335 `````` Proof. by rewrite big_opM_empty. Qed. `````` Robbert Krebbers committed May 30, 2016 336 `````` `````` Robbert Krebbers committed May 31, 2016 337 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 338 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 339 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 340 `````` Proof. apply: big_opM_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 341 `````` `````` Robbert Krebbers committed May 31, 2016 342 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 343 `````` m !! i = Some x → `````` Robbert Krebbers committed Nov 03, 2016 344 `````` ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 345 `````` Proof. apply: big_opM_delete. Qed. `````` Robbert Krebbers committed May 30, 2016 346 `````` `````` Robbert Krebbers committed Nov 24, 2016 347 348 349 350 351 352 353 `````` 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 354 `````` Lemma big_sepM_lookup Φ m i x : `````` Robbert Krebbers committed Nov 03, 2016 355 `````` m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Nov 24, 2016 356 357 `````` Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. `````` Robbert Krebbers committed Nov 20, 2016 358 359 360 `````` 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 361 `````` `````` Robbert Krebbers committed Nov 03, 2016 362 `````` Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 363 `````` Proof. by rewrite big_opM_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 364 `````` `````` Robbert Krebbers committed May 31, 2016 365 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : `````` Robbert Krebbers committed Nov 03, 2016 366 `````` ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 367 `````` Proof. by rewrite big_opM_fmap. Qed. `````` Robbert Krebbers committed May 31, 2016 368 `````` `````` Robbert Krebbers committed Dec 02, 2016 369 370 371 `````` 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 372 `````` Proof. apply: big_opM_insert_override. Qed. `````` Robbert Krebbers committed May 31, 2016 373 `````` `````` Robbert Krebbers committed Dec 02, 2016 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 `````` 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 394 `````` Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : `````` Robbert Krebbers committed May 31, 2016 395 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 396 397 `````` ([∗ 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 398 399 `````` Proof. apply: big_opM_fn_insert. Qed. `````` Robbert Krebbers committed May 31, 2016 400 401 `````` Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 402 `````` ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). `````` Robbert Krebbers committed Sep 28, 2016 403 `````` Proof. apply: big_opM_fn_insert'. Qed. `````` Robbert Krebbers committed May 31, 2016 404 `````` `````` Robbert Krebbers committed Feb 18, 2016 405 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Nov 27, 2016 406 `````` ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) `````` Robbert Krebbers committed Nov 03, 2016 407 `````` ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 408 `````` Proof. apply: big_opM_opM. Qed. `````` Robbert Krebbers committed May 31, 2016 409 `````` `````` Robbert Krebbers committed Nov 27, 2016 410 411 412 413 414 `````` 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 415 `````` Lemma big_sepM_later Φ m : `````` Robbert Krebbers committed Nov 03, 2016 416 `````` ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 417 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 418 `````` `````` Robbert Krebbers committed Nov 27, 2016 419 420 421 422 `````` 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 423 `````` Lemma big_sepM_always Φ m : `````` Robbert Krebbers committed Nov 03, 2016 424 `````` (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 425 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 426 427 `````` Lemma big_sepM_always_if p Φ m : `````` Robbert Krebbers committed Nov 03, 2016 428 `````` □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 429 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 430 431 432 `````` Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 433 `````` ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed May 31, 2016 434 435 436 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 437 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. } `````` Robbert Krebbers committed Sep 28, 2016 438 439 440 `````` 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 441 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 442 `````` - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. `````` Robbert Krebbers committed Sep 28, 2016 443 444 `````` apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. `````` Robbert Krebbers committed Nov 21, 2016 445 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 446 447 448 `````` Qed. Lemma big_sepM_impl Φ Ψ m : `````` Ralf Jung committed Nov 22, 2016 449 `````` □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 450 `````` ⊢ [∗ map] k↦x ∈ m, Ψ k x. `````` Robbert Krebbers committed May 31, 2016 451 452 `````` Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. `````` Robbert Krebbers committed Jun 24, 2016 453 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 454 455 456 `````` 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 457 `````` `````` Robbert Krebbers committed Aug 28, 2016 458 `````` Global Instance big_sepM_empty_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 459 `````` PersistentP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 460 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 461 `````` Global Instance big_sepM_persistent Φ m : `````` Robbert Krebbers committed Nov 03, 2016 462 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 463 `````` Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed. `````` Robbert Krebbers committed Aug 28, 2016 464 `````` Global Instance big_sepM_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 465 `````` TimelessP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 466 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 467 `````` Global Instance big_sepM_timeless Φ m : `````` Robbert Krebbers committed Nov 03, 2016 468 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 469 `````` Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed. `````` Robbert Krebbers committed Feb 17, 2016 470 471 ``````End gmap. `````` Robbert Krebbers committed Aug 24, 2016 472 `````` `````` Robbert Krebbers committed Apr 08, 2016 473 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 474 475 476 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 477 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 478 `````` `````` Robbert Krebbers committed Feb 18, 2016 479 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 480 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 481 `````` ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x. `````` Robbert Krebbers committed Feb 17, 2016 482 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 483 `````` intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Sep 28, 2016 484 485 486 `````` - 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 487 `````` Qed. `````` Robbert Krebbers committed Oct 03, 2016 488 489 `````` Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 490 `````` ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). `````` Robbert Krebbers committed Oct 03, 2016 491 `````` Proof. apply: big_opS_proper. Qed. `````` Robbert Krebbers committed Sep 28, 2016 492 `````` `````` Robbert Krebbers committed Oct 03, 2016 493 `````` Global Instance big_sepS_mono' X : `````` Robbert Krebbers committed Sep 28, 2016 494 495 496 `````` 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 497 `````` Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 498 `````` Proof. by rewrite big_opS_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 499 `````` `````` Robbert Krebbers committed Feb 18, 2016 500 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 501 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 502 503 `````` Proof. apply: big_opS_insert. Qed. `````` Robbert Krebbers committed Jun 01, 2016 504 `````` Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : `````` Robbert Krebbers committed Apr 11, 2016 505 `````` x ∉ X → `````` Robbert Krebbers committed Nov 03, 2016 506 507 `````` ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). `````` Robbert Krebbers committed Sep 28, 2016 508 509 `````` Proof. apply: big_opS_fn_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 510 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed Nov 03, 2016 511 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 512 `````` Proof. apply: big_opS_fn_insert'. Qed. `````` Robbert Krebbers committed Apr 11, 2016 513 `````` `````` Robbert Krebbers committed Nov 21, 2016 514 515 516 517 518 `````` 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 519 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 520 `````` x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Sep 28, 2016 521 `````` Proof. apply: big_opS_delete. Qed. `````` Robbert Krebbers committed Apr 11, 2016 522 `````` `````` Robbert Krebbers committed Nov 03, 2016 523 `````` Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. `````` 524 `````` Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. `````` Robbert Krebbers committed May 31, 2016 525 `````` `````` Robbert Krebbers committed Nov 24, 2016 526 527 528 529 530 531 532 `````` 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 533 `````` Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 534 `````` Proof. apply: big_opS_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 535 `````` `````` Robbert Krebbers committed Nov 21, 2016 536 `````` Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X : `````` Ralf Jung committed Nov 22, 2016 537 `````` ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y). `````` Robbert Krebbers committed Nov 21, 2016 538 539 540 541 542 543 544 545 546 547 548 `````` 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 549 550 551 552 553 554 555 556 557 558 559 `````` 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 560 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Nov 03, 2016 561 `````` ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Sep 28, 2016 562 `````` Proof. apply: big_opS_opS. Qed. `````` Robbert Krebbers committed May 31, 2016 563 `````` `````` Robbert Krebbers committed Nov 27, 2016 564 565 566 567 `````` 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 568 `````` Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 569 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 570 `````` `````` Robbert Krebbers committed Nov 27, 2016 571 572 573 574 `````` 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 575 `````` Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 576 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 577 `````` `````` Robbert Krebbers committed May 31, 2016 578 `````` Lemma big_sepS_always_if q Φ X : `````` Robbert Krebbers committed Nov 03, 2016 579 `````` □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y). `````` Robbert Krebbers committed Sep 28, 2016 580 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 581 582 `````` Lemma big_sepS_forall Φ X : `````` Ralf Jung committed Nov 22, 2016 583 `````` (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). `````` Robbert Krebbers committed May 31, 2016 584 585 586 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 587 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. } `````` Robbert Krebbers committed Nov 21, 2016 588 `````` induction X as [|x X ? IH] using collection_ind_L. `````` Robbert Krebbers committed Sep 28, 2016 589 590 `````` { rewrite big_sepS_empty; auto. } rewrite big_sepS_insert // -always_and_sep_l. apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 591 `````` - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed Sep 28, 2016 592 `````` - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. `````` Robbert Krebbers committed Nov 21, 2016 593 `````` by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 594 595 596 `````` Qed. Lemma big_sepS_impl Φ Ψ X : `````` Ralf Jung committed Nov 22, 2016 597 `````` □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 598 599 `````` Proof. rewrite always_and_sep_l always_forall. `````` Robbert Krebbers committed Jun 24, 2016 600 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 601 602 603 `````` 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 604 `````` `````` Robbert Krebbers committed Nov 03, 2016 605 `````` Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 606 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 607 `````` Global Instance big_sepS_persistent Φ X : `````` Robbert Krebbers committed Nov 03, 2016 608 `````` (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 609 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Nov 03, 2016 610 `````` Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 611 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 612 `````` Global Instance big_sepS_timeless Φ X : `````` Robbert Krebbers committed Nov 03, 2016 613 `````` (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 614 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 615 ``````End gset. `````` Robbert Krebbers committed Nov 19, 2016 616 `````` `````` Robbert Krebbers committed Dec 02, 2016 617 618 619 620 ``````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 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 `````` (** ** 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 660 661 662 663 664 665 666 `````` 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 667 668 669 670 671 672 673 `````` 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 674 675 676 677 `````` Lemma big_sepMS_and Φ Ψ X : ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y). Proof. auto using big_sepMS_mono with I. Qed. `````` Robbert Krebbers committed Nov 19, 2016 678 679 680 `````` Lemma big_sepMS_later Φ X : ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y). Proof. apply (big_opMS_commute _). Qed. `````` Robbert Krebbers committed Nov 27, 2016 681 682 683 684 `````` Lemma big_sepMS_laterN Φ n X : ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y). Proof. apply (big_opMS_commute _). Qed. `````` Robbert Krebbers committed Nov 19, 2016 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 `````` Lemma big_sepMS_always Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y). Proof. apply (big_opMS_commute _). Qed. Lemma big_sepMS_always_if q Φ X : □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y). Proof. apply (big_opMS_commute _). Qed. Global Instance big_sepMS_empty_persistent Φ : PersistentP ([∗ mset] x ∈ ∅, Φ x). Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. Global Instance big_sepMS_persistent Φ X : (∀ x, PersistentP (Φ x)) → PersistentP ([∗ mset] x ∈ X, Φ x). Proof. rewrite /big_opMS. apply _. Qed. Global Instance big_sepMS_nil_timeless Φ : TimelessP ([∗ mset] x ∈ ∅, Φ x). Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. Global Instance big_sepMS_timeless Φ X : (∀ x, TimelessP (Φ x)) → TimelessP ([∗ mset] x ∈ X, Φ x). Proof. rewrite /big_opMS. apply _. Qed. End gmultiset. `````` Robbert Krebbers committed Feb 16, 2016 703 ``End big_op.``