big_op.v 30.8 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. `````` Ralf Jung committed Feb 06, 2017 3 ``````From stdpp Require Import gmap fin_collections gmultiset functions. `````` Ralf Jung committed Jan 05, 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 Jan 22, 2017 118 ``````Hint Mode PersistentL + ! : typeclass_instances. `````` Robbert Krebbers committed Feb 14, 2016 119 `````` `````` Robbert Krebbers committed Aug 24, 2016 120 121 122 ``````Class TimelessL {M} (Ps : list (uPred M)) := timelessL : Forall TimelessP Ps. Arguments timelessL {_} _ {_}. `````` Robbert Krebbers committed Jan 22, 2017 123 ``````Hint Mode TimelessP + ! : typeclass_instances. `````` Robbert Krebbers committed Aug 24, 2016 124 `````` `````` Robbert Krebbers committed Apr 08, 2016 125 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 126 ``````Section big_op. `````` Robbert Krebbers committed May 27, 2016 127 ``````Context {M : ucmraT}. `````` Robbert Krebbers committed Feb 14, 2016 128 129 130 ``````Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Sep 28, 2016 131 132 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)). `````` Robbert Krebbers committed Feb 17, 2016 133 134 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Nov 03, 2016 135 ``````Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 136 ``````Proof. by rewrite big_op_app. Qed. `````` Robbert Krebbers committed Feb 17, 2016 137 `````` `````` Robbert Krebbers committed Jan 06, 2017 138 139 ``````Lemma big_sep_submseteq Ps Qs : Qs ⊆+ Ps → [∗] Ps ⊢ [∗] Qs. Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed. `````` Robbert Krebbers committed Nov 03, 2016 140 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. `````` Robbert Krebbers committed Sep 28, 2016 141 ``````Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. `````` Robbert Krebbers committed Nov 24, 2016 142 ``````Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps). `````` Robbert Krebbers committed Dec 06, 2016 143 ``````Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Feb 14, 2016 144 `````` `````` Robbert Krebbers committed Aug 24, 2016 145 ``````(** ** Persistence *) `````` Robbert Krebbers committed Nov 03, 2016 146 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 147 148 149 150 151 152 153 154 155 156 157 158 159 ``````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 160 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 161 162 163 164 165 ``````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 166 167 168 169 170 ``````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 171 172 `````` (** ** Timelessness *) `````` Robbert Krebbers committed Nov 03, 2016 173 ``````Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 174 175 176 177 178 179 180 181 182 183 184 185 186 ``````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 187 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 188 189 190 191 192 ``````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 193 194 195 196 197 198 199 200 201 202 203 204 ``````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 205 `````` Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 206 207 `````` Proof. done. Qed. Lemma big_sepL_cons Φ x l : `````` Robbert Krebbers committed Nov 03, 2016 208 `````` ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y. `````` Robbert Krebbers committed Sep 28, 2016 209 `````` Proof. by rewrite big_opL_cons. Qed. `````` Robbert Krebbers committed Nov 03, 2016 210 `````` Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. `````` Robbert Krebbers committed Sep 28, 2016 211 212 `````` Proof. by rewrite big_opL_singleton. Qed. Lemma big_sepL_app Φ l1 l2 : `````` Robbert Krebbers committed Nov 03, 2016 213 214 `````` ([∗ 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 215 216 `````` Proof. by rewrite big_opL_app. Qed. `````` Robbert Krebbers committed Aug 24, 2016 217 218 `````` Lemma big_sepL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 219 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y. `````` Robbert Krebbers committed Sep 28, 2016 220 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 221 222 `````` Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 223 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y). `````` Robbert Krebbers committed Sep 28, 2016 224 `````` Proof. apply big_opL_proper. Qed. `````` Robbert Krebbers committed Jan 06, 2017 225 226 227 `````` Lemma big_sepL_submseteq (Φ : A → uPred M) l1 l2 : l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y. Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed. `````` Robbert Krebbers committed Aug 24, 2016 228 229 230 `````` Global Instance big_sepL_mono' l : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 231 232 `````` (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 233 `````` `````` Jacques-Henri Jourdan committed Dec 05, 2016 234 235 236 237 `````` 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 238 239 `````` 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 240 241 `````` Qed. `````` Robbert Krebbers committed Aug 24, 2016 242 `````` Lemma big_sepL_lookup Φ l i x : `````` Robbert Krebbers committed Nov 03, 2016 243 `````` l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 244 `````` Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed. `````` Robbert Krebbers committed Aug 24, 2016 245 `````` `````` Robbert Krebbers committed Aug 28, 2016 246 `````` Lemma big_sepL_elem_of (Φ : A → uPred M) l x : `````` Robbert Krebbers committed Nov 03, 2016 247 `````` x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 248 `````` Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed. `````` Robbert Krebbers committed Aug 28, 2016 249 `````` `````` Robbert Krebbers committed Aug 24, 2016 250 `````` Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l : `````` Robbert Krebbers committed Nov 03, 2016 251 `````` ([∗ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 252 `````` Proof. by rewrite big_opL_fmap. Qed. `````` Robbert Krebbers committed Aug 24, 2016 253 254 `````` Lemma big_sepL_sepL Φ Ψ l : `````` Robbert Krebbers committed Nov 03, 2016 255 256 `````` ([∗ 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 257 `````` Proof. by rewrite big_opL_opL. Qed. `````` Robbert Krebbers committed Sep 28, 2016 258 `````` `````` Robbert Krebbers committed Nov 27, 2016 259 260 261 262 263 `````` 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 264 `````` Lemma big_sepL_later Φ l : `````` Robbert Krebbers committed Nov 03, 2016 265 `````` ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 266 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 267 `````` `````` Robbert Krebbers committed Nov 27, 2016 268 269 270 271 `````` 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 272 `````` Lemma big_sepL_always Φ l : `````` Robbert Krebbers committed Nov 03, 2016 273 `````` (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 274 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 275 276 `````` Lemma big_sepL_always_if p Φ l : `````` Robbert Krebbers committed Nov 03, 2016 277 `````` □?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 278 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 279 280 281 `````` Lemma big_sepL_forall Φ l : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 282 `````` ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 283 284 285 286 287 288 289 `````` 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 290 `````` - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. `````` Robbert Krebbers committed Aug 24, 2016 291 292 293 294 `````` - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. Lemma big_sepL_impl Φ Ψ l : `````` Ralf Jung committed Nov 22, 2016 295 `````` □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 296 `````` ⊢ [∗ list] k↦x ∈ l, Ψ k x. `````` Robbert Krebbers committed Aug 24, 2016 297 298 299 300 301 302 303 `````` 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 304 `````` Global Instance big_sepL_nil_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 305 `````` PersistentP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 306 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 307 `````` Global Instance big_sepL_persistent Φ l : `````` Robbert Krebbers committed Nov 03, 2016 308 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 309 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 310 `````` Global Instance big_sepL_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 311 `````` TimelessP ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 312 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 28, 2016 313 `````` Global Instance big_sepL_timeless Φ l : `````` Robbert Krebbers committed Nov 03, 2016 314 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 315 `````` Proof. rewrite /big_opL. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 316 317 ``````End list. `````` Ralf Jung committed Dec 20, 2016 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 344 345 ``````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 346 `````` `````` Robbert Krebbers committed Apr 08, 2016 347 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 348 349 350 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 351 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 352 `````` `````` Robbert Krebbers committed Feb 18, 2016 353 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 354 `````` m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 355 `````` ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x. `````` Robbert Krebbers committed Feb 16, 2016 356 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 357 `````` intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I. `````` Robbert Krebbers committed Jan 06, 2017 358 359 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, map_to_list_submseteq. `````` Robbert Krebbers committed Sep 28, 2016 360 `````` - apply big_opM_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 16, 2016 361 `````` Qed. `````` Robbert Krebbers committed Jul 22, 2016 362 363 `````` Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 364 `````` ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 365 `````` Proof. apply big_opM_proper. Qed. `````` Robbert Krebbers committed Feb 17, 2016 366 367 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 368 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 369 370 `````` (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 371 `````` `````` Robbert Krebbers committed Nov 03, 2016 372 `````` Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 373 `````` Proof. by rewrite big_opM_empty. Qed. `````` Robbert Krebbers committed May 30, 2016 374 `````` `````` Robbert Krebbers committed May 31, 2016 375 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 376 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 377 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 378 `````` Proof. apply: big_opM_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 379 `````` `````` Robbert Krebbers committed May 31, 2016 380 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 381 `````` m !! i = Some x → `````` Robbert Krebbers committed Nov 03, 2016 382 `````` ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 383 `````` Proof. apply: big_opM_delete. Qed. `````` Robbert Krebbers committed May 30, 2016 384 `````` `````` Robbert Krebbers committed Nov 24, 2016 385 386 387 388 389 390 391 `````` 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 392 `````` Lemma big_sepM_lookup Φ m i x : `````` Robbert Krebbers committed Nov 03, 2016 393 `````` m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Nov 24, 2016 394 395 `````` Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. `````` Robbert Krebbers committed Nov 20, 2016 396 397 398 `````` 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 399 `````` `````` Robbert Krebbers committed Nov 03, 2016 400 `````` Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 401 `````` Proof. by rewrite big_opM_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 402 `````` `````` Robbert Krebbers committed May 31, 2016 403 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : `````` Robbert Krebbers committed Nov 03, 2016 404 `````` ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 405 `````` Proof. by rewrite big_opM_fmap. Qed. `````` Robbert Krebbers committed May 31, 2016 406 `````` `````` Robbert Krebbers committed Dec 02, 2016 407 408 409 `````` 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 410 `````` Proof. apply: big_opM_insert_override. Qed. `````` Robbert Krebbers committed May 31, 2016 411 `````` `````` Robbert Krebbers committed Dec 02, 2016 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 `````` 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 432 `````` Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : `````` Robbert Krebbers committed May 31, 2016 433 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 434 435 `````` ([∗ 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 436 437 `````` Proof. apply: big_opM_fn_insert. Qed. `````` Robbert Krebbers committed May 31, 2016 438 439 `````` Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 440 `````` ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). `````` Robbert Krebbers committed Sep 28, 2016 441 `````` Proof. apply: big_opM_fn_insert'. Qed. `````` Robbert Krebbers committed May 31, 2016 442 `````` `````` Robbert Krebbers committed Feb 18, 2016 443 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Nov 27, 2016 444 `````` ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) `````` Robbert Krebbers committed Nov 03, 2016 445 `````` ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 446 `````` Proof. apply: big_opM_opM. Qed. `````` Robbert Krebbers committed May 31, 2016 447 `````` `````` Robbert Krebbers committed Nov 27, 2016 448 449 450 451 452 `````` 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 453 `````` Lemma big_sepM_later Φ m : `````` Robbert Krebbers committed Nov 03, 2016 454 `````` ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 455 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 456 `````` `````` Robbert Krebbers committed Nov 27, 2016 457 458 459 460 `````` 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 461 `````` Lemma big_sepM_always Φ m : `````` Robbert Krebbers committed Nov 03, 2016 462 `````` (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 463 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 464 465 `````` Lemma big_sepM_always_if p Φ m : `````` Robbert Krebbers committed Nov 03, 2016 466 `````` □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 467 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 468 469 470 `````` Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 471 `````` ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed May 31, 2016 472 473 474 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 475 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. } `````` Robbert Krebbers committed Sep 28, 2016 476 477 478 `````` 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 479 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 480 `````` - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. `````` Robbert Krebbers committed Sep 28, 2016 481 482 `````` apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. `````` Robbert Krebbers committed Nov 21, 2016 483 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 484 485 486 `````` Qed. Lemma big_sepM_impl Φ Ψ m : `````` Ralf Jung committed Nov 22, 2016 487 `````` □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 488 `````` ⊢ [∗ map] k↦x ∈ m, Ψ k x. `````` Robbert Krebbers committed May 31, 2016 489 490 `````` Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. `````` Robbert Krebbers committed Jun 24, 2016 491 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 492 493 494 `````` 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 495 `````` `````` Robbert Krebbers committed Aug 28, 2016 496 `````` Global Instance big_sepM_empty_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 497 `````` PersistentP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 498 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 499 `````` Global Instance big_sepM_persistent Φ m : `````` Robbert Krebbers committed Nov 03, 2016 500 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 501 `````` Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed. `````` Robbert Krebbers committed Aug 28, 2016 502 `````` Global Instance big_sepM_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 503 `````` TimelessP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 504 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 505 `````` Global Instance big_sepM_timeless Φ m : `````` Robbert Krebbers committed Nov 03, 2016 506 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 507 `````` Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed. `````` Robbert Krebbers committed Feb 17, 2016 508 509 ``````End gmap. `````` Robbert Krebbers committed Aug 24, 2016 510 `````` `````` Robbert Krebbers committed Apr 08, 2016 511 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 512 513 514 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 515 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 516 `````` `````` Robbert Krebbers committed Feb 18, 2016 517 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 518 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 519 `````` ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x. `````` Robbert Krebbers committed Feb 17, 2016 520 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 521 `````` intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Jan 06, 2017 522 523 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, elements_submseteq. `````` Robbert Krebbers committed Sep 28, 2016 524 `````` - apply big_opS_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 17, 2016 525 `````` Qed. `````` Robbert Krebbers committed Oct 03, 2016 526 527 `````` Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 528 `````` ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). `````` Robbert Krebbers committed Oct 03, 2016 529 `````` Proof. apply: big_opS_proper. Qed. `````` Robbert Krebbers committed Sep 28, 2016 530 `````` `````` Robbert Krebbers committed Oct 03, 2016 531 `````` Global Instance big_sepS_mono' X : `````` Robbert Krebbers committed Sep 28, 2016 532 533 534 `````` 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 535 `````` Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 536 `````` Proof. by rewrite big_opS_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 537 `````` `````` Robbert Krebbers committed Feb 18, 2016 538 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 539 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 540 541 `````` Proof. apply: big_opS_insert. Qed. `````` Robbert Krebbers committed Jun 01, 2016 542 `````` Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : `````` Robbert Krebbers committed Apr 11, 2016 543 `````` x ∉ X → `````` Robbert Krebbers committed Nov 03, 2016 544 545 `````` ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). `````` Robbert Krebbers committed Sep 28, 2016 546 547 `````` Proof. apply: big_opS_fn_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 548 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed Nov 03, 2016 549 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 550 `````` Proof. apply: big_opS_fn_insert'. Qed. `````` Robbert Krebbers committed Apr 11, 2016 551 `````` `````` Robbert Krebbers committed Nov 21, 2016 552 553 554 555 556 `````` 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 557 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 558 `````` x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Sep 28, 2016 559 `````` Proof. apply: big_opS_delete. Qed. `````` Robbert Krebbers committed Apr 11, 2016 560 `````` `````` Robbert Krebbers committed Nov 03, 2016 561 `````` Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. `````` 562 `````` Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. `````` Robbert Krebbers committed May 31, 2016 563 `````` `````` Robbert Krebbers committed Nov 24, 2016 564 565 566 567 568 569 570 `````` 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 571 `````` Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 572 `````` Proof. apply: big_opS_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 573 `````` `````` Robbert Krebbers committed Nov 21, 2016 574 `````` Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X : `````` Ralf Jung committed Nov 22, 2016 575 `````` ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y). `````` Robbert Krebbers committed Nov 21, 2016 576 577 578 579 580 581 582 583 584 585 586 `````` 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 587 588 589 590 591 592 593 594 595 596 597 `````` 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 598 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Nov 03, 2016 599 `````` ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Sep 28, 2016 600 `````` Proof. apply: big_opS_opS. Qed. `````` Robbert Krebbers committed May 31, 2016 601 `````` `````` Robbert Krebbers committed Nov 27, 2016 602 603 604 605 `````` 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 606 `````` Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 607 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 608 `````` `````` Robbert Krebbers committed Nov 27, 2016 609 610 611 612 `````` 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 613 `````` Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 614 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 615 `````` `````` Robbert Krebbers committed May 31, 2016 616 `````` Lemma big_sepS_always_if q Φ X : `````` Robbert Krebbers committed Nov 03, 2016 617 `````` □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y). `````` Robbert Krebbers committed Sep 28, 2016 618 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 619 620 `````` Lemma big_sepS_forall Φ X : `````` Ralf Jung committed Nov 22, 2016 621 `````` (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). `````` Robbert Krebbers committed May 31, 2016 622 623 624 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 625 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. } `````` Robbert Krebbers committed Nov 21, 2016 626 `````` induction X as [|x X ? IH] using collection_ind_L. `````` Robbert Krebbers committed Sep 28, 2016 627 628 `````` { rewrite big_sepS_empty; auto. } rewrite big_sepS_insert // -always_and_sep_l. apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 629 `````` - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed Sep 28, 2016 630 `````` - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. `````` Robbert Krebbers committed Nov 21, 2016 631 `````` by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 632 633 634 `````` Qed. Lemma big_sepS_impl Φ Ψ X : `````` Ralf Jung committed Nov 22, 2016 635 `````` □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 636 637 `````` Proof. rewrite always_and_sep_l always_forall. `````` Robbert Krebbers committed Jun 24, 2016 638 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 639 640 641 `````` 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 642 `````` `````` Robbert Krebbers committed Nov 03, 2016 643 `````` Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 644 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 645 `````` Global Instance big_sepS_persistent Φ X : `````` Robbert Krebbers committed Nov 03, 2016 646 `````` (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 647 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Nov 03, 2016 648 `````` Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 649 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 650 `````` Global Instance big_sepS_timeless Φ X : `````` Robbert Krebbers committed Nov 03, 2016 651 `````` (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 652 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 653 ``````End gset. `````` Robbert Krebbers committed Nov 19, 2016 654 `````` `````` Robbert Krebbers committed Dec 02, 2016 655 656 657 658 ``````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 659 660 661 662 663 664 665 666 667 668 669 670 `````` (** ** 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. `````` Robbert Krebbers committed Jan 06, 2017 671 672 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, gmultiset_elements_submseteq. `````` Robbert Krebbers committed Nov 19, 2016 673