big_op.v 36.2 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.algebra Require Export big_op. `````` Ralf Jung committed Mar 21, 2018 2 ``````From iris.bi Require Import derived_laws_sbi plainly. `````` Robbert Krebbers committed Oct 30, 2017 3 ``````From stdpp Require Import countable fin_collections functions. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Ralf Jung committed May 29, 2018 5 ``````Import interface.bi derived_laws_bi.bi. `````` Robbert Krebbers committed Feb 14, 2016 6 `````` `````` Robbert Krebbers committed Oct 25, 2016 7 ``````(* Notations *) `````` Ralf Jung committed Jun 05, 2018 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 ``````Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l) : bi_scope. Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l) : bi_scope. Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope. Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l) : bi_scope. Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l) : bi_scope. Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope. Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope. Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope. Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope. Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope. `````` Robbert Krebbers committed Aug 24, 2016 28 `````` `````` Robbert Krebbers committed Apr 08, 2016 29 ``````(** * Properties *) `````` Robbert Krebbers committed Oct 30, 2017 30 31 32 ``````Section bi_big_op. Context {PROP : bi}. Implicit Types Ps Qs : list PROP. `````` Robbert Krebbers committed Feb 14, 2016 33 34 ``````Implicit Types A : Type. `````` Robbert Krebbers committed Aug 24, 2016 35 ``````(** ** Big ops over lists *) `````` Robbert Krebbers committed Oct 30, 2017 36 ``````Section sep_list. `````` Robbert Krebbers committed Aug 24, 2016 37 38 `````` Context {A : Type}. Implicit Types l : list A. `````` Robbert Krebbers committed Oct 30, 2017 39 `````` Implicit Types Φ Ψ : nat → A → PROP. `````` Robbert Krebbers committed Aug 24, 2016 40 `````` `````` Robbert Krebbers committed Oct 30, 2017 41 `````` Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp. `````` Robbert Krebbers committed Sep 28, 2016 42 `````` Proof. done. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 43 `````` Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y. `````` Robbert Krebbers committed Oct 30, 2017 44 `````` Proof. apply (affine _). Qed. `````` Robbert Krebbers committed Sep 28, 2016 45 `````` Lemma big_sepL_cons Φ x l : `````` Robbert Krebbers committed Nov 03, 2016 46 `````` ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y. `````` Robbert Krebbers committed Sep 28, 2016 47 `````` Proof. by rewrite big_opL_cons. Qed. `````` Robbert Krebbers committed Nov 03, 2016 48 `````` Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. `````` Robbert Krebbers committed Sep 28, 2016 49 50 `````` Proof. by rewrite big_opL_singleton. Qed. Lemma big_sepL_app Φ l1 l2 : `````` Robbert Krebbers committed Nov 03, 2016 51 52 `````` ([∗ 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 53 54 `````` Proof. by rewrite big_opL_app. Qed. `````` Robbert Krebbers committed Aug 24, 2016 55 56 `````` Lemma big_sepL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 57 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y. `````` Robbert Krebbers committed Sep 28, 2016 58 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 59 60 `````` Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → `````` Robbert Krebbers committed Nov 03, 2016 61 `````` ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y). `````` Robbert Krebbers committed Sep 28, 2016 62 `````` Proof. apply big_opL_proper. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 63 `````` Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A → PROP) l1 l2 : `````` Robbert Krebbers committed Jan 06, 2017 64 `````` l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y. `````` Robbert Krebbers committed Oct 30, 2017 65 66 67 `````` Proof. intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l. Qed. `````` Robbert Krebbers committed Aug 24, 2016 68 `````` `````` Robbert Krebbers committed Mar 24, 2017 69 70 `````` Global Instance big_sepL_mono' : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢)) `````` Robbert Krebbers committed Oct 30, 2017 71 `````` (big_opL (@bi_sep PROP) (A:=A)). `````` Robbert Krebbers committed Mar 24, 2017 72 73 `````` Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Global Instance big_sep_mono' : `````` Robbert Krebbers committed Oct 30, 2017 74 `````` Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep M) (λ _ P, P)). `````` Robbert Krebbers committed Mar 24, 2017 75 `````` Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Aug 24, 2016 76 `````` `````` Ralf Jung committed Apr 05, 2018 77 `````` Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢@{PROP} emp. `````` Robbert Krebbers committed Oct 30, 2017 78 79 `````` Proof. by rewrite big_opL_unit. Qed. `````` Jacques-Henri Jourdan committed Dec 05, 2016 80 81 82 83 `````` 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 Mar 24, 2017 84 85 86 `````` intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=. rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl. rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l. `````` Jacques-Henri Jourdan committed Dec 05, 2016 87 88 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 89 `````` Lemma big_sepL_lookup Φ l i x `{!Absorbing (Φ i x)} : `````` Robbert Krebbers committed Nov 03, 2016 90 `````` l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Oct 30, 2017 91 `````` Proof. intros. rewrite big_sepL_lookup_acc //. by rewrite sep_elim_l. Qed. `````` Robbert Krebbers committed Aug 24, 2016 92 `````` `````` Robbert Krebbers committed Oct 30, 2017 93 `````` Lemma big_sepL_elem_of (Φ : A → PROP) l x `{!Absorbing (Φ x)} : `````` Robbert Krebbers committed Nov 03, 2016 94 `````` x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x. `````` Robbert Krebbers committed Mar 24, 2017 95 96 97 `````` Proof. intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)). Qed. `````` Robbert Krebbers committed Aug 28, 2016 98 `````` `````` Robbert Krebbers committed Oct 30, 2017 99 `````` Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l : `````` Robbert Krebbers committed Nov 03, 2016 100 `````` ([∗ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 101 `````` Proof. by rewrite big_opL_fmap. Qed. `````` Robbert Krebbers committed Aug 24, 2016 102 103 `````` Lemma big_sepL_sepL Φ Ψ l : `````` Robbert Krebbers committed Nov 03, 2016 104 105 `````` ([∗ 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 106 `````` Proof. by rewrite big_opL_opL. Qed. `````` Robbert Krebbers committed Sep 28, 2016 107 `````` `````` Robbert Krebbers committed Nov 27, 2016 108 109 110 `````` 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). `````` Robbert Krebbers committed Oct 30, 2017 111 `````` Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed. `````` Robbert Krebbers committed Nov 27, 2016 112 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 113 `````` Lemma big_sepL_persistently `{BiAffine PROP} Φ l : `````` Robbert Krebbers committed Mar 04, 2018 114 `````` ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, (Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 115 `````` Proof. apply (big_opL_commute _). Qed. `````` Robbert Krebbers committed Aug 24, 2016 116 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 117 `````` Lemma big_sepL_forall `{BiAffine PROP} Φ l : `````` Robbert Krebbers committed Oct 25, 2017 118 `````` (∀ k x, Persistent (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 119 `````` ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed Aug 24, 2016 120 121 122 `````` Proof. intros HΦ. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Oct 30, 2017 123 124 `````` apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. } revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ; [by auto using big_sepL_nil'|]. `````` Robbert Krebbers committed Oct 30, 2017 125 `````` rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 126 `````` - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. `````` Robbert Krebbers committed Aug 24, 2016 127 128 129 130 `````` - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. Lemma big_sepL_impl Φ Ψ l : `````` Robbert Krebbers committed Oct 30, 2017 131 `````` ([∗ list] k↦x ∈ l, Φ k x) -∗ `````` Jacques-Henri Jourdan committed Nov 02, 2017 132 `````` □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗ `````` Robbert Krebbers committed Oct 30, 2017 133 `````` [∗ list] k↦x ∈ l, Ψ k x. `````` Robbert Krebbers committed Aug 24, 2016 134 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 135 136 `````` apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=. { by rewrite sep_elim_r. } `````` 137 `````` rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. `````` Robbert Krebbers committed Oct 30, 2017 138 139 `````` apply sep_mono. - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. `````` 140 `````` by rewrite intuitionistically_elim wand_elim_l. `````` Robbert Krebbers committed Oct 30, 2017 141 `````` - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=. `````` Jacques-Henri Jourdan committed Nov 02, 2017 142 `````` apply sep_mono_l, affinely_mono, persistently_mono. `````` Robbert Krebbers committed Oct 30, 2017 143 `````` apply forall_intro=> k. by rewrite (forall_elim (S k)). `````` Robbert Krebbers committed Aug 24, 2016 144 145 `````` Qed. `````` Robbert Krebbers committed Apr 04, 2018 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 `````` Lemma big_sepL_delete Φ l i x : l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, if decide (k = i) then emp else Φ k y. Proof. intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r. rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl. rewrite decide_True // left_id. rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv. - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk. rewrite take_length in Hk. by rewrite decide_False; last lia. - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia. Qed. Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x : l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y. Proof. intros. rewrite big_sepL_delete //. (do 2 f_equiv)=> k y. rewrite -decide_emp. by repeat case_decide. Qed. `````` Robbert Krebbers committed Oct 30, 2017 168 `````` Global Instance big_sepL_nil_persistent Φ : `````` Robbert Krebbers committed Oct 25, 2017 169 `````` Persistent ([∗ list] k↦x ∈ [], Φ k x). `````` Robbert Krebbers committed Mar 24, 2017 170 `````` Proof. simpl; apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 171 `````` Global Instance big_sepL_persistent Φ l : `````` Robbert Krebbers committed Oct 25, 2017 172 `````` (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x). `````` Robbert Krebbers committed Mar 24, 2017 173 `````` Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 174 `````` Global Instance big_sepL_persistent_id Ps : `````` Robbert Krebbers committed Oct 25, 2017 175 `````` TCForall Persistent Ps → Persistent ([∗] Ps). `````` Robbert Krebbers committed Mar 24, 2017 176 `````` Proof. induction 1; simpl; apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 177 `````` `````` Robbert Krebbers committed Oct 30, 2017 178 179 180 `````` Global Instance big_sepL_nil_affine Φ : Affine ([∗ list] k↦x ∈ [], Φ k x). Proof. simpl; apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 181 182 183 `````` Global Instance big_sepL_affine Φ l : (∀ k x, Affine (Φ k x)) → Affine ([∗ list] k↦x ∈ l, Φ k x). Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 184 185 `````` Global Instance big_sepL_affine_id Ps : TCForall Affine Ps → Affine ([∗] Ps). Proof. induction 1; simpl; apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 186 ``````End sep_list. `````` Robbert Krebbers committed Aug 24, 2016 187 `````` `````` Robbert Krebbers committed Oct 30, 2017 188 ``````Section sep_list2. `````` Ralf Jung committed Dec 20, 2016 189 190 `````` Context {A : Type}. Implicit Types l : list A. `````` Robbert Krebbers committed Oct 30, 2017 191 `````` Implicit Types Φ Ψ : nat → A → PROP. `````` Ralf Jung committed Dec 20, 2016 192 193 194 `````` (* 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 195 `````` ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) `````` Robbert Krebbers committed Oct 30, 2017 196 `````` ⊣⊢ ([∗ list] k↦x ∈ l1, if l2 !! k is Some y then Φ k (f x y) else emp). `````` Ralf Jung committed Dec 20, 2016 197 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 198 199 200 `````` revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=. - by rewrite big_sepL_emp left_id. - by rewrite IH. `````` Ralf Jung committed Dec 20, 2016 201 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 ``````End sep_list2. Section and_list. Context {A : Type}. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → PROP. Lemma big_andL_nil Φ : ([∧ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. Proof. done. Qed. Lemma big_andL_nil' P Φ : P ⊢ [∧ list] k↦y ∈ nil, Φ k y. Proof. by apply pure_intro. Qed. Lemma big_andL_cons Φ x l : ([∧ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∧ [∧ list] k↦y ∈ l, Φ (S k) y. Proof. by rewrite big_opL_cons. Qed. Lemma big_andL_singleton Φ x : ([∧ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. Proof. by rewrite big_opL_singleton. Qed. Lemma big_andL_app Φ l1 l2 : ([∧ list] k↦y ∈ l1 ++ l2, Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l1, Φ k y) ∧ ([∧ list] k↦y ∈ l2, Φ (length l1 + k) y). Proof. by rewrite big_opL_app. Qed. Lemma big_andL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → ([∧ list] k ↦ y ∈ l, Φ k y) ⊢ [∧ list] k ↦ y ∈ l, Ψ k y. Proof. apply big_opL_forall; apply _. Qed. Lemma big_andL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → ([∧ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∧ list] k ↦ y ∈ l, Ψ k y). Proof. apply big_opL_proper. Qed. Lemma big_andL_submseteq (Φ : A → PROP) l1 l2 : l1 ⊆+ l2 → ([∧ list] y ∈ l2, Φ y) ⊢ [∧ list] y ∈ l1, Φ y. Proof. intros [l ->]%submseteq_Permutation. by rewrite big_andL_app and_elim_l. Qed. Global Instance big_andL_mono' : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢)) (big_opL (@bi_and PROP) (A:=A)). Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and M) (λ _ P, P)). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Lemma big_andL_lookup Φ l i x `{!Absorbing (Φ i x)} : l !! i = Some x → ([∧ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. Proof. intros. rewrite -(take_drop_middle l i x) // big_andL_app /=. rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'. Qed. Lemma big_andL_elem_of (Φ : A → PROP) l x `{!Absorbing (Φ x)} : x ∈ l → ([∧ list] y ∈ l, Φ y) ⊢ Φ x. Proof. intros [i ?]%elem_of_list_lookup; eauto using (big_andL_lookup (λ _, Φ)). Qed. Lemma big_andL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l : ([∧ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l, Φ k (f y)). Proof. by rewrite big_opL_fmap. Qed. Lemma big_andL_andL Φ Ψ l : ([∧ list] k↦x ∈ l, Φ k x ∧ Ψ k x) ⊣⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x). Proof. by rewrite big_opL_opL. Qed. Lemma big_andL_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 and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed. Lemma big_andL_persistently Φ l : `````` Robbert Krebbers committed Mar 04, 2018 274 `````` ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, (Φ k x). `````` Robbert Krebbers committed Oct 30, 2017 275 276 `````` Proof. apply (big_opL_commute _). Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 277 `````` Lemma big_andL_forall `{BiAffine PROP} Φ l : `````` Robbert Krebbers committed Oct 30, 2017 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 `````` ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). Proof. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. apply impl_intro_l, pure_elim_l=> ?; by apply: big_andL_lookup. } revert Φ. induction l as [|x l IH]=> Φ; [by auto using big_andL_nil'|]. rewrite big_andL_cons. apply and_intro. - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. Global Instance big_andL_nil_persistent Φ : Persistent ([∧ list] k↦x ∈ [], Φ k x). Proof. simpl; apply _. Qed. Global Instance big_andL_persistent Φ l : (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x). Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. `````` Robbert Krebbers committed Mar 03, 2018 295 `````` `````` Robbert Krebbers committed Oct 30, 2017 296 ``````End and_list. `````` Robbert Krebbers committed Aug 24, 2016 297 `````` `````` Robbert Krebbers committed Apr 08, 2016 298 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 299 300 301 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Oct 30, 2017 302 `````` Implicit Types Φ Ψ : K → A → PROP. `````` Robbert Krebbers committed Feb 14, 2016 303 `````` `````` Robbert Krebbers committed Oct 30, 2017 304 305 306 307 `````` Lemma big_sepM_mono Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊢ Ψ k x) → ([∗ map] k ↦ x ∈ m, Φ k x) ⊢ [∗ map] k ↦ x ∈ m, Ψ k x. Proof. apply big_opM_forall; apply _ || auto. Qed. `````` Robbert Krebbers committed Jul 22, 2016 308 309 `````` Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed Nov 03, 2016 310 `````` ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). `````` Robbert Krebbers committed Sep 28, 2016 311 `````` Proof. apply big_opM_proper. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 312 `````` Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 : `````` Robbert Krebbers committed Oct 30, 2017 313 314 `````` m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x. Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed. `````` Robbert Krebbers committed Feb 17, 2016 315 `````` `````` Robbert Krebbers committed Mar 24, 2017 316 317 `````` Global Instance big_sepM_mono' : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢)) `````` Robbert Krebbers committed Oct 30, 2017 318 319 `````` (big_opM (@bi_sep PROP) (K:=K) (A:=A)). Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed. `````` Robbert Krebbers committed Feb 17, 2016 320 `````` `````` Robbert Krebbers committed Oct 30, 2017 321 `````` Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp. `````` Robbert Krebbers committed Sep 28, 2016 322 `````` Proof. by rewrite big_opM_empty. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 323 `````` Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x. `````` Robbert Krebbers committed Oct 30, 2017 324 `````` Proof. rewrite big_sepM_empty. apply: affine. Qed. `````` Robbert Krebbers committed May 30, 2016 325 `````` `````` Robbert Krebbers committed May 31, 2016 326 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 327 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 328 `````` ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Mar 24, 2017 329 `````` Proof. apply big_opM_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 330 `````` `````` Robbert Krebbers committed May 31, 2016 331 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 332 `````` m !! i = Some x → `````` Robbert Krebbers committed Nov 03, 2016 333 `````` ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed Mar 24, 2017 334 `````` Proof. apply big_opM_delete. Qed. `````` Robbert Krebbers committed May 30, 2016 335 `````` `````` Robbert Krebbers committed Nov 24, 2016 336 337 338 339 340 341 342 `````` 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 Oct 30, 2017 343 `````` Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} : `````` Robbert Krebbers committed Nov 03, 2016 344 `````` m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. `````` Robbert Krebbers committed Oct 30, 2017 345 `````` Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed. `````` Robbert Krebbers committed Nov 24, 2016 346 `````` `````` Robbert Krebbers committed Oct 30, 2017 347 `````` Lemma big_sepM_lookup_dom (Φ : K → PROP) m i `{!Absorbing (Φ i)} : `````` Robbert Krebbers committed Nov 20, 2016 348 349 `````` 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 350 `````` `````` Robbert Krebbers committed Nov 03, 2016 351 `````` Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Sep 28, 2016 352 `````` Proof. by rewrite big_opM_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 353 `````` `````` Robbert Krebbers committed Oct 30, 2017 354 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → PROP) m : `````` Robbert Krebbers committed Nov 03, 2016 355 `````` ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). `````` Robbert Krebbers committed Sep 28, 2016 356 `````` Proof. by rewrite big_opM_fmap. Qed. `````` Robbert Krebbers committed May 31, 2016 357 `````` `````` Robbert Krebbers committed Dec 02, 2016 358 359 360 `````` 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 Mar 24, 2017 361 `````` Proof. apply big_opM_insert_override. Qed. `````` Robbert Krebbers committed May 31, 2016 362 `````` `````` Robbert Krebbers committed Dec 02, 2016 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 `````` 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 Oct 30, 2017 383 `````` Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → PROP) (f : K → B) m i x b : `````` Robbert Krebbers committed May 31, 2016 384 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 385 386 `````` ([∗ 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 Mar 24, 2017 387 `````` Proof. apply big_opM_fn_insert. Qed. `````` Robbert Krebbers committed Sep 28, 2016 388 `````` `````` Robbert Krebbers committed Oct 30, 2017 389 `````` Lemma big_sepM_fn_insert' (Φ : K → PROP) m i x P : `````` Robbert Krebbers committed May 31, 2016 390 `````` m !! i = None → `````` Robbert Krebbers committed Nov 03, 2016 391 `````` ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). `````` Robbert Krebbers committed Mar 24, 2017 392 `````` Proof. apply big_opM_fn_insert'. Qed. `````` Robbert Krebbers committed May 31, 2016 393 `````` `````` Robbert Krebbers committed Feb 18, 2016 394 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Nov 27, 2016 395 `````` ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) `````` Robbert Krebbers committed Nov 03, 2016 396 `````` ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). `````` Robbert Krebbers committed Mar 24, 2017 397 `````` Proof. apply big_opM_opM. Qed. `````` Robbert Krebbers committed May 31, 2016 398 `````` `````` Robbert Krebbers committed Nov 27, 2016 399 400 401 `````` 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). `````` Robbert Krebbers committed Oct 30, 2017 402 `````` Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed. `````` Robbert Krebbers committed Sep 28, 2016 403 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 404 `````` Lemma big_sepM_persistently `{BiAffine PROP} Φ m : `````` Robbert Krebbers committed Mar 04, 2018 405 `````` ( ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, (Φ k x)). `````` Robbert Krebbers committed Sep 28, 2016 406 `````` Proof. apply (big_opM_commute _). Qed. `````` Robbert Krebbers committed May 31, 2016 407 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 408 `````` Lemma big_sepM_forall `{BiAffine PROP} Φ m : `````` Robbert Krebbers committed Oct 25, 2017 409 `````` (∀ k x, Persistent (Φ k x)) → `````` Ralf Jung committed Nov 22, 2016 410 `````` ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). `````` Robbert Krebbers committed May 31, 2016 411 412 413 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. `````` Robbert Krebbers committed Oct 30, 2017 414 415 `````` apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. } induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'. `````` Robbert Krebbers committed Oct 30, 2017 416 `````` rewrite big_sepM_insert // -persistent_and_sep. apply and_intro. `````` Robbert Krebbers committed Sep 28, 2016 417 `````` - rewrite (forall_elim i) (forall_elim x) lookup_insert. `````` Robbert Krebbers committed Nov 21, 2016 418 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 419 `````` - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. `````` Robbert Krebbers committed Sep 28, 2016 420 421 `````` apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. `````` Robbert Krebbers committed Nov 21, 2016 422 `````` by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 423 424 425 `````` Qed. Lemma big_sepM_impl Φ Ψ m : `````` Robbert Krebbers committed Oct 30, 2017 426 `````` ([∗ map] k↦x ∈ m, Φ k x) -∗ `````` Jacques-Henri Jourdan committed Nov 02, 2017 427 `````` □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗ `````` Robbert Krebbers committed Oct 30, 2017 428 `````` [∗ map] k↦x ∈ m, Ψ k x. `````` Robbert Krebbers committed May 31, 2016 429 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 430 431 `````` apply wand_intro_l. induction m as [|i x m ? IH] using map_ind. { by rewrite sep_elim_r. } `````` 432 `````` rewrite !big_sepM_insert // intuitionistically_sep_dup. `````` Jacques-Henri Jourdan committed Nov 02, 2017 433 `````` rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono. `````` Robbert Krebbers committed Oct 30, 2017 434 `````` - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //. `````` 435 `````` by rewrite True_impl intuitionistically_elim wand_elim_l. `````` Robbert Krebbers committed Oct 30, 2017 436 `````` - rewrite comm -IH /=. `````` Jacques-Henri Jourdan committed Nov 02, 2017 437 `````` apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k. `````` Robbert Krebbers committed Oct 30, 2017 438 439 440 `````` apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. rewrite lookup_insert_ne; last by intros ?; simplify_map_eq. by rewrite pure_True // True_impl. `````` Robbert Krebbers committed May 31, 2016 441 `````` Qed. `````` Robbert Krebbers committed Aug 24, 2016 442 `````` `````` Robbert Krebbers committed Oct 30, 2017 443 `````` Global Instance big_sepM_empty_persistent Φ : `````` Robbert Krebbers committed Oct 25, 2017 444 `````` Persistent ([∗ map] k↦x ∈ ∅, Φ k x). `````` Robbert Krebbers committed Sep 28, 2016 445 `````` Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 446 `````` Global Instance big_sepM_persistent Φ m : `````` Robbert Krebbers committed Oct 25, 2017 447 `````` (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Mar 24, 2017 448 `````` Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 449 `````` `````` Robbert Krebbers committed Oct 30, 2017 450 451 452 `````` Global Instance big_sepM_empty_affine Φ : Affine ([∗ map] k↦x ∈ ∅, Φ k x). Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 453 454 `````` Global Instance big_sepM_affine Φ m : (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x). `````` Robbert Krebbers committed Oct 30, 2017 455 `````` Proof. intros. apply big_sepL_affine=> _ [??]; apply _. Qed. `````` Robbert Krebbers committed Feb 17, 2016 456 457 ``````End gmap. `````` Robbert Krebbers committed Apr 08, 2016 458 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 459 460 461 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Oct 30, 2017 462 `````` Implicit Types Φ : A → PROP. `````` Robbert Krebbers committed Feb 17, 2016 463 `````` `````` Robbert Krebbers committed Oct 30, 2017 464 465 466 467 `````` Lemma big_sepS_mono Φ Ψ X : (∀ x, x ∈ X → Φ x ⊢ Ψ x) → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. Proof. intros. apply big_opS_forall; apply _ || auto. Qed. `````` Robbert Krebbers committed Oct 03, 2016 468 469 `````` Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → `````` Robbert Krebbers committed Nov 03, 2016 470 `````` ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). `````` Robbert Krebbers committed Mar 24, 2017 471 `````` Proof. apply big_opS_proper. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 472 `````` Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y : `````` Robbert Krebbers committed Oct 30, 2017 473 474 `````` Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x. Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed. `````` Robbert Krebbers committed Sep 28, 2016 475 `````` `````` Robbert Krebbers committed Mar 24, 2017 476 `````` Global Instance big_sepS_mono' : `````` Robbert Krebbers committed Oct 30, 2017 477 478 `````` Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)). Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed. `````` Robbert Krebbers committed Sep 28, 2016 479 `````` `````` Robbert Krebbers committed Oct 30, 2017 480 `````` Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp. `````` Robbert Krebbers committed Sep 28, 2016 481 `````` Proof. by rewrite big_opS_empty. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 482 `````` Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x. `````` Robbert Krebbers committed Oct 30, 2017 483 `````` Proof. rewrite big_sepS_empty. apply: affine. Qed. `````` Robbert Krebbers committed Apr 11, 2016 484 `````` `````` Robbert Krebbers committed Feb 18, 2016 485 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 486 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Mar 24, 2017 487 `````` Proof. apply big_opS_insert. Qed. `````` Robbert Krebbers committed Sep 28, 2016 488 `````` `````` Robbert Krebbers committed Oct 30, 2017 489 `````` Lemma big_sepS_fn_insert {B} (Ψ : A → B → PROP) f X x b : `````` Robbert Krebbers committed Apr 11, 2016 490 `````` x ∉ X → `````` Robbert Krebbers committed Nov 03, 2016 491 492 `````` ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). `````` Robbert Krebbers committed Mar 24, 2017 493 `````` Proof. apply big_opS_fn_insert. Qed. `````` Robbert Krebbers committed Sep 28, 2016 494 `````` `````` Robbert Krebbers committed May 30, 2016 495 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed Nov 03, 2016 496 `````` x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Mar 24, 2017 497 `````` Proof. apply big_opS_fn_insert'. Qed. `````` Robbert Krebbers committed Apr 11, 2016 498 `````` `````` Robbert Krebbers committed Nov 21, 2016 499 `````` Lemma big_sepS_union Φ X Y : `````` Jacques-Henri Jourdan committed Nov 03, 2017 500 `````` X ## Y → `````` Robbert Krebbers committed Nov 21, 2016 501 `````` ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y). `````` Robbert Krebbers committed Mar 24, 2017 502 `````` Proof. apply big_opS_union. Qed. `````` Robbert Krebbers committed Nov 21, 2016 503 `````` `````` Robbert Krebbers committed Feb 18, 2016 504 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Nov 03, 2016 505 `````` x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Mar 24, 2017 506 `````` Proof. apply big_opS_delete. Qed. `````` Robbert Krebbers committed Apr 11, 2016 507 `````` `````` Robbert Krebbers committed Oct 30, 2017 508 509 `````` Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. `````` Robbert Krebbers committed Oct 30, 2017 510 `````` Proof. intros. rewrite big_sepS_delete //. by rewrite sep_elim_l. Qed. `````` Robbert Krebbers committed May 31, 2016 511 `````` `````` Robbert Krebbers committed Nov 24, 2016 512 513 514 515 516 517 518 `````` 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 519 `````` Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Mar 24, 2017 520 `````` Proof. apply big_opS_singleton. Qed. `````` Ralf Jung committed Feb 17, 2016 521 `````` `````` Robbert Krebbers committed Oct 30, 2017 522 523 524 `````` Lemma big_sepS_filter' (P : A → Prop) `{∀ x, Decision (P x)} Φ X : ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, if decide (P y) then Φ y else emp). `````` Robbert Krebbers committed Nov 21, 2016 525 526 527 528 529 530 `````` 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. `````` Robbert Krebbers committed Oct 30, 2017 531 `````` by rewrite decide_True // IH. `````` Robbert Krebbers committed Nov 21, 2016 532 `````` - rewrite filter_union_L filter_singleton_not_L // left_id_L. `````` Robbert Krebbers committed Oct 30, 2017 533 `````` by rewrite !big_sepS_insert // decide_False // IH left_id. `````` Robbert Krebbers committed Nov 21, 2016 534 535 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 536 `````` Lemma big_sepS_filter_acc' (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y : `````` Robbert Krebbers committed Nov 29, 2016 537 538 `````` (∀ y, y ∈ Y → P y → y ∈ X) → ([∗ set] y ∈ X, Φ y) -∗ `````` Robbert Krebbers committed Oct 30, 2017 539 540 `````` ([∗ set] y ∈ Y, if decide (P y) then Φ y else emp) ∗ (([∗ set] y ∈ Y, if decide (P y) then Φ y else emp) -∗ [∗ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Nov 29, 2016 541 542 543 `````` Proof. intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X)) as (Z&->&?); first set_solver. `````` Robbert Krebbers committed Oct 30, 2017 544 545 `````` rewrite big_sepS_union // big_sepS_filter'. by apply sep_mono_r, wand_intro_l. `````` Robbert Krebbers committed Nov 29, 2016 546 547 `````` Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 548 `````` Lemma big_sepS_filter `{BiAffine PROP} `````` Robbert Krebbers committed Oct 30, 2017 549 550 551 552 `````` (P : A → Prop) `{∀ x, Decision (P x)} Φ X : ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y). Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 553 `````` Lemma big_sepS_filter_acc `{BiAffine PROP} `````` Robbert Krebbers committed Oct 30, 2017 554 555 556 557 558 559 560 `````` (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. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed. `````` Robbert Krebbers committed Feb 18, 2016 561 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Nov 03, 2016 562 `````` ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Mar 24, 2017 563 `````` Proof. apply big_opS_opS. Qed. `````` Robbert Krebbers committed May 31, 2016 564 `````` `````` Robbert Krebbers committed Nov 27, 2016 565 566 `````` Lemma big_sepS_and Φ Ψ X : ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y). `````` Robbert Krebbers committed Oct 30, 2017 567 `````` Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed. `````` Robbert Krebbers committed Sep 28, 2016 568 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 569 `````` Lemma big_sepS_persistently `{BiAffine PROP} Φ X : `````` Robbert Krebbers committed Mar 04, 2018 570 `````` ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, (Φ y). `````` Robbert Krebbers committed Nov 27, 2016 571 572 `````` Proof. apply (big_opS_commute _). Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 573 `````` Lemma big_sepS_forall `{BiAffine PROP} Φ X : `````` Robbert Krebbers committed Oct 25, 2017 574 `````` (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). `````` Robbert Krebbers committed May 31, 2016 575 576 577 `````` Proof. intros. apply (anti_symm _). { apply forall_intro=> x. `````` Robbert Krebbers committed Oct 30, 2017 578 579 `````` apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. } induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'. `````` Robbert Krebbers committed Oct 30, 2017 580 `````` rewrite big_sepS_insert // -persistent_and_sep. apply and_intro. `````` Robbert Krebbers committed Nov 21, 2016 581 `````` - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed Sep 28, 2016 582 `````` - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. `````` Robbert Krebbers committed Nov 21, 2016 583 `````` by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 584 585 586 `````` Qed. Lemma big_sepS_impl Φ Ψ X : `````` Robbert Krebbers committed Oct 30, 2017 587 `````` ([∗ set] x ∈ X, Φ x) -∗ `````` Jacques-Henri Jourdan committed Nov 02, 2017 588 `````` □ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗ `````` Robbert Krebbers committed Oct 30, 2017 589 `````` [∗ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 590 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 591 592 `````` apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L. { by rewrite sep_elim_r. } `````` 593 `````` rewrite !big_sepS_insert // intuitionistically_sep_dup. `````` Jacques-Henri Jourdan committed Nov 02, 2017 594 `````` rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono. `````` Robbert Krebbers committed Oct 30, 2017 595 `````` - rewrite (forall_elim x) pure_True; last set_solver. `````` 596 `````` by rewrite True_impl intuitionistically_elim wand_elim_l. `````` Jacques-Henri Jourdan committed Nov 02, 2017 597 `````` - rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono. `````` Robbert Krebbers committed Oct 30, 2017 598 599 `````` apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?. by rewrite pure_True ?True_impl; last set_solver. `````` Robbert Krebbers committed May 31, 2016 600 `````` Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 601 `````` `````` Robbert Krebbers committed Oct 30, 2017 602 `````` Global Instance big_sepS_empty_persistent Φ : `````` Robbert Krebbers committed Oct 30, 2017 603 `````` Persistent ([∗ set] x ∈ ∅, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 604 `````` Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Robbert Krebbers committed Oct 30, 2017 605 `````` Global Instance big_sepS_persistent Φ X : `````` Robbert Krebbers committed Oct 25, 2017 606 `````` (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x). `````` Robbert Krebbers committed Sep 28, 2016 607 `````` Proof. rewrite /big_opS. apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 608 `````` `````` Robbert Krebbers committed Oct 30, 2017 609 610 `````` Global Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x). Proof. rewrite /big_opS elements_empty. apply _. Qed. `````` Aleš Bizjak committed Oct 30, 2017 611 612 613 `````` Global Instance big_sepS_affine Φ X : (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x). Proof. rewrite /big_opS. apply _. Qed. `````` Robbert Krebbers committed Aug 24, 2016 614 ``````End gset. `````` Robbert Krebbers committed Nov 19, 2016 615 `````` `````` Robbert Krebbers committed Oct 30, 2017 616 ``````Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) : `````` Robbert Krebbers committed Dec 02, 2016 617 `````` ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k). `````` Robbert Krebbers committed Mar 24, 2017 618 ``````Proof. apply big_opM_dom. Qed. `````` Robbert Krebbers committed Dec 02, 2016 619 `````` `````` Robbert Krebbers committed Nov 19, 2016 620 621 622 623 ``````(** ** Big ops over finite multisets *) Section gmultiset. Context `{Countable A}. Implicit Types X : gmultiset A. `````` Robbert Krebbers committed Oct 30, 2017 624 `````` Implicit Types Φ : A → PROP. `````` Robbert Krebbers committed Nov 19, 2016 625 `````` `````` Robbert Krebbers committed Oct 30, 2017 626 627 628 629 `````` Lemma big_sepMS_mono Φ Ψ X : (∀ x, x ∈ X → Φ x ⊢ Ψ x) → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ X, Ψ x. Proof. intros. apply big_opMS_forall; apply _ || auto. Qed. `````` Robbert Krebbers committed Nov 19, 2016 630 631 632 `````` Lemma big_sepMS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x). `````` Robbert Krebbers committed Mar 24, 2017 633 `````` Proof. apply big_opMS_proper. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 634 `````` Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y : `````` Robbert Krebbers committed Oct 30, 2017 635 636 `````` Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x. Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed. `````` Robbert Krebbers committed Nov 19, 2016 637 `````` `````` Robbert Krebbers committed Mar 24, 2017 638 `````` Global Instance big_sepMS_mono' : `````` Robbert Krebbers committed Oct 30, 2017 639 640 `````` Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@bi_sep PROP) (A:=A)). Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed. `````` Robbert Krebbers committed Nov 19, 2016 641 `````` ``````