derived_laws.v 102 KB
 Jacques-Henri Jourdan committed Dec 04, 2017 1 ``````From iris.bi Require Export derived_connectives. `````` Robbert Krebbers committed Oct 30, 2017 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 ``````From iris.algebra Require Import monoid. From stdpp Require Import hlist. 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. Hint Extern 100 (NonExpansive _) => solve_proper. (* Force implicit argument PROP *) Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I). Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I). (* 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. Global Instance bi_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_valid PROP). Proof. solve_proper. Qed. Global Instance bi_valid_mono : Proper ((⊢) ==> impl) (@bi_valid PROP). Proof. solve_proper. Qed. Global Instance bi_valid_flip_mono : Proper (flip (⊢) ==> flip impl) (@bi_valid PROP). 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. `````` Jacques-Henri Jourdan committed Nov 03, 2017 71 72 ``````Global Instance plainly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly PROP) := ne_proper _. `````` Robbert Krebbers committed Oct 30, 2017 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 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 ``````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. Hint Resolve pure_intro forall_intro. Hint Resolve or_elim or_intro_l' or_intro_r'. Hint Resolve and_intro and_elim_l' and_elim_r'. 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. Hint Immediate False_elim. 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 209 ``````Lemma exist_impl_forall {A} P (Ψ : A → PROP) : `````` Robbert Krebbers committed Oct 30, 2017 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 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 313 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 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 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 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 `````` ((∃ 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. 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 *) Hint Resolve sep_mono. 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. Lemma sep_intro_valid_l P Q R : P → (R ⊢ Q) → R ⊢ P ∗ Q. Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed. Lemma sep_intro_valid_r P Q R : (R ⊢ P) → Q → R ⊢ P ∗ Q. Proof. intros -> ?. rewrite comm. by apply sep_intro_valid_l. Qed. Lemma sep_elim_valid_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q. Proof. intros <- <-. by rewrite left_id. Qed. Lemma sep_elim_valid_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q. 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. Lemma emp_wand P : (emp -∗ P) ⊣⊢ P. Proof. apply (anti_symm _). - by rewrite -[(emp -∗ P)%I]left_id wand_elim_r. - apply wand_intro_l. by rewrite left_id. Qed. Lemma False_wand P : (False -∗ P) ⊣⊢ True. Proof. apply (anti_symm (⊢)); [by auto|]. apply wand_intro_l. rewrite left_absorb. auto. Qed. 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. Proof. intros. rewrite -[P]left_id. by apply wand_elim_l'. Qed. Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I. Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed. 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 (⊢)); apply wand_entails; rewrite /bi_valid HPQ /bi_wand_iff; auto. 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 (⊢)); apply: impl_entails; rewrite /bi_valid HPQ /bi_iff; auto. Qed. (* 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φ. by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro emp%I φ) // wand_elim_r. - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ. `````` Robbert Krebbers committed Oct 30, 2017 497 `````` apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing. `````` Robbert Krebbers committed Oct 30, 2017 498 499 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 500 501 ``````(* Properties of the affinely modality *) Global Instance affinely_ne : NonExpansive (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 502 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 503 ``````Global Instance affinely_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 504 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 505 ``````Global Instance affinely_mono' : Proper ((⊢) ==> (⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 506 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 507 508 ``````Global Instance affinely_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP). `````` Robbert Krebbers committed Oct 30, 2017 509 510 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 511 512 513 514 515 ``````Lemma affinely_elim_emp P : bi_affinely P ⊢ emp. Proof. rewrite /bi_affinely; auto. Qed. Lemma affinely_elim P : bi_affinely P ⊢ P. Proof. rewrite /bi_affinely; auto. Qed. Lemma affinely_mono P Q : (P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q. `````` Robbert Krebbers committed Oct 30, 2017 516 ``````Proof. by intros ->. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 517 518 ``````Lemma affinely_idemp P : bi_affinely (bi_affinely P) ⊣⊢ bi_affinely P. Proof. by rewrite /bi_affinely assoc idemp. Qed. `````` Robbert Krebbers committed Oct 30, 2017 519 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 520 521 ``````Lemma affinely_intro' P Q : (bi_affinely P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q. Proof. intros <-. by rewrite affinely_idemp. Qed. `````` Robbert Krebbers committed Oct 30, 2017 522 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 523 524 525 526 527 528 529 ``````Lemma affinely_False : bi_affinely False ⊣⊢ False. Proof. by rewrite /bi_affinely right_absorb. Qed. Lemma affinely_emp : bi_affinely emp ⊣⊢ emp. Proof. by rewrite /bi_affinely (idemp bi_and). Qed. Lemma affinely_or P Q : bi_affinely (P ∨ Q) ⊣⊢ bi_affinely P ∨ bi_affinely Q. Proof. by rewrite /bi_affinely and_or_l. Qed. Lemma affinely_and P Q : bi_affinely (P ∧ Q) ⊣⊢ bi_affinely P ∧ bi_affinely Q. `````` Robbert Krebbers committed Oct 30, 2017 530 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 531 `````` rewrite /bi_affinely -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P). `````` Robbert Krebbers committed Oct 30, 2017 532 533 `````` by rewrite idemp !assoc (comm _ P). Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 534 ``````Lemma affinely_sep_2 P Q : bi_affinely P ∗ bi_affinely Q ⊢ bi_affinely (P ∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 535 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 536 `````` rewrite /bi_affinely. apply and_intro. `````` Robbert Krebbers committed Oct 30, 2017 537 538 539 `````` - by rewrite !and_elim_l right_id. - by rewrite !and_elim_r. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 540 ``````Lemma affinely_sep `{BiPositive PROP} P Q : `````` Jacques-Henri Jourdan committed Nov 02, 2017 541 `````` bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q. `````` Robbert Krebbers committed Oct 30, 2017 542 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 543 `````` apply (anti_symm _), affinely_sep_2. `````` Jacques-Henri Jourdan committed Dec 04, 2017 544 `````` by rewrite -{1}affinely_idemp bi_positive !(comm _ (bi_affinely P)%I) bi_positive. `````` Robbert Krebbers committed Oct 30, 2017 545 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 546 547 ``````Lemma affinely_forall {A} (Φ : A → PROP) : bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a). `````` Robbert Krebbers committed Oct 30, 2017 548 ``````Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 ``````Lemma affinely_exist {A} (Φ : A → PROP) : bi_affinely (∃ a, Φ a) ⊣⊢ ∃ a, bi_affinely (Φ a). Proof. by rewrite /bi_affinely and_exist_l. Qed. Lemma affinely_True_emp : bi_affinely True ⊣⊢ bi_affinely emp. Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed. Lemma affinely_and_l P Q : bi_affinely P ∧ Q ⊣⊢ bi_affinely (P ∧ Q). Proof. by rewrite /bi_affinely assoc. Qed. Lemma affinely_and_r P Q : P ∧ bi_affinely Q ⊣⊢ bi_affinely (P ∧ Q). Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed. Lemma affinely_and_lr P Q : bi_affinely P ∧ Q ⊣⊢ P ∧ bi_affinely Q. 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 565 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 566 ``````Global Instance absorbingly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 567 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 568 ``````Global Instance absorbingly_mono' : Proper ((⊢) ==> (⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 569 ``````Proof. solve_proper. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 570 571 ``````Global Instance absorbingly_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP). `````` Robbert Krebbers committed Oct 30, 2017 572 573 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Dec 03, 2017 574 ``````Lemma absorbingly_intro P : P ⊢ bi_absorbingly P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 575 ``````Proof. by rewrite /bi_absorbingly -True_sep_2. Qed. `````` Robbert Krebbers committed Dec 03, 2017 576 ``````Lemma absorbingly_mono P Q : (P ⊢ Q) → bi_absorbingly P ⊢ bi_absorbingly Q. `````` Robbert Krebbers committed Oct 30, 2017 577 ``````Proof. by intros ->. Qed. `````` Robbert Krebbers committed Dec 03, 2017 578 ``````Lemma absorbingly_idemp P : bi_absorbingly (bi_absorbingly P) ⊣⊢ bi_absorbingly P. `````` Robbert Krebbers committed Oct 30, 2017 579 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 580 581 `````` apply (anti_symm _), absorbingly_intro. rewrite /bi_absorbingly assoc. apply sep_mono; auto. `````` Robbert Krebbers committed Oct 30, 2017 582 583 ``````Qed. `````` Robbert Krebbers committed Dec 03, 2017 584 ``````Lemma absorbingly_pure φ : bi_absorbingly ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝. `````` Robbert Krebbers committed Oct 30, 2017 585 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 586 `````` apply (anti_symm _), absorbingly_intro. `````` Robbert Krebbers committed Oct 30, 2017 587 588 `````` apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto. Qed. `````` Robbert Krebbers committed Dec 03, 2017 589 590 ``````Lemma absorbingly_or P Q : bi_absorbingly (P ∨ Q) ⊣⊢ bi_absorbingly P ∨ bi_absorbingly Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 591 ``````Proof. by rewrite /bi_absorbingly sep_or_l. Qed. `````` Robbert Krebbers committed Dec 03, 2017 592 593 ``````Lemma absorbingly_and P Q : bi_absorbingly (P ∧ Q) ⊢ bi_absorbingly P ∧ bi_absorbingly Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 594 ``````Proof. apply and_intro; apply absorbingly_mono; auto. Qed. `````` Robbert Krebbers committed Dec 03, 2017 595 596 ``````Lemma absorbingly_forall {A} (Φ : A → PROP) : bi_absorbingly (∀ a, Φ a) ⊢ ∀ a, bi_absorbingly (Φ a). `````` Robbert Krebbers committed Oct 30, 2017 597 ``````Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. `````` Robbert Krebbers committed Dec 03, 2017 598 599 ``````Lemma absorbingly_exist {A} (Φ : A → PROP) : bi_absorbingly (∃ a, Φ a) ⊣⊢ ∃ a, bi_absorbingly (Φ a). `````` Jacques-Henri Jourdan committed Nov 02, 2017 600 ``````Proof. by rewrite /bi_absorbingly sep_exist_l. Qed. `````` Robbert Krebbers committed Oct 30, 2017 601 `````` `````` Robbert Krebbers committed Dec 03, 2017 602 ``````Lemma absorbingly_sep P Q : bi_absorbingly (P ∗ Q) ⊣⊢ bi_absorbingly P ∗ bi_absorbingly Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 603 ``````Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed. `````` Robbert Krebbers committed Dec 03, 2017 604 ``````Lemma absorbingly_True_emp : bi_absorbingly True ⊣⊢ bi_absorbingly emp. `````` Jacques-Henri Jourdan committed Nov 02, 2017 605 ``````Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed. `````` Robbert Krebbers committed Dec 03, 2017 606 ``````Lemma absorbingly_wand P Q : bi_absorbingly (P -∗ Q) ⊢ bi_absorbingly P -∗ bi_absorbingly Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 607 ``````Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 608 `````` `````` Robbert Krebbers committed Dec 03, 2017 609 ``````Lemma absorbingly_sep_l P Q : bi_absorbingly P ∗ Q ⊣⊢ bi_absorbingly (P ∗ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 610 ``````Proof. by rewrite /bi_absorbingly assoc. Qed. `````` Robbert Krebbers committed Dec 03, 2017 611 ``````Lemma absorbingly_sep_r P Q : P ∗ bi_absorbingly Q ⊣⊢ bi_absorbingly (P ∗ Q). `````` Jacques-Henri Jourdan committed Nov 02, 2017 612 ``````Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed. `````` Robbert Krebbers committed Dec 03, 2017 613 ``````Lemma absorbingly_sep_lr P Q : bi_absorbingly P ∗ Q ⊣⊢ P ∗ bi_absorbingly Q. `````` Jacques-Henri Jourdan committed Nov 02, 2017 614 ``````Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 615 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 616 ``````Lemma affinely_absorbingly `{!BiPositive PROP} P : `````` Robbert Krebbers committed Dec 03, 2017 617 `````` bi_affinely (bi_absorbingly P) ⊣⊢ bi_affinely P. `````` Robbert Krebbers committed Oct 30, 2017 618 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 619 620 `````` 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 621 622 ``````Qed. `````` 623 ``````(* Affine and absorbing propositions *) `````` Robbert Krebbers committed Oct 30, 2017 624 ``````Global Instance Affine_proper : Proper ((⊣⊢) ==> iff) (@Affine PROP). `````` Robbert Krebbers committed Oct 30, 2017 625 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 30, 2017 626 627 ``````Global Instance Absorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP). Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 30, 2017 628 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 629 630 ``````Lemma affine_affinely P `{!Affine P} : bi_affinely P ⊣⊢ P. Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed. `````` Robbert Krebbers committed Dec 03, 2017 631 ``````Lemma absorbing_absorbingly P `{!Absorbing P} : bi_absorbingly P ⊣⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 632 ``````Proof. by apply (anti_symm _), absorbingly_intro. Qed. `````` Robbert Krebbers committed Oct 30, 2017 633 `````` `````` Robbert Krebbers committed Oct 30, 2017 634 635 636 ``````Lemma True_affine_all_affine P : Affine (True%I : PROP) → Affine P. Proof. rewrite /Affine=> <-; auto. Qed. Lemma emp_absorbing_all_absorbing P : Absorbing (emp%I : PROP) → Absorbing P. `````` Robbert Krebbers committed Oct 30, 2017 637 638 ``````Proof. intros. rewrite /Absorbing -{2}(left_id emp%I _ P). `````` Jacques-Henri Jourdan committed Nov 02, 2017 639 `````` by rewrite -(absorbing emp) absorbingly_sep_l left_id. `````` Robbert Krebbers committed Oct 30, 2017 640 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 641 642 `````` Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 643 644 645 646 647 ``````Proof. destruct H. - by rewrite (affine Q) right_id. - by rewrite (True_intro Q) comm. Qed. `````` Robbert Krebbers committed Oct 30, 2017 648 649 650 ``````Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q. Proof. by rewrite comm sep_elim_l. Qed. `````` Robbert Krebbers committed Oct 30, 2017 651 652 ``````Lemma sep_and P Q `{HPQ : TCOr (TCAnd (Affine P) (Affine Q)) (TCAnd (Absorbing P) (Absorbing Q))} : `````` Robbert Krebbers committed Oct 30, 2017 653 `````` P ∗ Q ⊢ P ∧ Q. `````` Robbert Krebbers committed Oct 30, 2017 654 655 656 657 ``````Proof. destruct HPQ as [[??]|[??]]; apply and_intro; apply: sep_elim_l || apply: sep_elim_r. Qed. `````` Robbert Krebbers committed Oct 30, 2017 658 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 659 660 ``````Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_affinely Q. Proof. intros <-. by rewrite affine_affinely. Qed. `````` Robbert Krebbers committed Oct 30, 2017 661 662 663 664 665 666 667 668 669 670 671 `````` 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 672 ``````Proof. apply (anti_symm _); auto using True_sep_2. Qed. `````` Robbert Krebbers committed Oct 30, 2017 673 ``````Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 674 ``````Proof. by rewrite comm True_sep. Qed. `````` Robbert Krebbers committed Oct 30, 2017 675 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 676 677 ``````Section bi_affine. Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 678 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 679 `````` Global Instance bi_affine_absorbing P : Absorbing P | 0. `````` Jacques-Henri Jourdan committed Nov 02, 2017 680 `````` Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 681 `````` Global Instance bi_affine_positive : BiPositive PROP. `````` Jacques-Henri Jourdan committed Nov 02, 2017 682 `````` Proof. intros P Q. by rewrite !affine_affinely. Qed. `````` Robbert Krebbers committed Oct 30, 2017 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 `````` 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 707 ``````End bi_affine. `````` Robbert Krebbers committed Oct 30, 2017 708 `````` `````` Jacques-Henri Jourdan committed Nov 03, 2017 709 ``````(* Properties of the persistence modality *) `````` Robbert Krebbers committed Oct 30, 2017 710 711 712 713 714 715 ``````Hint Resolve persistently_mono. 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 716 `````` `````` Robbert Krebbers committed Dec 03, 2017 717 718 ``````Lemma absorbingly_persistently P : bi_absorbingly (bi_persistently P) ⊣⊢ bi_persistently P. `````` Robbert Krebbers committed Oct 30, 2017 719 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 720 721 `````` apply (anti_symm _), absorbingly_intro. by rewrite /bi_absorbingly comm persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 722 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 723 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 724 725 ``````Lemma persistently_and_sep_assoc P Q R : bi_persistently P ∧ (Q ∗ R) ⊣⊢ (bi_persistently P ∧ Q) ∗ R. `````` Robbert Krebbers committed Oct 30, 2017 726 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 727 728 729 `````` apply (anti_symm (⊢)). - rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc. apply sep_mono_l, and_intro. `````` 730 `````` + by rewrite and_elim_r persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 731 732 `````` + by rewrite and_elim_l left_id. - apply and_intro. `````` 733 `````` + by rewrite and_elim_l persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 734 `````` + by rewrite and_elim_r. `````` Robbert Krebbers committed Oct 30, 2017 735 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 736 ``````Lemma persistently_and_emp_elim P : emp ∧ bi_persistently P ⊢ P. `````` Robbert Krebbers committed Oct 30, 2017 737 ``````Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed. `````` Robbert Krebbers committed Dec 03, 2017 738 ``````Lemma persistently_elim_absorbingly P : bi_persistently P ⊢ bi_absorbingly P. `````` Robbert Krebbers committed Oct 30, 2017 739 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 740 `````` rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I). `````` Robbert Krebbers committed Oct 30, 2017 741 `````` by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm. `````` Robbert Krebbers committed Oct 30, 2017 742 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 743 ``````Lemma persistently_elim P `{!Absorbing P} : bi_persistently P ⊢ P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 744 ``````Proof. by rewrite persistently_elim_absorbingly absorbing_absorbingly. Qed. `````` Robbert Krebbers committed Oct 30, 2017 745 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 746 747 ``````Lemma persistently_idemp_1 P : bi_persistently (bi_persistently P) ⊢ bi_persistently P. `````` Jacques-Henri Jourdan committed Nov 02, 2017 748 ``````Proof. by rewrite persistently_elim_absorbingly absorbingly_persistently. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 749 750 ``````Lemma persistently_idemp P : bi_persistently (bi_persistently P) ⊣⊢ bi_persistently P. `````` Robbert Krebbers committed Oct 30, 2017 751 ``````Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed. `````` Robbert Krebbers committed Oct 30, 2017 752 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 753 754 ``````Lemma persistently_intro' P Q : (bi_persistently P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 755 756 ``````Proof. intros <-. apply persistently_idemp_2. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 757 ``````Lemma persistently_pure φ : bi_persistently ⌜φ⌝ ⊣⊢ ⌜φ⌝. `````` Robbert Krebbers committed Oct 30, 2017 758 ``````Proof. `````` 759 760 `````` apply (anti_symm _). { by rewrite persistently_elim_absorbingly absorbingly_pure. } `````` Robbert Krebbers committed Oct 30, 2017 761 `````` apply pure_elim'=> Hφ. `````` Jacques-Henri Jourdan committed Nov 02, 2017 762 `````` trans (∀ x : False, bi_persistently True : PROP)%I; [by apply forall_intro|]. `````` Robbert Krebbers committed Oct 30, 2017 763 `````` rewrite persistently_forall_2. auto using persistently_mono, pure_intro. `````` Robbert Krebbers committed Oct 30, 2017 764 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 765 766 ``````Lemma persistently_forall {A} (Ψ : A → PROP) : bi_persistently (∀ a, Ψ a) ⊣⊢ ∀ a, bi_persistently (Ψ a). `````` Robbert Krebbers committed Oct 30, 2017 767 768 769 770 ``````Proof. apply (anti_symm _); auto using persistently_forall_2. apply forall_intro=> x. by rewrite (forall_elim x). Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 771 772 ``````Lemma persistently_exist {A} (Ψ : A → PROP) : bi_persistently (∃ a, Ψ a) ⊣⊢ ∃ a, bi_persistently (Ψ a). `````` Robbert Krebbers committed Oct 30, 2017 773 774 775 776 ``````Proof. apply (anti_symm _); auto using persistently_exist_1. apply exist_elim=> x. by rewrite (exist_intro x). Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 777 778 ``````Lemma persistently_and P Q : bi_persistently (P ∧ Q) ⊣⊢ bi_persistently P ∧ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 779 ``````Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 780 781 ``````Lemma persistently_or P Q : bi_persistently (P ∨ Q) ⊣⊢ bi_persistently P ∨ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 782 ``````Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 783 784 ``````Lemma persistently_impl P Q : bi_persistently (P → Q) ⊢ bi_persistently P → bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 785 786 787 788 789 ``````Proof. apply impl_intro_l; rewrite -persistently_and. apply persistently_mono, impl_elim with P; auto. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 790 791 ``````Lemma persistently_sep_dup P : bi_persistently P ⊣⊢ bi_persistently P ∗ bi_persistently P. `````` Robbert Krebbers committed Oct 30, 2017 792 ``````Proof. `````` 793 794 795 796 797 `````` apply (anti_symm _). - rewrite -{1}(idemp bi_and (bi_persistently _)). by rewrite -{2}(left_id emp%I _ (bi_persistently _)) persistently_and_sep_assoc and_elim_l. - by rewrite persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 798 799 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 800 ``````Lemma persistently_and_sep_l_1 P Q : bi_persistently P ∧ Q ⊢ bi_persistently P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 801 802 803 ``````Proof. by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 804 ``````Lemma persistently_and_sep_r_1 P Q : P ∧ bi_persistently Q ⊢ P ∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 805 806 ``````Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 807 808 809 ``````Lemma persistently_emp_intro P : P ⊢ bi_persistently emp. Proof. by rewrite -plainly_elim_persistently -plainly_emp_intro. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 810 ``````Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp. `````` Robbert Krebbers committed Oct 30, 2017 811 ``````Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 812 ``````Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 813 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 814 815 816 817 818 `````` rewrite persistently_and. rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I). by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 819 ``````Lemma persistently_affinely P : bi_persistently (bi_affinely P) ⊣⊢ bi_persistently P. `````` Robbert Krebbers committed Oct 30, 2017 820 ``````Proof. `````` Jacques-Henri Jourdan committed Nov 02, 2017 821 `````` by rewrite /bi_affinely persistently_and -persistently_True_emp `````` Robbert Krebbers committed Oct 30, 2017 822 `````` persistently_pure left_id. `````` Robbert Krebbers committed Oct 30, 2017 823 824 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 825 826 ``````Lemma and_sep_persistently P Q : bi_persistently P ∧ bi_persistently Q ⊣⊢ bi_persistently P ∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 827 ``````Proof. `````` 828 829 830 831 `````` apply (anti_symm _); auto using persistently_and_sep_l_1. apply and_intro. - by rewrite persistently_absorbing. - by rewrite comm persistently_absorbing. `````` Robbert Krebbers committed Oct 30, 2017 832 ``````Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 833 834 ``````Lemma persistently_sep_2 P Q : bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 835 ``````Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 836 ``````Lemma persistently_sep `{BiPositive PROP} P Q : `````` Jacques-Henri Jourdan committed Nov 02, 2017 837 `````` bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 838 839 ``````Proof. apply (anti_symm _); auto using persistently_sep_2. `````` 840 841 842 `````` rewrite -persistently_affinely affinely_sep -and_sep_persistently. apply and_intro. - by rewrite (affinely_elim_emp Q) right_id affinely_elim. - by rewrite (affinely_elim_emp P) left_id affinely_elim. `````` Robbert Krebbers committed Oct 30, 2017 843 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 844 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 845 846 ``````Lemma persistently_wand P Q : bi_persistently (P -∗ Q) ⊢ bi_persistently P -∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 847 ``````Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed. `````` Robbert Krebbers committed Oct 30, 2017 848 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 849 850 ``````Lemma persistently_entails_l P Q : (P ⊢ bi_persistently Q) → P ⊢ bi_persistently Q ∗ P. `````` Robbert Krebbers committed Oct 30, 2017 851 ``````Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 852 853 ``````Lemma persistently_entails_r P Q : (P ⊢ bi_persistently Q) → P ⊢ P ∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 854 855 ``````Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 856 857 ``````Lemma persistently_impl_wand_2 P Q : bi_persistently (P -∗ Q) ⊢ bi_persistently (P → Q). `````` Robbert Krebbers committed Oct 30, 2017 858 859 860 861 862 863 ``````Proof. apply persistently_intro', impl_intro_r. rewrite -{2}(left_id emp%I _ P%I) persistently_and_sep_assoc. by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Dec 03, 2017 864 ``````Lemma impl_wand_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persistently P → Q). `````` Robbert Krebbers committed Dec 03, 2017 865 866 ``````Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 867 ``````Section persistently_affinely_bi. `````` Jacques-Henri Jourdan committed Dec 04, 2017 868 `````` Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 869 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 870 `````` Lemma persistently_emp : bi_persistently emp ⊣⊢ emp. `````` Robbert Krebbers committed Oct 30, 2017 871 872 `````` Proof. by rewrite -!True_emp persistently_pure. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 873 874 `````` Lemma persistently_and_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ bi_persistently P ∗ Q. `````` Robbert Krebbers committed Oct 30, 2017 875 876 877 878 `````` Proof. apply (anti_symm (⊢)); eauto using persistently_and_sep_l_1, sep_and with typeclass_instances. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 879 `````` Lemma persistently_and_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ bi_persistently Q. `````` Robbert Krebbers committed Oct 30, 2017 880 881 `````` Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 882 883 `````` Lemma persistently_impl_wand P Q : bi_persistently (P → Q) ⊣⊢ bi_persistently (P -∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 884 885 886 `````` Proof. apply (anti_symm (⊢)); auto using persistently_impl_wand_2. apply persistently_intro', wand_intro_l. `````` Robbert Krebbers committed Oct 30, 2017 887 `````` by rewrite -persistently_and_sep_r persistently_elim impl_elim_r. `````` Robbert Krebbers committed Oct 30, 2017 888 889 `````` Qed. `````` Robbert Krebbers committed Dec 03, 2017 890 `````` Lemma impl_wand_persistently P Q : (bi_persistently P → Q) ⊣⊢ (bi_persistently P -∗ Q). `````` Robbert Krebbers committed Dec 03, 2017 891 `````` Proof. `````` Robbert Krebbers committed Dec 03, 2017 892 `````` apply (anti_symm (⊢)). by rewrite -impl_wand_1. apply impl_wand_persistently_2. `````` Robbert Krebbers committed Dec 03, 2017 893 894 `````` Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 895 `````` Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ bi_persistently (P ∗ R → Q). `````` Robbert Krebbers committed Oct 30, 2017 896 897 898 `````` Proof. apply (anti_symm (⊢)). - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I). `````` Robbert Krebbers committed Oct 30, 2017 899 900 `````` apply sep_mono_r. rewrite -persistently_pure. apply persistently_intro', impl_intro_l. `````` Robbert Krebbers committed Oct 30, 2017 901 `````` by rewrite wand_elim_r persistently_pure right_id. `````` Robbert Krebbers committed Oct 30, 2017 902 903 `````` - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r. `````` Robbert Krebbers committed Oct 30, 2017 904 `````` by rewrite persistently_elim impl_elim_r. `````` Robbert Krebbers committed Oct 30, 2017 905 `````` Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 906 `````` Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ bi_persistently (P ∧ R -∗ Q). `````` Robbert Krebbers committed Oct 30, 2017 907 908 909 `````` Proof. apply (anti_symm (⊢)). - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I). `````` Robbert Krebbers committed Oct 30, 2017 910 911 `````` apply and_mono_r. rewrite -persistently_pure. apply persistently_intro', wand_intro_l. `````` Robbert Krebbers committed Oct 30, 2017 912 `````` by rewrite impl_elim_r persistently_pure right_id. `````` Jacques-Henri Jourdan committed Nov 02, 2017 913 914 `````` - apply exist_elim=> R. apply impl_intro_l. by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r. `````` Robbert Krebbers committed Oct 30, 2017 915 `````` Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 916 ``````End persistently_affinely_bi. `````` Robbert Krebbers committed Oct 30, 2017 917 `````` `````` Jacques-Henri Jourdan committed Nov 03, 2017 918 919 920 921 922 923 924 925 ``````(* Properties of the plainness modality *) Hint Resolve plainly_mono. Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@bi_plainly PROP). Proof. intros P Q; apply plainly_mono. Qed. Global Instance plainly_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@bi_plainly PROP). Proof. intros P Q; apply plainly_mono. Qed. `````` 926 ``````Lemma persistently_plainly P : bi_persistently (bi_plainly P) ⊣⊢ bi_plainly P. `````` Jacques-Henri Jourdan committed Nov 03, 2017 927 ``````Proof. `````` 928 929 930 `````` apply (anti_symm _). - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorbing. - by rewrite {1}plainly_idemp_2 plainly_elim_persistently. `````` Jacques-Henri Jourdan committed Nov 03, 2017 931 ``````Qed. `````` 932 933 934 935 936 937 938 939 ``````Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P. Proof. apply (anti_symm _); first apply plainly_persistently_1. by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P). Qed. Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P. Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 940 941 942 943 944 `````` Lemma plainly_and_sep_elim P Q : bi_plainly P ∧ Q -∗ (emp ∧ P) ∗ Q. Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim. Qed. Lemma plainly_and_sep_assoc P Q R : bi_plainly P ∧ (Q ∗ R) ⊣⊢ (bi_plainly P ∧ Q) ∗ R. `````` 945 ``````Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 946 947 ``````Lemma plainly_and_emp_elim P : emp ∧ bi_plainly P ⊢ P. Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed. `````` Robbert Krebbers committed Dec 03, 2017 948 ``````Lemma plainly_elim_absorbingly P : bi_plainly P ⊢ bi_absorbingly P. `````` Jacques-Henri Jourdan committed Nov 03, 2017 949 950 951 952 953 ``````Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed. Lemma plainly_elim P `{!Absorbing P} : bi_plainly P ⊢ P. Proof. by rewrite plainly_elim_persistently persistently_elim. Qed. Lemma plainly_idemp_1 P : bi_plainly (bi_plainly P) ⊢ bi_plainly P. `````` 954 ``````Proof. by rewrite plainly_elim_absorbingly absorbingly_plainly. Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 955 956 957 958 959 960 961 962 963 ``````Lemma plainly_idemp P : bi_plainly (bi_plainly P) ⊣⊢ bi_plainly P. Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed. Lemma plainly_intro' P Q : (bi_plainly P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q. Proof. intros <-. apply plainly_idemp_2. Qed. Lemma plainly_pure φ : bi_plainly ⌜φ⌝ ⊣⊢ ⌜φ⌝. Proof. apply (anti_symm _); auto. `````` 964 `````` - by rewrite plainly_elim_persistently persistently_pure. `````` Jacques-Henri Jourdan committed Nov 03, 2017 965 966 967 968 969 970 971