derived_laws_bi.v 65.6 KB
 Jacques-Henri Jourdan committed Dec 04, 2017 1 ``````From iris.bi Require Export derived_connectives. `````` Robbert Krebbers committed Oct 30, 2017 2 3 ``````From iris.algebra Require Import monoid. `````` Ralf Jung committed Mar 22, 2018 4 5 6 7 8 9 10 ``````(** Naming schema for lemmas about modalities: M1_into_M2: M1 P ⊢ M2 P M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P) *) `````` Robbert Krebbers committed Oct 30, 2017 11 12 13 14 15 16 17 18 19 ``````Module bi. Import interface.bi. Section bi_derived. Context {PROP : bi}. Implicit Types φ : Prop. Implicit Types P Q R : PROP. Implicit Types Ps : list PROP. Implicit Types A : Type. `````` Tej Chajed committed Nov 29, 2018 20 ``````Hint Extern 100 (NonExpansive _) => solve_proper : core. `````` Robbert Krebbers committed Oct 30, 2017 21 22 `````` (* Force implicit argument PROP *) `````` Ralf Jung committed Apr 05, 2018 23 24 ``````Notation "P ⊢ Q" := (P ⊢@{PROP} Q). Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q). `````` Robbert Krebbers committed Oct 30, 2017 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 `````` (* Derived stuff about the entailment *) Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP). Proof. intros P Q ??. by apply equiv_spec. Qed. Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q). Proof. apply equiv_spec. Qed. Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q). Proof. apply equiv_spec. Qed. Global Instance entails_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation PROP). Proof. move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split=>?. - by trans P1; [|trans Q1]. - by trans P2; [|trans Q2]. Qed. Lemma entails_equiv_l P Q R : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R). Proof. by intros ->. Qed. Lemma entails_equiv_r P Q R : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R). Proof. by intros ? <-. Qed. `````` Ralf Jung committed Mar 19, 2018 44 ``````Global Instance bi_emp_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_emp_valid PROP). `````` Robbert Krebbers committed Oct 30, 2017 45 ``````Proof. solve_proper. Qed. `````` Ralf Jung committed Mar 19, 2018 46 ``````Global Instance bi_emp_valid_mono : Proper ((⊢) ==> impl) (@bi_emp_valid PROP). `````` Robbert Krebbers committed Oct 30, 2017 47 ``````Proof. solve_proper. Qed. `````` Ralf Jung committed Mar 19, 2018 48 49 ``````Global Instance bi_emp_valid_flip_mono : Proper (flip (⊢) ==> flip impl) (@bi_emp_valid PROP). `````` Robbert Krebbers committed Oct 30, 2017 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 ``````Proof. solve_proper. Qed. (* Propers *) Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@bi_pure PROP) | 0. Proof. intros φ1 φ2 Hφ. apply equiv_dist=> n. by apply pure_ne. Qed. Global Instance and_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_and PROP) := ne_proper_2 _. Global Instance or_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_or PROP) := ne_proper_2 _. Global Instance impl_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_impl PROP) := ne_proper_2 _. Global Instance sep_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_sep PROP) := ne_proper_2 _. Global Instance wand_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand PROP) := ne_proper_2 _. Global Instance forall_proper A : Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_forall PROP A). Proof. intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply forall_ne=> x. apply equiv_dist, HΦ. Qed. Global Instance exist_proper A : Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_exist PROP A). Proof. intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply exist_ne=> x. apply equiv_dist, HΦ. Qed. Global Instance persistently_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP) := ne_proper _. (* Derived logical stuff *) Lemma and_elim_l' P Q R : (P ⊢ R) → P ∧ Q ⊢ R. Proof. by rewrite and_elim_l. Qed. Lemma and_elim_r' P Q R : (Q ⊢ R) → P ∧ Q ⊢ R. Proof. by rewrite and_elim_r. Qed. Lemma or_intro_l' P Q R : (P ⊢ Q) → P ⊢ Q ∨ R. Proof. intros ->; apply or_intro_l. Qed. Lemma or_intro_r' P Q R : (P ⊢ R) → P ⊢ Q ∨ R. Proof. intros ->; apply or_intro_r. Qed. Lemma exist_intro' {A} P (Ψ : A → PROP) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a. Proof. intros ->; apply exist_intro. Qed. Lemma forall_elim' {A} P (Ψ : A → PROP) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a. Proof. move=> HP a. by rewrite HP forall_elim. Qed. `````` Tej Chajed committed Nov 29, 2018 94 95 96 ``````Hint Resolve pure_intro forall_intro : core. Hint Resolve or_elim or_intro_l' or_intro_r' : core. Hint Resolve and_intro and_elim_l' and_elim_r' : core. `````` Robbert Krebbers committed Oct 30, 2017 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R. Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed. Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R. Proof. intros. rewrite -(impl_elim_l' P Q R); auto. Qed. Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R. Proof. intros; apply impl_elim with P; auto. Qed. Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q. Proof. by apply impl_elim_l'. Qed. Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q. Proof. by apply impl_elim_r'. Qed. Lemma False_elim P : False ⊢ P. Proof. by apply (pure_elim' False). Qed. Lemma True_intro P : P ⊢ True. Proof. by apply pure_intro. Qed. `````` Tej Chajed committed Nov 29, 2018 113 ``````Hint Immediate False_elim : core. `````` Robbert Krebbers committed Oct 30, 2017 114 `````` `````` Ralf Jung committed May 03, 2018 115 116 117 118 119 120 121 122 123 ``````Lemma entails_eq_True P Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I). Proof. split=>EQ. - apply bi.equiv_spec; split; [by apply True_intro|]. apply impl_intro_r. rewrite and_elim_r //. - trans (P ∧ True)%I. + apply and_intro; first done. by apply pure_intro. + rewrite -EQ impl_elim_r. done. Qed. `````` Ralf Jung committed May 03, 2018 124 ``````Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)). `````` Robbert Krebbers committed May 07, 2018 125 ``````Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed. `````` Ralf Jung committed May 03, 2018 126 `````` `````` Robbert Krebbers committed Oct 30, 2017 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 ``````Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'. Proof. auto. Qed. Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'. Proof. by intros; apply and_mono. Qed. Lemma and_mono_r P P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'. Proof. by apply and_mono. Qed. Lemma or_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'. Proof. auto. Qed. Lemma or_mono_l P P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'. Proof. by intros; apply or_mono. Qed. Lemma or_mono_r P P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'. Proof. by apply or_mono. Qed. Lemma impl_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P → P') ⊢ Q → Q'. Proof. intros HP HQ'; apply impl_intro_l; rewrite -HQ'. apply impl_elim with P; eauto. Qed. Lemma forall_mono {A} (Φ Ψ : A → PROP) : (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ ∀ a, Ψ a. Proof. intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim. Qed. Lemma exist_mono {A} (Φ Ψ : A → PROP) : (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ ∃ a, Ψ a. Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed. Global Instance and_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_and PROP). Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed. Global Instance and_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_and PROP). Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed. Global Instance or_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_or PROP). Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed. Global Instance or_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_or PROP). Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed. Global Instance impl_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_impl PROP). Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed. Global Instance impl_flip_mono' : Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_impl PROP). Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed. Global Instance forall_mono' A : Proper (pointwise_relation _ (⊢) ==> (⊢)) (@bi_forall PROP A). Proof. intros P1 P2; apply forall_mono. Qed. Global Instance forall_flip_mono' A : Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_forall PROP A). Proof. intros P1 P2; apply forall_mono. Qed. Global Instance exist_mono' A : Proper (pointwise_relation _ ((⊢)) ==> (⊢)) (@bi_exist PROP A). Proof. intros P1 P2; apply exist_mono. Qed. Global Instance exist_flip_mono' A : Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_exist PROP A). Proof. intros P1 P2; apply exist_mono. Qed. Global Instance and_idem : IdemP (⊣⊢) (@bi_and PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_idem : IdemP (⊣⊢) (@bi_or PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_comm : Comm (⊣⊢) (@bi_and PROP). Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed. Global Instance True_and : LeftId (⊣⊢) True%I (@bi_and PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_True : RightId (⊣⊢) True%I (@bi_and PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@bi_and PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_False : RightAbsorb (⊣⊢) False%I (@bi_and PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@bi_or PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_True : RightAbsorb (⊣⊢) True%I (@bi_or PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance False_or : LeftId (⊣⊢) False%I (@bi_or PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_False : RightId (⊣⊢) False%I (@bi_or PROP). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_assoc : Assoc (⊣⊢) (@bi_and PROP). Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed. Global Instance or_comm : Comm (⊣⊢) (@bi_or PROP). Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed. Global Instance or_assoc : Assoc (⊣⊢) (@bi_or PROP). Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed. Global Instance True_impl : LeftId (⊣⊢) True%I (@bi_impl PROP). Proof. intros P; apply (anti_symm (⊢)). - by rewrite -(left_id True%I (∧)%I (_ → _)%I) impl_elim_r. - by apply impl_intro_l; rewrite left_id. Qed. Lemma False_impl P : (False → P) ⊣⊢ True. Proof. apply (anti_symm (⊢)); [by auto|]. apply impl_intro_l. rewrite left_absorb. auto. Qed. `````` Jacques-Henri Jourdan committed Dec 11, 2017 225 ``````Lemma exist_impl_forall {A} P (Ψ : A → PROP) : `````` Robbert Krebbers committed Oct 30, 2017 226 227 228 229 230 231 232 `````` ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P. Proof. apply equiv_spec; split. - apply forall_intro=>x. by rewrite -exist_intro. - apply impl_intro_r, impl_elim_r', exist_elim=>x. apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r. Qed. `````` Ralf Jung committed Apr 26, 2018 233 234 235 236 237 238 239 240 241 242 243 244 245 246 ``````Lemma forall_unit (Ψ : unit → PROP) : (∀ x, Ψ x) ⊣⊢ Ψ (). Proof. apply (anti_symm (⊢)). - rewrite (forall_elim ()) //. - apply forall_intro=>[[]]. done. Qed. Lemma exist_unit (Ψ : unit → PROP) : (∃ x, Ψ x) ⊣⊢ Ψ (). Proof. apply (anti_symm (⊢)). - apply exist_elim=>[[]]. done. - rewrite -(exist_intro ()). done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 247 `````` `````` Dan Frumin committed Apr 07, 2019 248 249 250 251 252 253 254 ``````Lemma impl_curry P Q R : (P → Q → R) ⊣⊢ (P ∧ Q → R). Proof. apply (anti_symm _). - apply impl_intro_l. by rewrite (comm _ P) -and_assoc !impl_elim_r. - do 2 apply impl_intro_l. by rewrite assoc (comm _ Q) impl_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 ``````Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R). Proof. apply (anti_symm (⊢)); first auto. do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto. Qed. Lemma or_and_r P Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R). Proof. by rewrite -!(comm _ R) or_and_l. Qed. Lemma and_or_l P Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R. Proof. apply (anti_symm (⊢)); last auto. apply impl_elim_r', or_elim; apply impl_intro_l; auto. Qed. Lemma and_or_r P Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R. Proof. by rewrite -!(comm _ R) and_or_l. Qed. Lemma and_exist_l {A} P (Ψ : A → PROP) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a. Proof. apply (anti_symm (⊢)). - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l. by rewrite -(exist_intro a). - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l. by rewrite -(exist_intro a) and_elim_r. Qed. Lemma and_exist_r {A} P (Φ: A → PROP) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a, Φ a ∧ P. Proof. rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm. Qed. Lemma or_exist {A} (Φ Ψ : A → PROP) : (∃ a, Φ a ∨ Ψ a) ⊣⊢ (∃ a, Φ a) ∨ (∃ a, Ψ a). Proof. apply (anti_symm (⊢)). - apply exist_elim=> a. by rewrite -!(exist_intro a). - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto. Qed. Lemma and_alt P Q : P ∧ Q ⊣⊢ ∀ b : bool, if b then P else Q. Proof. apply (anti_symm _); first apply forall_intro=> -[]; auto. by apply and_intro; [rewrite (forall_elim true)|rewrite (forall_elim false)]. Qed. Lemma or_alt P Q : P ∨ Q ⊣⊢ ∃ b : bool, if b then P else Q. Proof. apply (anti_symm _); last apply exist_elim=> -[]; auto. by apply or_elim; [rewrite -(exist_intro true)|rewrite -(exist_intro false)]. Qed. Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q). Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed. Global Instance iff_ne : NonExpansive2 (@bi_iff PROP). Proof. unfold bi_iff; solve_proper. Qed. Global Instance iff_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_iff PROP) := ne_proper_2 _. Lemma iff_refl Q P : Q ⊢ P ↔ P. Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed. (* BI Stuff *) `````` Tej Chajed committed Nov 29, 2018 313 ``````Hint Resolve sep_mono : core. `````` Robbert Krebbers committed Oct 30, 2017 314 315 316 317 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 346 347 348 349 350 351 352 353 354 ``````Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'. Proof. by intros; apply sep_mono. Qed. Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'. Proof. by apply sep_mono. Qed. Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_sep PROP). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. Global Instance sep_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_sep PROP). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -∗ P') ⊢ Q -∗ Q'. Proof. intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'. Qed. Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_wand PROP). Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed. Global Instance wand_flip_mono' : Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_wand PROP). Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed. Global Instance sep_comm : Comm (⊣⊢) (@bi_sep PROP). Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed. Global Instance sep_assoc : Assoc (⊣⊢) (@bi_sep PROP). Proof. intros P Q R; apply (anti_symm _); auto using sep_assoc'. by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'. Qed. Global Instance emp_sep : LeftId (⊣⊢) emp%I (@bi_sep PROP). Proof. intros P; apply (anti_symm _); auto using emp_sep_1, emp_sep_2. Qed. Global Instance sep_emp : RightId (⊣⊢) emp%I (@bi_sep PROP). Proof. by intros P; rewrite comm left_id. Qed. Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@bi_sep PROP). Proof. intros P; apply (anti_symm _); auto using wand_elim_l'. Qed. Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@bi_sep PROP). Proof. intros P. by rewrite comm left_absorb. Qed. Lemma True_sep_2 P : P ⊢ True ∗ P. Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed. Lemma sep_True_2 P : P ⊢ P ∗ True. Proof. by rewrite comm -True_sep_2. Qed. `````` Ralf Jung committed Mar 19, 2018 355 ``````Lemma sep_intro_emp_valid_l P Q R : P → (R ⊢ Q) → R ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 356 ``````Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed. `````` Ralf Jung committed Mar 19, 2018 357 358 359 ``````Lemma sep_intro_emp_valid_r P Q R : (R ⊢ P) → Q → R ⊢ P ∗ Q. Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed. Lemma sep_elim_emp_valid_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 30, 2017 360 ``````Proof. intros <- <-. by rewrite left_id. Qed. `````` Ralf Jung committed Mar 19, 2018 361 ``````Lemma sep_elim_emp_valid_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 30, 2017 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 ``````Proof. intros <- <-. by rewrite right_id. Qed. Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R. Proof. rewrite comm; apply wand_intro_r. Qed. Lemma wand_elim_l P Q : (P -∗ Q) ∗ P ⊢ Q. Proof. by apply wand_elim_l'. Qed. Lemma wand_elim_r P Q : P ∗ (P -∗ Q) ⊢ Q. Proof. rewrite (comm _ P); apply wand_elim_l. Qed. Lemma wand_elim_r' P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R. Proof. intros ->; apply wand_elim_r. Qed. Lemma wand_apply P Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R. Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed. Lemma wand_frame_l P Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R. Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed. Lemma wand_frame_r P Q R : (Q -∗ R) ⊢ Q ∗ P -∗ R ∗ P. Proof. apply wand_intro_l. rewrite ![(_ ∗ P)%I]comm -assoc. apply sep_mono_r, wand_elim_r. Qed. `````` Ralf Jung committed Jun 10, 2018 382 ``````Global Instance emp_wand : LeftId (⊣⊢) emp%I (@bi_wand PROP). `````` Robbert Krebbers committed Oct 30, 2017 383 ``````Proof. `````` Ralf Jung committed Jun 10, 2018 384 `````` intros P. apply (anti_symm _). `````` Robbert Krebbers committed Oct 30, 2017 385 386 387 `````` - by rewrite -[(emp -∗ P)%I]left_id wand_elim_r. - apply wand_intro_l. by rewrite left_id. Qed. `````` Ralf Jung committed Jun 10, 2018 388 `````` `````` Robbert Krebbers committed Oct 30, 2017 389 390 391 392 393 394 ``````Lemma False_wand P : (False -∗ P) ⊣⊢ True. Proof. apply (anti_symm (⊢)); [by auto|]. apply wand_intro_l. rewrite left_absorb. auto. Qed. `````` Robbert Krebbers committed Oct 27, 2018 395 396 397 ``````Lemma wand_trans P Q R : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R). Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 ``````Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). Proof. apply (anti_symm _). - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r. - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r. Qed. Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R). Proof. auto. Qed. Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R). Proof. auto. Qed. Lemma sep_or_l P Q R : P ∗ (Q ∨ R) ⊣⊢ (P ∗ Q) ∨ (P ∗ R). Proof. apply (anti_symm (⊢)); last by eauto 8. apply wand_elim_r', or_elim; apply wand_intro_l; auto. Qed. Lemma sep_or_r P Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R). Proof. by rewrite -!(comm _ R) sep_or_l. Qed. Lemma sep_exist_l {A} P (Ψ : A → PROP) : P ∗ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∗ Ψ a. Proof. intros; apply (anti_symm (⊢)). - apply wand_elim_r', exist_elim=>a. apply wand_intro_l. by rewrite -(exist_intro a). - apply exist_elim=> a; apply sep_mono; auto using exist_intro. Qed. Lemma sep_exist_r {A} (Φ: A → PROP) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q. Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed. Lemma sep_forall_l {A} P (Ψ : A → PROP) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. Lemma sep_forall_r {A} (Φ : A → PROP) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP). Proof. solve_proper. Qed. Global Instance wand_iff_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand_iff PROP) := ne_proper_2 _. Lemma wand_iff_refl P : emp ⊢ P ∗-∗ P. Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed. Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q. `````` Ralf Jung committed Jun 10, 2018 439 ``````Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed. `````` Robbert Krebbers committed Oct 30, 2017 440 441 ``````Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I. Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed. `````` Robbert Krebbers committed Oct 27, 2018 442 443 444 ``````(* A version that works with rewrite, in which bi_emp_valid is unfolded. *) Lemma entails_wand' P Q : (P ⊢ Q) → emp ⊢ (P -∗ Q). Proof. apply entails_wand. Qed. `````` Robbert Krebbers committed Oct 30, 2017 445 446 447 448 449 450 `````` Lemma equiv_wand_iff P Q : (P ⊣⊢ Q) → (P ∗-∗ Q)%I. Proof. intros ->; apply wand_iff_refl. Qed. Lemma wand_iff_equiv P Q : (P ∗-∗ Q)%I → (P ⊣⊢ Q). Proof. intros HPQ; apply (anti_symm (⊢)); `````` Ralf Jung committed Mar 19, 2018 451 `````` apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto. `````` Robbert Krebbers committed Oct 30, 2017 452 453 454 455 456 457 458 459 460 461 462 463 ``````Qed. Lemma entails_impl P Q : (P ⊢ Q) → (P → Q)%I. Proof. intros ->. apply impl_intro_l. auto. Qed. Lemma impl_entails P Q `{!Affine P} : (P → Q)%I → P ⊢ Q. Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed. Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I. Proof. intros ->; apply iff_refl. Qed. Lemma iff_equiv P Q `{!Affine P, !Affine Q} : (P ↔ Q)%I → (P ⊣⊢ Q). Proof. intros HPQ; apply (anti_symm (⊢)); `````` Ralf Jung committed Mar 19, 2018 464 `````` apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto. `````` Robbert Krebbers committed Oct 30, 2017 465 466 ``````Qed. `````` Ralf Jung committed Jun 04, 2018 467 468 469 470 471 472 473 474 ``````Lemma and_parallel P1 P2 Q1 Q2 : (P1 ∧ P2) -∗ ((P1 -∗ Q1) ∧ (P2 -∗ Q2)) -∗ Q1 ∧ Q2. Proof. apply wand_intro_r, and_intro. - rewrite !and_elim_l wand_elim_r. done. - rewrite !and_elim_r wand_elim_r. done. Qed. `````` Ralf Jung committed Jul 02, 2018 475 476 477 478 ``````Lemma wandM_sound (mP : option PROP) Q : (mP -∗? Q) ⊣⊢ (default emp mP -∗ Q). Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed. `````` Robbert Krebbers committed Oct 30, 2017 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 ``````(* Pure stuff *) Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R. Proof. intros HQ HQR. rewrite -(idemp (∧)%I Q) {1}HQ. apply impl_elim_l', pure_elim'=> ?. apply impl_intro_l. rewrite and_elim_l; auto. Qed. Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝. Proof. auto using pure_elim', pure_intro. Qed. Global Instance pure_mono' : Proper (impl ==> (⊢)) (@bi_pure PROP). Proof. intros φ1 φ2; apply pure_mono. Qed. Global Instance pure_flip_mono : Proper (flip impl ==> flip (⊢)) (@bi_pure PROP). Proof. intros φ1 φ2; apply pure_mono. Qed. Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝. Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed. Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∧ Q ⊢ R. Proof. intros; apply pure_elim with φ; eauto. Qed. Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ⌜φ⌝ ⊢ R. Proof. intros; apply pure_elim with φ; eauto. Qed. Lemma pure_True (φ : Prop) : φ → ⌜φ⌝ ⊣⊢ True. Proof. intros; apply (anti_symm _); auto. Qed. Lemma pure_False (φ : Prop) : ¬φ → ⌜φ⌝ ⊣⊢ False. Proof. intros; apply (anti_symm _); eauto using pure_mono. Qed. Lemma pure_and φ1 φ2 : ⌜φ1 ∧ φ2⌝ ⊣⊢ ⌜φ1⌝ ∧ ⌜φ2⌝. Proof. apply (anti_symm _). - apply and_intro; apply pure_mono; tauto. - eapply (pure_elim φ1); [auto|]=> ?. rewrite and_elim_r. auto using pure_mono. Qed. Lemma pure_or φ1 φ2 : ⌜φ1 ∨ φ2⌝ ⊣⊢ ⌜φ1⌝ ∨ ⌜φ2⌝. Proof. apply (anti_symm _). - eapply pure_elim=> // -[?|?]; auto using pure_mono. - apply or_elim; eauto using pure_mono. Qed. Lemma pure_impl φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝). Proof. apply (anti_symm _). - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. - rewrite -pure_forall_2. apply forall_intro=> ?. by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r. Qed. Lemma pure_forall {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝. Proof. apply (anti_symm _); auto using pure_forall_2. apply forall_intro=> x. eauto using pure_mono. Qed. Lemma pure_exist {A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝. Proof. apply (anti_symm _). - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto using pure_mono. - apply exist_elim=> x. eauto using pure_mono. Qed. Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P). Proof. apply (anti_symm _). - apply forall_intro=> ?. by rewrite pure_True // left_id. - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ). Qed. Lemma pure_alt φ : ⌜φ⌝ ⊣⊢ ∃ _ : φ, True. Proof. apply (anti_symm _). - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto. - by apply exist_elim, pure_intro. Qed. Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ : φ, P). Proof. apply (anti_symm _). - apply forall_intro=> Hφ. `````` Ralf Jung committed Jun 10, 2018 551 `````` rewrite -(pure_intro φ emp%I) // emp_wand //. `````` Robbert Krebbers committed Oct 30, 2017 552 `````` - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ. `````` Robbert Krebbers committed Oct 30, 2017 553 `````` apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing. `````` Robbert Krebbers committed Oct 30, 2017 554 555 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 556 557 ``````(* Properties of the affinely modality *) Global Instance affinely_ne : NonExpansive (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 558 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 559 ``````Global Instance affinely_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 560 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 561 ``````Global Instance affinely_mono' : Proper ((⊢) ==> (⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 562 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 563 564 ``````Global Instance affinely_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 565 566 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Mar 04, 2018 567 ``````Lemma affinely_elim_emp P : P ⊢ emp. `````` Jacques-Henri Jourdan committed Nov 02, 2017 568 ``````Proof. rewrite /bi_affinely; auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 569 ``````Lemma affinely_elim P : P ⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 570 ``````Proof. rewrite /bi_affinely; auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 571 ``````Lemma affinely_mono P Q : (P ⊢ Q) → P ⊢ Q. `````` Robbert Krebbers committed Oct 30, 2017 572 ``````Proof. by intros ->. Qed. `````` Robbert Krebbers committed Mar 04, 2018 573 ``````Lemma affinely_idemp P : P ⊣⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 574 ``````Proof. by rewrite /bi_affinely assoc idemp. Qed. `````` Robbert Krebbers committed Oct 30, 2017 575 `````` `````` Robbert Krebbers committed Mar 04, 2018 576 ``````Lemma affinely_intro' P Q : ( P ⊢ Q) → P ⊢ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 577 ``````Proof. intros <-. by rewrite affinely_idemp. Qed. `````` Robbert Krebbers committed Oct 30, 2017 578 `````` `````` Robbert Krebbers committed Mar 04, 2018 579 ``````Lemma affinely_False : False ⊣⊢ False. `````` Jacques-Henri Jourdan committed Nov 02, 2017 580 ``````Proof. by rewrite /bi_affinely right_absorb. Qed. `````` Robbert Krebbers committed Mar 04, 2018 581 ``````Lemma affinely_emp : emp ⊣⊢ emp. `````` Jacques-Henri Jourdan committed Nov 02, 2017 582 ``````Proof. by rewrite /bi_affinely (idemp bi_and). Qed. `````` Robbert Krebbers committed Mar 04, 2018 583 ``````Lemma affinely_or P Q : (P ∨ Q) ⊣⊢ P ∨ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 584 ``````Proof. by rewrite /bi_affinely and_or_l. Qed. `````` Robbert Krebbers committed Mar 04, 2018 585 ``````Lemma affinely_and P Q : (P ∧ Q) ⊣⊢ P ∧ Q. `````` Robbert Krebbers committed Oct 30, 2017 586 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 587 `````` rewrite /bi_affinely -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P). `````` Robbert Krebbers committed Oct 30, 2017 588 589 `````` by rewrite idemp !assoc (comm _ P). Qed. `````` Robbert Krebbers committed Mar 04, 2018 590 ``````Lemma affinely_sep_2 P Q : P ∗ Q ⊢ (P ∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 591 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 592 `````` rewrite /bi_affinely. apply and_intro. `````` Robbert Krebbers committed Oct 30, 2017 593 594 595 `````` - by rewrite !and_elim_l right_id. - by rewrite !and_elim_r. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 596 ``````Lemma affinely_sep `{BiPositive PROP} P Q : `````` Robbert Krebbers committed Mar 04, 2018 597 `````` (P ∗ Q) ⊣⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 598 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 599 `````` apply (anti_symm _), affinely_sep_2. `````` Robbert Krebbers committed Mar 04, 2018 600 `````` by rewrite -{1}affinely_idemp bi_positive !(comm _ ( P)%I) bi_positive. `````` Robbert Krebbers committed Oct 30, 2017 601 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 602 ``````Lemma affinely_forall {A} (Φ : A → PROP) : (∀ a, Φ a) ⊢ ∀ a, (Φ a). `````` Robbert Krebbers committed Oct 30, 2017 603 ``````Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. `````` Robbert Krebbers committed Mar 04, 2018 604 ``````Lemma affinely_exist {A} (Φ : A → PROP) : (∃ a, Φ a) ⊣⊢ ∃ a, (Φ a). `````` Jacques-Henri Jourdan committed Nov 02, 2017 605 606 ``````Proof. by rewrite /bi_affinely and_exist_l. Qed. `````` Robbert Krebbers committed Mar 04, 2018 607 ``````Lemma affinely_True_emp : True ⊣⊢ emp. `````` Jacques-Henri Jourdan committed Nov 02, 2017 608 609 ``````Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 610 ``````Lemma affinely_and_l P Q : P ∧ Q ⊣⊢ (P ∧ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 611 ``````Proof. by rewrite /bi_affinely assoc. Qed. `````` Robbert Krebbers committed Mar 04, 2018 612 ``````Lemma affinely_and_r P Q : P ∧ Q ⊣⊢ (P ∧ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 613 ``````Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed. `````` Robbert Krebbers committed Mar 04, 2018 614 ``````Lemma affinely_and_lr P Q : P ∧ Q ⊣⊢ P ∧ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 615 616 617 618 ``````Proof. by rewrite affinely_and_l affinely_and_r. Qed. (* Properties of the absorbingly modality *) Global Instance absorbingly_ne : NonExpansive (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 619 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 620 ``````Global Instance absorbingly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 621 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 622 ``````Global Instance absorbingly_mono' : Proper ((⊢) ==> (⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 623 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 624 625 ``````Global Instance absorbingly_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 626 627 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Mar 04, 2018 628 ``````Lemma absorbingly_intro P : P ⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 629 ``````Proof. by rewrite /bi_absorbingly -True_sep_2. Qed. `````` Robbert Krebbers committed Mar 04, 2018 630 ``````Lemma absorbingly_mono P Q : (P ⊢ Q) → P ⊢ Q. `````` Robbert Krebbers committed Oct 30, 2017 631 ``````Proof. by intros ->. Qed. `````` Robbert Krebbers committed Mar 04, 2018 632 ``````Lemma absorbingly_idemp P : P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 633 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 634 635 `````` apply (anti_symm _), absorbingly_intro. rewrite /bi_absorbingly assoc. apply sep_mono; auto. `````` Robbert Krebbers committed Oct 30, 2017 636 637 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 638 ``````Lemma absorbingly_pure φ : ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝. `````` Robbert Krebbers committed Oct 30, 2017 639 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 640 `````` apply (anti_symm _), absorbingly_intro. `````` Robbert Krebbers committed Oct 30, 2017 641 642 `````` apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 643 ``````Lemma absorbingly_or P Q : (P ∨ Q) ⊣⊢ P ∨ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 644 ``````Proof. by rewrite /bi_absorbingly sep_or_l. Qed. `````` Robbert Krebbers committed Mar 08, 2018 645 ``````Lemma absorbingly_and_1 P Q : (P ∧ Q) ⊢ P ∧ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 646 ``````Proof. apply and_intro; apply absorbingly_mono; auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 647 ``````Lemma absorbingly_forall {A} (Φ : A → PROP) : (∀ a, Φ a) ⊢ ∀ a, (Φ a). `````` Robbert Krebbers committed Oct 30, 2017 648 ``````Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. `````` Robbert Krebbers committed Mar 04, 2018 649 ``````Lemma absorbingly_exist {A} (Φ : A → PROP) : (∃ a, Φ a) ⊣⊢ ∃ a, (Φ a). `````` Jacques-Henri Jourdan committed Nov 02, 2017 650 ``````Proof. by rewrite /bi_absorbingly sep_exist_l. Qed. `````` Robbert Krebbers committed Oct 30, 2017 651 `````` `````` Robbert Krebbers committed Mar 04, 2018 652 ``````Lemma absorbingly_sep P Q : (P ∗ Q) ⊣⊢ P ∗ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 653 ``````Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed. `````` Robbert Krebbers committed Mar 04, 2018 654 ``````Lemma absorbingly_True_emp : True ⊣⊢ emp. `````` Jacques-Henri Jourdan committed Nov 02, 2017 655 ``````Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed. `````` Robbert Krebbers committed Mar 04, 2018 656 ``````Lemma absorbingly_wand P Q : (P -∗ Q) ⊢ P -∗ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 657 ``````Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 658 `````` `````` Robbert Krebbers committed Mar 04, 2018 659 ``````Lemma absorbingly_sep_l P Q : P ∗ Q ⊣⊢ (P ∗ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 660 ``````Proof. by rewrite /bi_absorbingly assoc. Qed. `````` Robbert Krebbers committed Mar 04, 2018 661 ``````Lemma absorbingly_sep_r P Q : P ∗ Q ⊣⊢ (P ∗ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 662 ``````Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed. `````` Robbert Krebbers committed Mar 04, 2018 663 ``````Lemma absorbingly_sep_lr P Q : P ∗ Q ⊣⊢ P ∗ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 664 ``````Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 665 `````` `````` Ralf Jung committed Mar 22, 2018 666 ``````Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 667 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 668 669 `````` apply (anti_symm _), affinely_mono, absorbingly_intro. by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id. `````` Robbert Krebbers committed Oct 30, 2017 670 671 ``````Qed. `````` 672 ``````(* Affine and absorbing propositions *) `````` Robbert Krebbers committed Oct 30, 2017 673 ``````Global Instance Affine_proper : Proper ((⊣⊢) ==> iff) (@Affine PROP). `````` Robbert Krebbers committed Oct 30, 2017 674 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 30, 2017 675 676 ``````Global Instance Absorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP). Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 30, 2017 677 `````` `````` Robbert Krebbers committed Mar 04, 2018 678 ``````Lemma affine_affinely P `{!Affine P} : P ⊣⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 679 ``````Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed. `````` Robbert Krebbers committed Mar 04, 2018 680 ``````Lemma absorbing_absorbingly P `{!Absorbing P} : P ⊣⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 681 ``````Proof. by apply (anti_symm _), absorbingly_intro. Qed. `````` Robbert Krebbers committed Oct 30, 2017 682 `````` `````` Ralf Jung committed Apr 05, 2018 683 ``````Lemma True_affine_all_affine P : Affine (PROP:=PROP) True → Affine P. `````` Robbert Krebbers committed Oct 30, 2017 684 ``````Proof. rewrite /Affine=> <-; auto. Qed. `````` Ralf Jung committed Apr 05, 2018 685 ``````Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp → Absorbing P. `````` Robbert Krebbers committed Oct 30, 2017 686 ``````Proof. `````` Ralf Jung committed Jun 10, 2018 687 688 `````` intros. rewrite /Absorbing -{2}(emp_sep P). rewrite -(absorbing emp) absorbingly_sep_l left_id //. `````` Robbert Krebbers committed Oct 30, 2017 689 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 690 691 `````` Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 692 693 694 695 696 ``````Proof. destruct H. - by rewrite (affine Q) right_id. - by rewrite (True_intro Q) comm. Qed. `````` Robbert Krebbers committed Oct 30, 2017 697 698 699 ``````Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q. Proof. by rewrite comm sep_elim_l. Qed. `````` Ralf Jung committed Feb 21, 2018 700 701 ``````Lemma sep_and P Q : TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) → `````` Robbert Krebbers committed Oct 30, 2017 702 `````` P ∗ Q ⊢ P ∧ Q. `````` Robbert Krebbers committed Oct 30, 2017 703 ``````Proof. `````` Ralf Jung committed Feb 21, 2018 704 `````` intros [?|?] [?|?]; `````` Robbert Krebbers committed Oct 30, 2017 705 706 `````` apply and_intro; apply: sep_elim_l || apply: sep_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 707 `````` `````` Robbert Krebbers committed Mar 04, 2018 708 ``````Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 709 ``````Proof. intros <-. by rewrite affine_affinely. Qed. `````` Robbert Krebbers committed Oct 30, 2017 710 711 712 713 714 715 716 717 718 719 720 `````` Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P. Proof. apply (anti_symm _); auto. Qed. Lemma and_emp P `{!Affine P} : P ∧ emp ⊣⊢ P. Proof. apply (anti_symm _); auto. Qed. Lemma emp_or P `{!Affine P} : emp ∨ P ⊣⊢ emp. Proof. apply (anti_symm _); auto. Qed. Lemma or_emp P `{!Affine P} : P ∨ emp ⊣⊢ emp. Proof. apply (anti_symm _); auto. Qed. Lemma True_sep P `{!Absorbing P} : True ∗ P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 721 ``````Proof. apply (anti_symm _); auto using True_sep_2. Qed. `````` Robbert Krebbers committed Oct 30, 2017 722 ``````Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 723 ``````Proof. by rewrite comm True_sep. Qed. `````` Robbert Krebbers committed Oct 30, 2017 724 `````` `````` Ralf Jung committed Feb 21, 2018 725 726 727 728 729 730 731 732 733 ``````Lemma True_emp_iff_BiAffine : BiAffine PROP ↔ (True ⊢ emp). Proof. split. - intros ?. exact: affine. - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp. exact: True_intro. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 734 735 ``````Section bi_affine. Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 736 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 737 `````` Global Instance bi_affine_absorbing P : Absorbing P | 0. `````` Jacques-Henri Jourdan committed Nov 02, 2017 738 `````` Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 739 `````` Global Instance bi_affine_positive : BiPositive PROP. `````` Jacques-Henri Jourdan committed Nov 02, 2017 740 `````` Proof. intros P Q. by rewrite !affine_affinely. Qed. `````` Robbert Krebbers committed Oct 30, 2017 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 `````` Lemma True_emp : True ⊣⊢ emp. Proof. apply (anti_symm _); auto using affine. Qed. Global Instance emp_and' : LeftId (⊣⊢) emp%I (@bi_and PROP). Proof. intros P. by rewrite -True_emp left_id. Qed. Global Instance and_emp' : RightId (⊣⊢) emp%I (@bi_and PROP). Proof. intros P. by rewrite -True_emp right_id. Qed. Global Instance True_sep' : LeftId (⊣⊢) True%I (@bi_sep PROP). Proof. intros P. by rewrite True_emp left_id. Qed. Global Instance sep_True' : RightId (⊣⊢) True%I (@bi_sep PROP). Proof. intros P. by rewrite True_emp right_id. Qed. Lemma impl_wand_1 P Q : (P → Q) ⊢ P -∗ Q. Proof. apply wand_intro_l. by rewrite sep_and impl_elim_r. Qed. Lemma decide_emp φ `{!Decision φ} (P : PROP) : (if decide φ then P else emp) ⊣⊢ (⌜φ⌝ → P). Proof. destruct (decide _). - by rewrite pure_True // True_impl. - by rewrite pure_False // False_impl True_emp. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 765 ``````End bi_affine. `````` Robbert Krebbers committed Oct 30, 2017 766 `````` `````` Jacques-Henri Jourdan committed Nov 03, 2017 767 ``````(* Properties of the persistence modality *) `````` Tej Chajed committed Nov 29, 2018 768 ``````Hint Resolve persistently_mono : core. `````` Robbert Krebbers committed Oct 30, 2017 769 770 771 772 773 ``````Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP). Proof. intros P Q; apply persistently_mono. Qed. Global Instance persistently_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP). Proof. intros P Q; apply persistently_mono. Qed. `````` Robbert Krebbers committed Oct 30, 2017 774 `````` `````` Ralf Jung committed Mar 22, 2018 775 ``````Lemma absorbingly_elim_persistently P : P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 776 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 777 778 `````` apply (anti_symm _), absorbingly_intro. by rewrite /bi_absorbingly comm persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 779 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 780 `````` `````` Ralf Jung committed Feb 21, 2018 781 ``````Lemma persistently_forall {A} (Ψ : A → PROP) : `````` Robbert Krebbers committed Mar 04, 2018 782 `````` (∀ a, Ψ a) ⊣⊢ ∀ a, (Ψ a). `````` Ralf Jung committed Feb 21, 2018 783 784 785 786 787 ``````Proof. apply (anti_symm _); auto using persistently_forall_2. apply forall_intro=> x. by rewrite (forall_elim x). Qed. Lemma persistently_exist {A} (Ψ : A → PROP) : `````` Robbert Krebbers committed Mar 04, 2018 788 `````` (∃ a, Ψ a) ⊣⊢ ∃ a, (Ψ a). `````` Ralf Jung committed Feb 21, 2018 789 790 791 792 ``````Proof. apply (anti_symm _); auto using persistently_exist_1. apply exist_elim=> x. by rewrite (exist_intro x). Qed. `````` Robbert Krebbers committed Mar 04, 2018 793 ``````Lemma persistently_and P Q : (P ∧ Q) ⊣⊢ P ∧ Q. `````` Ralf Jung committed Feb 21, 2018 794 ``````Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed. `````` Robbert Krebbers committed Mar 04, 2018 795 ``````Lemma persistently_or P Q : (P ∨ Q) ⊣⊢ P ∨ Q. `````` Ralf Jung committed Feb 21, 2018 796 ``````Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed. `````` Robbert Krebbers committed Mar 04, 2018 797 ``````Lemma persistently_impl P Q : (P → Q) ⊢ P → Q. `````` Ralf Jung committed Feb 21, 2018 798 799 800 801 802 ``````Proof. apply impl_intro_l; rewrite -persistently_and. apply persistently_mono, impl_elim with P; auto. Qed. `````` Robbert Krebbers committed Mar 16, 2018 803 804 805 806 807 ``````Lemma persistently_emp_intro P : P ⊢ emp. Proof. by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing. Qed. `````` Robbert Krebbers committed Mar 04, 2018 808 ``````Lemma persistently_True_emp : True ⊣⊢ emp. `````` Ralf Jung committed Feb 21, 2018 809 810 ``````Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed. `````` Robbert Krebbers committed Mar 04, 2018 811 ``````Lemma persistently_and_emp P : P ⊣⊢ (emp ∧ P). `````` Ralf Jung committed Feb 21, 2018 812 813 814 815 816 817 ``````Proof. apply (anti_symm (⊢)); last by rewrite and_elim_r. rewrite persistently_and. apply and_intro; last done. apply persistently_emp_intro. Qed. `````` Robbert Krebbers committed Mar 04, 2018 818 ``````Lemma persistently_and_sep_elim_emp P Q : P ∧ Q ⊢ (emp ∧ P) ∗ Q. `````` Ralf Jung committed Feb 21, 2018 819 820 821 822 823 ``````Proof. rewrite persistently_and_emp. apply persistently_and_sep_elim. Qed. `````` Robbert Krebbers committed Mar 04, 2018 824 ``````Lemma persistently_and_sep_assoc P Q R : P ∧ (Q ∗ R) ⊣⊢ ( P ∧ Q) ∗ R. `````` Robbert Krebbers committed Oct 30, 2017 825 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 826 `````` apply (anti_symm (⊢)). `````` Ralf Jung committed Feb 21, 2018 827 `````` - rewrite {1}persistently_idemp_2 persistently_and_sep_elim_emp assoc. `````` Robbert Krebbers committed Oct 30, 2017 828 `````` apply sep_mono_l, and_intro. `````` 829 `````` + by rewrite and_elim_r persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 830 831 `````` + by rewrite and_elim_l left_id. - apply and_intro. `````` 832 `````` + by rewrite and_elim_l persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 833 `````` + by rewrite and_elim_r. `````` Robbert Krebbers committed Oct 30, 2017 834 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 835 ``````Lemma persistently_and_emp_elim P : emp ∧ P ⊢ P. `````` Ralf Jung committed Feb 21, 2018 836 ``````Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed. `````` Ralf Jung committed Mar 22, 2018 837 ``````Lemma persistently_into_absorbingly P : P ⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 838 ``````Proof. `````` Ralf Jung committed Jun 10, 2018 839 840 `````` rewrite -(right_id True%I _ ( _)%I) -{1}(emp_sep True%I). rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm //. `````` Robbert Krebbers committed Oct 30, 2017 841 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 842 ``````Lemma persistently_elim P `{!Absorbing P} : P ⊢ P. `````` Ralf Jung committed Mar 22, 2018 843 ``````Proof. by rewrite persistently_into_absorbingly absorbing_absorbingly. Qed. `````` Robbert Krebbers committed Oct 30, 2017 844 `````` `````` Robbert Krebbers committed Mar 04, 2018 845 ``````Lemma persistently_idemp_1 P : P ⊢ P. `````` Ralf Jung committed Mar 22, 2018 846 ``````Proof. by rewrite persistently_into_absorbingly absorbingly_elim_persistently. Qed. `````` Robbert Krebbers committed Mar 04, 2018 847 ``````Lemma persistently_idemp P : P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 848 ``````Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed. `````` Robbert Krebbers committed Oct 30, 2017 849 `````` `````` Robbert Krebbers committed Mar 04, 2018 850 ``````Lemma persistently_intro' P Q : ( P ⊢ Q) → P ⊢ Q. `````` Robbert Krebbers committed Oct 30, 2017 851 852 ``````Proof. intros <-. apply persistently_idemp_2. Qed. `````` Robbert Krebbers committed Mar 04, 2018 853 ``````Lemma persistently_pure φ : ⌜φ⌝ ⊣⊢ ⌜φ⌝. `````` Robbert Krebbers committed Oct 30, 2017 854 ``````Proof. `````` 855 `````` apply (anti_symm _). `````` Ralf Jung committed Mar 22, 2018 856 `````` { by rewrite persistently_into_absorbingly absorbingly_pure. } `````` Robbert Krebbers committed Oct 30, 2017 857 `````` apply pure_elim'=> Hφ. `````` Robbert Krebbers committed Mar 04, 2018 858 `````` trans (∀ x : False, True : PROP)%I; [by apply forall_intro|]. `````` Robbert Krebbers committed Oct 30, 2017 859 `````` rewrite persistently_forall_2. auto using persistently_mono, pure_intro. `````` Robbert Krebbers committed Oct 30, 2017 860 861 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 862 ``````Lemma persistently_sep_dup P : P ⊣⊢ P ∗ P. `````` Robbert Krebbers committed Oct 30, 2017 863 ``````Proof. `````` 864 `````` apply (anti_symm _). `````` Robbert Krebbers committed Mar 04, 2018 865 `````` - rewrite -{1}(idemp bi_and ( _)%I). `````` Ralf Jung committed Jun 10, 2018 866 `````` by rewrite -{2}(emp_sep ( _)%I) `````` 867 868 `````` persistently_and_sep_assoc and_elim_l. - by rewrite persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 869 870 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 871 ``````Lemma persistently_and_sep_l_1 P Q : P ∧ Q ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 872 ``````Proof. `````` Ralf Jung committed Jun 10, 2018 873 `````` by rewrite -{1}(emp_sep Q%I) persistently_and_sep_assoc and_elim_l. `````` Robbert Krebbers committed Oct 30, 2017 874 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 875 ``````Lemma persistently_and_sep_r_1 P Q : P ∧ Q ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 876 877 ``````Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed. `````` Robbert Krebbers committed Mar 04, 2018 878 ``````Lemma persistently_and_sep P Q : (P ∧ Q) ⊢ (P ∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 879 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 880 `````` rewrite persistently_and. `````` Ralf Jung committed Jun 10, 2018 881 `````` rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q%I). `````` Robbert Krebbers committed Oct 30, 2017 882 883 884 `````` by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim. Qed. `````` Ralf Jung committed Mar 22, 2018 885 ``````Lemma persistently_affinely_elim P : P ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 886 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 887 `````` by rewrite /bi_affinely persistently_and -persistently_True_emp `````` Robbert Krebbers committed Oct 30, 2017 888 `````` persistently_pure left_id. `````` Robbert Krebbers committed Oct 30, 2017 889 890 ``````Qed. `````` Robbert Krebbers committed Mar 04, 2018 891 ``````Lemma and_sep_persistently P Q : P ∧ Q ⊣⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 892 ``````Proof. `````` 893 894 895 896 `````` apply (anti_symm _); auto using persistently_and_sep_l_1. apply and_intro. - by<``````