big_op.v 31 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 `````` 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. `````` Robbert Krebbers committed Feb 09, 2017 40 `````` - intros n P Q ??. by ofe_subst. `````` Robbert Krebbers committed Oct 25, 2016 41 42 43 44 45 46 47 48 49 50 51 52 53 54 `````` - 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. `````` Robbert Krebbers committed Feb 09, 2017 55 `````` Canonical Structure uPredR := CMRAT (uPred M) uPred_cmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 56 57 58 59 60 61 62 63 64 65 `````` 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. `````` Robbert Krebbers committed Feb 09, 2017 66 `````` Canonical Structure uPredUR := UCMRAT (uPred M) uPred_ucmra_mixin. `````` Robbert Krebbers committed Oct 25, 2016 67 68 69 70 71 72 73 74 `````` 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 75 76 `````` 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 77 78 79 80 81 82 83 84 85 86 87 `````` 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 88 ``````Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Sep 28, 2016 89 `````` `````` Robbert Krebbers committed Nov 03, 2016 90 ``````Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P)) `````` Robbert Krebbers committed Aug 24, 2016 91 `````` (at level 200, l at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 92 93 `````` 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 94 `````` (at level 200, l at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 95 `````` format "[∗ list ] x ∈ l , P") : uPred_scope. `````` Robbert Krebbers committed Aug 24, 2016 96 `````` `````` Robbert Krebbers committed Nov 03, 2016 97 ``````Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P)) `````` Robbert Krebbers committed May 24, 2016 98 `````` (at level 200, m at level 10, k, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 99 100 `````` 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 101 `````` (at level 200, m at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 102 `````` format "[∗ map ] x ∈ m , P") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 103 `````` `````` Robbert Krebbers committed Nov 03, 2016 104 ``````Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P)) `````` Robbert Krebbers committed May 24, 2016 105 `````` (at level 200, X at level 10, x at level 1, right associativity, `````` Robbert Krebbers committed Nov 03, 2016 106 `````` format "[∗ set ] x ∈ X , P") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 107 `````` `````` Robbert Krebbers committed Nov 19, 2016 108 109 110 111 ``````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 112 ``````(** * Persistence and timelessness of lists of uPreds *) `````` Robbert Krebbers committed Mar 11, 2016 113 ``````Class PersistentL {M} (Ps : list (uPred M)) := `````` Robbert Krebbers committed Mar 15, 2016 114 `````` persistentL : Forall PersistentP Ps. `````` Robbert Krebbers committed Mar 11, 2016 115 ``````Arguments persistentL {_} _ {_}. `````` Robbert Krebbers committed Jan 22, 2017 116 ``````Hint Mode PersistentL + ! : typeclass_instances. `````` Robbert Krebbers committed Feb 14, 2016 117 `````` `````` Robbert Krebbers committed Aug 24, 2016 118 119 120 ``````Class TimelessL {M} (Ps : list (uPred M)) := timelessL : Forall TimelessP Ps. Arguments timelessL {_} _ {_}. `````` Robbert Krebbers committed Jan 22, 2017 121 ``````Hint Mode TimelessP + ! : typeclass_instances. `````` Robbert Krebbers committed Aug 24, 2016 122 `````` `````` Robbert Krebbers committed Apr 08, 2016 123 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 124 ``````Section big_op. `````` Robbert Krebbers committed May 27, 2016 125 ``````Context {M : ucmraT}. `````` Robbert Krebbers committed Feb 14, 2016 126 127 128 ``````Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Sep 28, 2016 129 130 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)). `````` Robbert Krebbers committed Feb 17, 2016 131 132 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Nov 03, 2016 133 ``````Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs. `````` Robbert Krebbers committed Sep 28, 2016 134 ``````Proof. by rewrite big_op_app. Qed. `````` Robbert Krebbers committed Feb 17, 2016 135 `````` `````` Robbert Krebbers committed Jan 06, 2017 136 137 ``````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 138 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. `````` Robbert Krebbers committed Sep 28, 2016 139 ``````Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. `````` Robbert Krebbers committed Nov 24, 2016 140 ``````Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps). `````` Robbert Krebbers committed Dec 06, 2016 141 ``````Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed. `````` Robbert Krebbers committed Feb 14, 2016 142 `````` `````` Robbert Krebbers committed Aug 24, 2016 143 ``````(** ** Persistence *) `````` Robbert Krebbers committed Nov 03, 2016 144 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 145 146 147 148 149 150 151 152 153 154 155 156 157 ``````Proof. induction 1; apply _. Qed. Global Instance nil_persistent : PersistentL (@nil (uPred M)). Proof. constructor. Qed. Global Instance cons_persistent P Ps : PersistentP P → PersistentL Ps → PersistentL (P :: Ps). Proof. by constructor. Qed. Global Instance app_persistent Ps Ps' : PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps'). Proof. apply Forall_app_2. Qed. Global Instance fmap_persistent {A} (f : A → uPred M) xs : (∀ x, PersistentP (f x)) → PersistentL (f <\$> xs). `````` Robbert Krebbers committed Aug 24, 2016 158 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 159 160 161 162 163 ``````Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys : (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys). Proof. unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 164 165 166 167 168 ``````Global Instance imap_persistent {A} (f : nat → A → uPred M) xs : (∀ i x, PersistentP (f i x)) → PersistentL (imap f xs). Proof. rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 169 170 `````` (** ** Timelessness *) `````` Robbert Krebbers committed Nov 03, 2016 171 ``````Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps). `````` Robbert Krebbers committed Aug 24, 2016 172 173 174 175 176 177 178 179 180 181 182 183 184 ``````Proof. induction 1; apply _. Qed. Global Instance nil_timeless : TimelessL (@nil (uPred M)). Proof. constructor. Qed. Global Instance cons_timeless P Ps : TimelessP P → TimelessL Ps → TimelessL (P :: Ps). Proof. by constructor. Qed. Global Instance app_timeless Ps Ps' : TimelessL Ps → TimelessL Ps' → TimelessL (Ps ++ Ps'). Proof. apply Forall_app_2. Qed. Global Instance fmap_timeless {A} (f : A → uPred M) xs : (∀ x, TimelessP (f x)) → TimelessL (f <\$> xs). `````` Robbert Krebbers committed Aug 24, 2016 185 ``````Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 186 187 188 189 190 ``````Global Instance zip_with_timeless {A B} (f : A → B → uPred M) xs ys : (∀ x y, TimelessP (f x y)) → TimelessL (zip_with f xs ys). Proof. unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Aug 24, 2016 191 192 193 194 195 196 197 198 199 200 201 202 ``````Global Instance imap_timeless {A} (f : nat → A → uPred M) xs : (∀ i x, TimelessP (f i x)) → TimelessL (imap f xs). Proof. rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto. Qed. (** ** Big ops over lists *) Section list. Context {A : Type}. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → uPred M. `````` Robbert Krebbers committed Nov 03, 2016 203 `````` Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 204 `````` Proof. done. Qed. `````` Robbert Krebbers committed Mar 15, 2017 205 206 `````` Lemma big_sepL_nil' P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y. Proof. apply True_intro. Qed. `````` Robbert Krebbers committed Sep 28, 2016 207 `````` 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 ``````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) : `````` Robbert Krebbers committed Mar 14, 2017 325 326 `````` ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)). `````` Ralf Jung committed Dec 20, 2016 327 `````` Proof. `````` Robbert Krebbers committed Mar 14, 2017 328 329 330 331 332 333 334 335 336 `````` revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//=. - rewrite big_sepL_nil. apply (anti_symm _), True_intro. trans ([∗ list] _↦_ ∈ x :: l1, True : uPred M)%I. + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro. + apply big_sepL_mono=> k y _. apply forall_intro=> z. by apply impl_intro_l, pure_elim_l. - rewrite !big_sepL_cons IH. apply sep_proper=> //. apply (anti_symm _). + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->]. + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro. `````` Ralf Jung committed Dec 20, 2016 337 338 `````` Qed. End list2. `````` Robbert Krebbers committed Aug 24, 2016 339 `````` `````` Robbert Krebbers committed Apr 08, 2016 340 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 341 342 343 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 344 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 345 `````` `````` Robbert Krebbers committed Feb 18, 2016 346 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 347 `````` m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 348 `````` ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x. `````` Robbert Krebbers committed Feb 16, 2016 349 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 350 `````` intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I. `````` Robbert Krebbers committed Jan 06, 2017 351 352 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, map_to_list_submseteq. `````` Robbert Krebbers committed Sep 28, 2016 353 `````` - apply big_opM_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 16, 2016 354 `````` Qed. `````` Robbert Krebbers committed Jul 22, 2016 355 356 `````` Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 357 `````` ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 358 `````` Proof. apply big_opM_proper. Qed. `````` Robbert Krebbers committed Feb 17, 2016 359 360 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 361 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Sep 28, 2016 362 363 `````` (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 364 `````` `````` Robbert Krebbers committed Nov 03, 2016 365 `````` Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 366 `````` Proof. by rewrite big_opM_empty. Qed. `````` Robbert Krebbers committed Mar 15, 2017 367 368 `````` Lemma big_sepM_empty' P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x. Proof. rewrite big_sepM_empty. apply True_intro. Qed. `````` Robbert Krebbers committed May 30, 2016 369 `````` `````` Robbert Krebbers committed May 31, 2016 370 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 371 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 372 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 373 `````` Proof. apply: big_opM_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 374 `````` `````` Robbert Krebbers committed May 31, 2016 375 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 376 `````` m !! i = Some x → `````` Robbert Krebbers committed Nov 03, 2016 377 `````` ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed Sep 28, 2016 378 `````` Proof. apply: big_opM_delete. Qed. `````` Robbert Krebbers committed May 30, 2016 379 `````` `````` Robbert Krebbers committed Nov 24, 2016 380 381 382 383 384 385 386 `````` 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 387 `````` Lemma big_sepM_lookup Φ m i x : `````` Robbert Krebbers committed Nov 03, 2016 388 `````` m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Nov 24, 2016 389 390 `````` Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. `````` Robbert Krebbers committed Nov 20, 2016 391 392 393 `````` 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 394 `````` `````` Robbert Krebbers committed Nov 03, 2016 395 `````` Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 396 `````` Proof. by rewrite big_opM_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 397 `````` `````` Robbert Krebbers committed May 31, 2016 398 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : `````` Robbert Krebbers committed Nov 03, 2016 399 `````` ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 400 `````` Proof. by rewrite big_opM_fmap. Qed. `````` Robbert Krebbers committed May 31, 2016 401 `````` `````` Robbert Krebbers committed Dec 02, 2016 402 403 404 `````` 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 405 `````` Proof. apply: big_opM_insert_override. Qed. `````` Robbert Krebbers committed May 31, 2016 406 `````` `````` Robbert Krebbers committed Dec 02, 2016 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 `````` 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 427 `````` Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : `````` Robbert Krebbers committed May 31, 2016 428 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 429 430 `````` ([∗ 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 431 432 `````` Proof. apply: big_opM_fn_insert. Qed. `````` Robbert Krebbers committed May 31, 2016 433 434 `````` Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 435 `````` ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). `````` Robbert Krebbers committed Sep 28, 2016 436 `````` Proof. apply: big_opM_fn_insert'. Qed. `````` Robbert Krebbers committed May 31, 2016 437 `````` `````` Robbert Krebbers committed Feb 18, 2016 438 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Nov 27, 2016 439 `````` ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) `````` Robbert Krebbers committed Nov 03, 2016 440 `````` ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 441 `````` Proof. apply: big_opM_opM. Qed. `````` Robbert Krebbers committed May 31, 2016 442 `````` `````` Robbert Krebbers committed Nov 27, 2016 443 444 445 446 447 `````` 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 448 `````` Lemma big_sepM_later Φ m : `````` Robbert Krebbers committed Nov 03, 2016 449 `````` ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 450 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 451 `````` `````` Robbert Krebbers committed Nov 27, 2016 452 453 454 455 `````` 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 456 `````` Lemma big_sepM_always Φ m : `````` Robbert Krebbers committed Nov 03, 2016 457 `````` (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 458 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 459 460 `````` Lemma big_sepM_always_if p Φ m : `````` Robbert Krebbers committed Nov 03, 2016 461 `````` □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 462 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 463 464 465 `````` Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 466 `````` ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed May 31, 2016 467 468 469 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 470 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. } `````` Robbert Krebbers committed Sep 28, 2016 471 472 473 `````` 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 474 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 475 `````` - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. `````` Robbert Krebbers committed Sep 28, 2016 476 477 `````` apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. `````` Robbert Krebbers committed Nov 21, 2016 478 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 479 480 481 `````` Qed. Lemma big_sepM_impl Φ Ψ m : `````` Ralf Jung committed Nov 22, 2016 482 `````` □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x) `````` Robbert Krebbers committed Nov 03, 2016 483 `````` ⊢ [∗ map] k↦x ∈ m, Ψ k x. `````` Robbert Krebbers committed May 31, 2016 484 485 `````` Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. `````` Robbert Krebbers committed Jun 24, 2016 486 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 487 488 489 `````` 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 490 `````` `````` Robbert Krebbers committed Aug 28, 2016 491 `````` Global Instance big_sepM_empty_persistent Φ : `````` Robbert Krebbers committed Nov 03, 2016 492 `````` PersistentP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 493 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 494 `````` Global Instance big_sepM_persistent Φ m : `````` Robbert Krebbers committed Nov 03, 2016 495 `````` (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 496 `````` Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed. `````` Robbert Krebbers committed Aug 28, 2016 497 `````` Global Instance big_sepM_nil_timeless Φ : `````` Robbert Krebbers committed Nov 03, 2016 498 `````` TimelessP ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 499 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 500 `````` Global Instance big_sepM_timeless Φ m : `````` Robbert Krebbers committed Nov 03, 2016 501 `````` (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 502 `````` Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed. `````` Robbert Krebbers committed Feb 17, 2016 503 504 ``````End gmap. `````` Robbert Krebbers committed Aug 24, 2016 505 `````` `````` Robbert Krebbers committed Apr 08, 2016 506 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 507 508 509 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 510 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 511 `````` `````` Robbert Krebbers committed Feb 18, 2016 512 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 513 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 514 `````` ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x. `````` Robbert Krebbers committed Feb 17, 2016 515 `````` Proof. `````` Robbert Krebbers committed Nov 03, 2016 516 `````` intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Jan 06, 2017 517 518 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, elements_submseteq. `````` Robbert Krebbers committed Sep 28, 2016 519 `````` - apply big_opS_forall; apply _ || auto. `````` Robbert Krebbers committed Feb 17, 2016 520 `````` Qed. `````` Robbert Krebbers committed Oct 03, 2016 521 522 `````` Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 523 `````` ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). `````` Robbert Krebbers committed Oct 03, 2016 524 `````` Proof. apply: big_opS_proper. Qed. `````` Robbert Krebbers committed Sep 28, 2016 525 `````` `````` Robbert Krebbers committed Oct 03, 2016 526 `````` Global Instance big_sepS_mono' X : `````` Robbert Krebbers committed Sep 28, 2016 527 528 529 `````` 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 530 `````` Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Sep 28, 2016 531 `````` Proof. by rewrite big_opS_empty. Qed. `````` Robbert Krebbers committed Mar 15, 2017 532 533 `````` Lemma big_sepS_empty' P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x. Proof. rewrite big_sepS_empty. apply True_intro. Qed. `````` Robbert Krebbers committed Apr 11, 2016 534 `````` `````` Robbert Krebbers committed Feb 18, 2016 535 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 536 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 537 538 `````` Proof. apply: big_opS_insert. Qed. `````` Robbert Krebbers committed Jun 01, 2016 539 `````` Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : `````` Robbert Krebbers committed Apr 11, 2016 540 `````` x ∉ X → `````` Robbert Krebbers committed Nov 03, 2016 541 542 `````` ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). `````` Robbert Krebbers committed Sep 28, 2016 543 544 `````` Proof. apply: big_opS_fn_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 545 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed Nov 03, 2016 546 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Sep 28, 2016 547 `````` Proof. apply: big_opS_fn_insert'. Qed. `````` Robbert Krebbers committed Apr 11, 2016 548 `````` `````` Robbert Krebbers committed Nov 21, 2016 549 550 551 552 553 `````` 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 554 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 555 `````` x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Sep 28, 2016 556 `````` Proof. apply: big_opS_delete. Qed. `````` Robbert Krebbers committed Apr 11, 2016 557 `````` `````` Robbert Krebbers committed Nov 03, 2016 558 `````` Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. `````` 559 `````` Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. `````` Robbert Krebbers committed May 31, 2016 560 `````` `````` Robbert Krebbers committed Nov 24, 2016 561 562 563 564 565 566 567 `````` 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 568 `````` Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Sep 28, 2016 569 `````` Proof. apply: big_opS_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 570 `````` `````` Robbert Krebbers committed Nov 21, 2016 571 `````` Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X : `````` Ralf Jung committed Nov 22, 2016 572 `````` ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y). `````` Robbert Krebbers committed Nov 21, 2016 573 574 575 576 577 578 579 580 581 582 583 `````` 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 584 585 586 587 588 589 590 591 592 593 594 `````` 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 595 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Nov 03, 2016 596 `````` ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Sep 28, 2016 597 `````` Proof. apply: big_opS_opS. Qed. `````` Robbert Krebbers committed May 31, 2016 598 `````` `````` Robbert Krebbers committed Nov 27, 2016 599 600 601 602 `````` 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 603 `````` Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 604 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 605 `````` `````` Robbert Krebbers committed Nov 27, 2016 606 607 608 609 `````` 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 610 `````` Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y). `````` Robbert Krebbers committed Sep 28, 2016 611 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 612 `````` `````` Robbert Krebbers committed May 31, 2016 613 `````` Lemma big_sepS_always_if q Φ X : `````` Robbert Krebbers committed Nov 03, 2016 614 `````` □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y). `````` Robbert Krebbers committed Sep 28, 2016 615 `````` Proof. apply (big_opS_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 616 617 `````` Lemma big_sepS_forall Φ X : `````` Ralf Jung committed Nov 22, 2016 618 `````` (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). `````` Robbert Krebbers committed May 31, 2016 619 620 621 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> x. `````` Robbert Krebbers committed Jun 24, 2016 622 `````` apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. } `````` Robbert Krebbers committed Nov 21, 2016 623 `````` induction X as [|x X ? IH] using collection_ind_L. `````` Robbert Krebbers committed Sep 28, 2016 624 625 `````` { rewrite big_sepS_empty; auto. } rewrite big_sepS_insert // -always_and_sep_l. apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 626 `````` - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed Sep 28, 2016 627 `````` - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. `````` Robbert Krebbers committed Nov 21, 2016 628 `````` by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 629 630 631 `````` Qed. Lemma big_sepS_impl Φ Ψ X : `````` Ralf Jung committed Nov 22, 2016 632 `````` □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 633 634 `````` Proof. rewrite always_and_sep_l always_forall. `````` Robbert Krebbers committed Jun 24, 2016 635 `````` setoid_rewrite always_impl; setoid_rewrite always_pure. `````` Robbert Krebbers committed May 31, 2016 636 637 638 `````` 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 639 `````` `````` Robbert Krebbers committed Nov 03, 2016 640 `````` Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 641 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 642 `````` Global Instance big_sepS_persistent Φ X : `````` Robbert Krebbers committed Nov 03, 2016 643 `````` (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 644 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Nov 03, 2016 645 `````` Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 646 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 647 `````` Global Instance big_sepS_timeless Φ X : `````` Robbert Krebbers committed Nov 03, 2016 648 `````` (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 649 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 650 ``````End gset. `````` Robbert Krebbers committed Nov 19, 2016 651 `````` `````` Robbert Krebbers committed Dec 02, 2016 652 653 654 655 ``````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 656 657 658 659 660 661 662 663 664 665 666 667 `````` (** ** 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 668 669 `````` - apply uPred_included. apply: big_op_submseteq. by apply fmap_submseteq, gmultiset_elements_submseteq. `````` Robbert Krebbers committed Nov 19, 2016 670 671 672 673 674 675 676 677 678 679 680 681 682 `````` - apply big_opMS_forall; apply _ || auto. Qed. Lemma big_sepMS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x