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