derived.v 72.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 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 71 72 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 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 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 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 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874
From iris.bi Require Export interface.
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.

Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P  Q)  (Q  P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_iff) 1.
Infix "↔" := bi_iff : bi_scope.

Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
  ((P - Q)  (Q - P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.

Class Persistent {PROP : bi} (P : PROP) := persistent :  P  P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.

Definition bi_bare {PROP : bi} (P : PROP) : PROP := (emp  P)%I.
Arguments bi_bare {_} _%I : simpl never.
Instance: Params (@bi_bare) 1.
Typeclasses Opaque bi_bare.
Notation "■ P" := (bi_bare P) (at level 20, right associativity) : bi_scope.
Notation "⬕ P" := (  P)%I (at level 20, right associativity) : bi_scope.

Class Affine {PROP : bi} (Q : PROP) := affine : Q  emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
Hint Mode Affine + ! : typeclass_instances.

Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Existing Instance absorbing_bi | 0.

Class Absorbing {PROP : bi} (P : PROP) := absorbing Q : P  Q  P.
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I _%I.

Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then  P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
Notation "□? p P" := (bi_persistently_if p P)
  (at level 20, p at level 9, P at level 20,
   right associativity, format "□? p  P") : bi_scope.

Definition bi_bare_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then  P else P)%I.
Arguments bi_bare_if {_} !_ _%I /.
Instance: Params (@bi_bare_if) 2.
Typeclasses Opaque bi_bare_if.
Notation "■? p P" := (bi_bare_if p P)
  (at level 20, p at level 9, P at level 20,
   right associativity, format "■? p  P") : bi_scope.
Notation "⬕? p P" := (?p ?p P)%I
  (at level 20, p at level 9, P at level 20,
   right associativity, format "⬕? p  P") : bi_scope.

Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hexist (Φ x)
  end%I.
Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hforall (Φ x)
  end%I.

Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
  Nat.iter n bi_later P.
Arguments bi_laterN {_} !_%nat_scope _%I.
Instance: Params (@bi_laterN) 2.
Notation "▷^ n P" := (bi_laterN n P)
  (at level 20, n at level 9, P at level 20, format "▷^ n  P") : bi_scope.
Notation "▷? p P" := (bi_laterN (Nat.b2n p) P)
  (at level 20, p at level 9, P at level 20, format "▷? p  P") : bi_scope.

Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := ( False  P)%I.
Arguments bi_except_0 {_} _%I : simpl never.
Notation "◇ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
Instance: Params (@bi_except_0) 1.
Typeclasses Opaque bi_except_0.

Class Timeless {PROP : sbi} (P : PROP) := timeless :  P   P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.

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.
Global Instance internal_eq_proper (A : ofeT) :
  Proper (() ==> () ==> ()) (@bi_internal_eq PROP A) := ne_proper_2 _.
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.

Lemma exists_impl_forall {A} P (Ψ : A  PROP) :
  (( 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.

(* Equality stuff *)
Hint Resolve internal_eq_refl.
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
Proof. intros ->. auto. Qed.
Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A  PROP) P
  {HΨ : NonExpansive Ψ} : (P  a  b)  (P  Ψ a)  P  Ψ b.
Proof.
  intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
  apply impl_elim_l'. by apply internal_eq_rewrite.
Qed.

Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
Proof. apply (internal_eq_rewrite' a b (λ b, b  a)%I); auto. Qed.
Lemma internal_eq_iff P Q : P  Q  P  Q.
Proof. apply (internal_eq_rewrite' P Q (λ Q, P  Q))%I; auto using iff_refl. Qed.

Lemma f_equiv {A B : ofeT} (f : A  B) `{!NonExpansive f} x y :
  x  y  f x  f y.
Proof. apply (internal_eq_rewrite' x y (λ y, f x  f y)%I); auto. Qed.

Lemma prod_equivI {A B : ofeT} (x y : A * B) : x  y  x.1  y.1  x.2  y.2.
Proof.
  apply (anti_symm _).
  - apply and_intro; apply f_equiv; apply _.
  - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
    apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2)  (a,y.2))%I); auto.
    apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2)  (x.1,b))%I); auto.
Qed.
Lemma sum_equivI {A B : ofeT} (x y : A + B) :
  x  y 
    match x, y with
    | inl a, inl a' => a  a' | inr b, inr b' => b  b' | _, _ => False
    end.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' x y (λ y,
             match x, y with
             | inl a, inl a' => a  a' | inr b, inr b' => b  b' | _, _ => False
             end)%I); auto.
    destruct x; auto.
  - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _.
Qed.
Lemma option_equivI {A : ofeT} (x y : option A) :
  x  y  match x, y with
           | Some a, Some a' => a  a' | None, None => True | _, _ => False
           end.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' x y (λ y,
             match x, y with
             | Some a, Some a' => a  a' | None, None => True | _, _ => False
             end)%I); auto.
    destruct x; auto.
  - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _.
Qed.

Lemma sig_equivI {A : ofeT} (P : A  Prop) (x y : sig P) : `x  `y  x  y.
Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.

Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f  g   x, f x  g x.
Proof.
  apply (anti_symm _); auto using fun_ext.
  apply (internal_eq_rewrite' f g (λ g,  x : A, f x  g x)%I); auto.
  intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
Qed.
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f  g   x, f x  g x.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' f g (λ g,  x : A, f x  g x)%I); auto.
  - rewrite -(ofe_funC_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
    set (h1 (f : A -n> B) :=
      exist (λ f : A -c> B, NonExpansive f) f (ofe_mor_ne A B f)).
    set (h2 (f : sigC (λ f : A -c> B, NonExpansive f)) :=
      @CofeMor A B (`f) (proj2_sig f)).
    assert ( f, h2 (h1 f) = f) as Hh by (by intros []).
    assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
    by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
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φ.
    apply wand_intro_l. by rewrite (forall_elim Hφ) absorbing.
Qed.

Lemma pure_internal_eq {A : ofeT} (x y : A) : x  y  x  y.
Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a  a  b  a  b.
Proof.
  intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
Qed.

(* Properties of the bare modality *)
Global Instance bare_ne : NonExpansive (@bi_bare PROP).
Proof. solve_proper. Qed.
Global Instance bare_proper : Proper (() ==> ()) (@bi_bare PROP).
Proof. solve_proper. Qed.
Global Instance bare_mono' : Proper (() ==> ()) (@bi_bare PROP).
Proof. solve_proper. Qed.
Global Instance bare_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_bare PROP).
Proof. solve_proper. Qed.

Lemma bare_elim_emp P :  P  emp.
Proof. rewrite /bi_bare; auto. Qed.
Lemma bare_elim P :  P  P.
Proof. rewrite /bi_bare; auto. Qed.
Lemma bare_mono P Q : (P  Q)   P   Q.
Proof. by intros ->. Qed.
Lemma bare_idemp P :   P   P.
Proof. by rewrite /bi_bare assoc idemp. Qed.

Lemma bare_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. by rewrite bare_idemp. Qed.

Lemma bare_False :  False  False.
Proof. by rewrite /bi_bare right_absorb. Qed.
Lemma bare_emp :  emp  emp.
Proof. by rewrite /bi_bare (idemp bi_and). Qed.
Lemma bare_or P Q :  (P  Q)   P   Q.
Proof. by rewrite /bi_bare and_or_l. Qed.
Lemma bare_and P Q :  (P  Q)   P   Q.
Proof.
  rewrite /bi_bare -(comm _ P) (assoc _ (_  _)%I) -!(assoc _ P).
  by rewrite idemp !assoc (comm _ P).
Qed.
Lemma bare_sep P Q :  (P  Q)   P   Q.
Proof.
  rewrite /bi_bare. apply (anti_symm _).
  - rewrite -{1}(idemp bi_and emp%I) -assoc emp_and_sep_assoc_1.
    by rewrite (comm bi_sep) emp_and_sep_assoc_1 comm.
  - apply and_intro.
    + by rewrite !and_elim_l right_id.
    + by rewrite !and_elim_r.
Qed.
Lemma bare_forall {A} (Φ : A  PROP) :  ( a, Φ a)   a,  Φ a.
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
Lemma bare_exist {A} (Φ : A  PROP) :  ( a, Φ a)   a,  Φ a.
Proof. by rewrite /bi_bare and_exist_l. Qed.

Lemma bare_sep_l P Q :  (P  Q)   P.
Proof.
  rewrite /bi_bare. apply and_intro; auto.
  by rewrite (comm _ P) emp_and_sep_assoc_1 {1}and_elim_l left_id.
Qed.
Lemma bare_sep_r P Q :  (P  Q)   Q.
Proof. by rewrite (comm _ P) bare_sep_l. Qed.

Lemma bare_True_emp :  True   emp.
Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.

Lemma bare_and_l P Q : P   Q   (P  Q).
Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
Lemma bare_and_r P Q :  P  Q   (P  Q).
Proof. by rewrite /bi_bare assoc. Qed.

(* Affine propositions *)
Global Instance Affine_proper : Proper (() ==> iff) (@Affine PROP).
Proof. solve_proper. Qed.

Global Instance emp_affine_l : Affine (emp%I : PROP).
Proof. by rewrite /Affine. Qed.
Global Instance and_affine_l P Q : Affine P  Affine (P  Q).
Proof. rewrite /Affine=> ->; auto. Qed.
Global Instance and_affine_r P Q : Affine Q  Affine (P  Q).
Proof. rewrite /Affine=> ->; auto. Qed.
Global Instance or_affine P Q : Affine P  Affine Q  Affine (P  Q).
Proof.  rewrite /Affine=> -> ->; auto. Qed.
Global Instance forall_affine `{Inhabited A} (Φ : A  PROP) :
  ( x, Affine (Φ x))  Affine ( x, Φ x).
Proof. intros. rewrite /Affine (forall_elim inhabitant). apply: affine. Qed.
Global Instance exist_affine {A} (Φ : A  PROP) :
  ( x, Affine (Φ x))  Affine ( x, Φ x).
Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
Global Instance sep_affine P Q : Affine P  Affine Q  Affine (P  Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.

Global Instance bare_affine P : Affine ( P).
Proof. rewrite /bi_bare. apply _. Qed.

(* Absorbing propositions *)
Global Instance Absorbing_proper : Proper (() ==> iff) (@Absorbing PROP).
Proof. intros P P' HP. apply base.forall_proper=> Q. by rewrite HP. Qed.

Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
Proof.
  intros R. apply wand_elim_l', pure_elim'=> Hφ.
  by apply wand_intro_l, pure_intro.
Qed.
Global Instance and_absorbing P Q : Absorbing P  Absorbing Q  Absorbing (P  Q).
Proof.
  rewrite /Absorbing=> HP HQ R.
  apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; auto.
Qed.
Global Instance or_absorbing P Q : Absorbing P  Absorbing Q  Absorbing (P  Q).
Proof. rewrite /Absorbing=> HP HQ R. by rewrite sep_or_r HP HQ. Qed.
Global Instance forall_absorbing {A} (Φ : A  PROP) :
  ( x, Absorbing (Φ x))  Absorbing ( x, Φ x).
Proof. rewrite /Absorbing=> ? R. rewrite sep_forall_r. auto using forall_mono. Qed.
Global Instance exist_absorbing {A} (Φ : A  PROP) :
  ( x, Absorbing (Φ x))  Absorbing ( x, Φ x).
Proof. rewrite /Absorbing=> ? R. rewrite sep_exist_r. auto using exist_mono. Qed.

Global Instance internal_eq_absorbing {A : ofeT} (a b : A) :
  Absorbing (a  b : PROP)%I.
Proof.
  intros Q.
  apply wand_elim_l', (internal_eq_rewrite' a b (λ b, Q - a  b)%I); auto.
  by apply wand_intro_l, internal_eq_refl.
Qed.

Global Instance sep_absorbing P Q : Absorbing P  Absorbing (P  Q).
Proof. rewrite /Absorbing=> HP R. by rewrite -assoc -(comm _ R) assoc HP. Qed.
Global Instance wand_absorbing P Q : Absorbing Q  Absorbing (P - Q).
Proof.
  rewrite /Absorbing=> HP R. apply wand_intro_l. by rewrite assoc wand_elim_r.
Qed.

(* Properties of affine and absorbing propositions *)
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.
Proof. intros HQ R. by rewrite -(left_id emp%I _ R) HQ right_id. Qed.

Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P  Q  P.
Proof. destruct H. by rewrite (affine Q) right_id. by rewrite absorbing. Qed.
Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P  Q  Q.
Proof. by rewrite comm sep_elim_l. Qed.

Lemma sep_and P Q `{TCOr (Affine P) (Absorbing Q), TCOr (Affine Q) (Absorbing P)} :
  P  Q  P  Q.
Proof. auto using and_intro, sep_elim_l, sep_elim_r. Qed.

Lemma affine_bare P `{!Affine P} :  P  P.
Proof. rewrite /bi_bare. apply (anti_symm _); auto. Qed.
Lemma bare_intro P Q `{!Affine P} : (P  Q)  P   Q.
Proof. intros <-. by rewrite affine_bare. Qed.

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.
Proof. apply (anti_symm _); auto using True_sep_2. by rewrite sep_elim_r. Qed.
Lemma sep_True P `{!Absorbing P} : P  True  P.
Proof. apply (anti_symm _); auto using sep_True_2. Qed.

Section affine_bi.
  Context `{AffineBI PROP}.

  Global Instance affine_bi P : Absorbing P | 0.
  Proof. intros Q. by rewrite (affine Q) right_id. Qed.

  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.
End affine_bi.

(* Properties of the persistently modality *)
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.
Global Instance persistently_absorbing P : Absorbing ( P).
Proof. rewrite /Absorbing=> R. apply persistently_absorbing. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
875 876 877 878 879 880 881 882 883
Lemma persistently_and_sep_assoc_1 P Q R :  P  (Q  R)  ( P  Q)  R.
Proof.
  rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
  apply sep_mono_l, and_intro.
  - by rewrite and_elim_r absorbing.
  - by rewrite and_elim_l left_id.
Qed.
Lemma persistently_and_emp_elim P : emp   P  P.
Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284
Lemma persistently_elim P :  P  P  True.
Proof.
  rewrite -(right_id True%I _ ( _)%I) -{1}(left_id emp%I _ True%I).
  by rewrite persistently_and_sep_assoc_1 (comm bi_and) persistently_and_emp_elim.
Qed.
Lemma persistently_elim_absorbing P `{!Absorbing P} :  P  P.
Proof. by rewrite persistently_elim sep_elim_l. Qed.

Lemma persistently_idemp_1 P :   P   P.
Proof. by rewrite persistently_elim persistently_absorbing. Qed.
Lemma persistently_idemp P :   P   P.
Proof.
  apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2.
Qed.

Lemma persistently_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. apply persistently_idemp_2. Qed.

Lemma persistently_pure φ :  ⌜φ⌝  ⌜φ⌝.
Proof.
  apply (anti_symm _).
  - by rewrite persistently_elim sep_elim_l.
  - apply pure_elim'=> Hφ.
    trans ( x : False,  True : PROP)%I; [by apply forall_intro|].
    rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Qed.
Lemma persistently_forall {A} (Ψ : A  PROP) : (  a, Ψ a)  ( a,  Ψ a).
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) : (  a, Ψ a)  ( a,  Ψ a).
Proof.
  apply (anti_symm _); auto using persistently_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma persistently_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
Lemma persistently_or P Q :  (P  Q)   P   Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Lemma persistently_impl P Q :  (P  Q)   P   Q.
Proof.
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
Qed.

Lemma persistently_internal_eq {A : ofeT} (a b : A) :  (a  b)  a  b.
Proof.
  apply (anti_symm ()); auto using persistently_elim.
  - rewrite persistently_elim. apply wand_elim_l'.
    apply (internal_eq_rewrite' a b (λ b, True - a  b)%I); auto using wand_intro_l.
  - apply (internal_eq_rewrite' a b (λ b,  (a  b))%I); auto.
    rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
Qed.

Lemma persistently_sep_dup P :  P   P   P.
Proof.
  apply (anti_symm _); last by eauto using sep_elim_l with typeclass_instances.
  rewrite -{1}(idemp bi_and ( _)%I) -{2}(left_id emp%I _ ( _)%I).
  by rewrite persistently_and_sep_assoc_1 and_elim_l.
Qed.

Lemma persistently_and_sep_assoc P Q R :  P  (Q  R)  ( P  Q)  R.
Proof.
  apply (anti_symm ()); auto using persistently_and_sep_assoc_1.
  apply and_intro.
  - by rewrite and_elim_l sep_elim_l.
  - by rewrite and_elim_r.
Qed.
Lemma persistently_sep_elim_l P Q :  (P  Q)   P.
Proof.
  rewrite -(left_id True%I bi_and ( _)%I) (persistently_emp_intro True%I).
  by rewrite -persistently_and (comm bi_sep) emp_and_sep_assoc_1 and_elim_l left_id.
Qed.
Lemma persistently_sep_elim_r P Q :  (P  Q)   Q.
Proof. by rewrite comm persistently_sep_elim_l. Qed.

Lemma persistently_and_sep_l_1 P Q :  P  Q   P  Q.
Proof.
  by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
Qed.
Lemma persistently_and_sep_r_1 P Q : P   Q  P   Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.

Lemma persistently_True_emp :  True   emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
Lemma persistently_and_sep P Q :  (P  Q)   (P  Q).
Proof.
  rewrite persistently_and. apply (anti_symm ()).
  - 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.
  - auto using persistently_sep_elim_l, persistently_sep_elim_r.
Qed.

Lemma and_sep_persistently P Q :  P   Q   P   Q.
Proof.
  apply (anti_symm _).
  - auto using persistently_and_sep_l_1.
  - eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
Qed.
Lemma persistently_sep P Q :  (P  Q)   P   Q.
Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.

Lemma persistently_wand P Q :  (P - Q)   P -  Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.

Lemma persistently_entails_l P Q : (P   Q)  P   Q  P.
Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
Lemma persistently_entails_r P Q : (P   Q)  P  P   Q.
Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.

Lemma persistently_impl_wand_2 P Q :  (P - Q)   (P  Q).
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.

Section persistently_bare_bi.
  Context `{AffineBI PROP}.

  Lemma persistently_emp :  emp  emp.
  Proof. by rewrite -!True_emp persistently_pure. Qed.

  Lemma persistently_and_sep_l P Q :  P  Q   P  Q.
  Proof.
    apply (anti_symm ());
      eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
  Qed.
  Lemma persistently_and_sep_r P Q : P   Q  P   Q.
  Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.

  Lemma persistently_impl_wand P Q :  (P  Q)   (P - Q).
  Proof.
    apply (anti_symm ()); auto using persistently_impl_wand_2.
    apply persistently_intro', wand_intro_l.
    by rewrite -persistently_and_sep_r persistently_elim_absorbing impl_elim_r.
  Qed.

  Lemma wand_alt P Q : (P - Q)   R, R   (P  R  Q).
  Proof.
    apply (anti_symm ()).
    - rewrite -(right_id True%I bi_sep (P - Q)%I) -(exist_intro (P - Q)%I).
      apply sep_mono_r. rewrite -persistently_pure.
      apply persistently_intro', impl_intro_l.
      by rewrite wand_elim_r persistently_pure right_id.
    - apply exist_elim=> R. apply wand_intro_l.
      rewrite assoc -persistently_and_sep_r.
      by rewrite persistently_elim_absorbing impl_elim_r.
  Qed.
  Lemma impl_alt P Q : (P  Q)   R, R   (P  R - Q).
  Proof.
    apply (anti_symm ()).
    - rewrite -(right_id True%I bi_and (P  Q)%I) -(exist_intro (P  Q)%I).
      apply and_mono_r. rewrite -persistently_pure.
      apply persistently_intro', wand_intro_l.
      by rewrite impl_elim_r persistently_pure right_id.
    - apply exist_elim=> R. apply impl_intro_l.
      rewrite assoc persistently_and_sep_r.
      by rewrite persistently_elim_absorbing wand_elim_r.
  Qed.
End persistently_bare_bi.

(* The combined bare persistently modality *)
Lemma persistently_bare P :   P   P.
Proof.
  by rewrite /bi_bare persistently_and -persistently_True_emp
             persistently_pure left_id.
Qed.

Lemma bare_persistently_elim P :  P  P.
Proof. apply persistently_and_emp_elim. Qed.
Lemma bare_persistently_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. by rewrite persistently_bare persistently_idemp. Qed.

Lemma bare_persistently_emp :  emp  emp.
Proof.
  by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp.
Qed.
Lemma bare_persistently_and P Q :  (P  Q)   P   Q.
Proof. by rewrite persistently_and bare_and. Qed.
Lemma bare_persistently_or P Q :  (P  Q)   P   Q.
Proof. by rewrite persistently_or bare_or. Qed.
Lemma bare_persistently_exist {A} (Φ : A  PROP) :  ( x, Φ x)   x,  Φ x.
Proof. by rewrite persistently_exist bare_exist. Qed.
Lemma bare_persistently_sep P Q :  (P  Q)   P   Q.
Proof. by rewrite persistently_sep bare_sep. Qed.

Lemma bare_persistently_idemp P :   P   P.
Proof. by rewrite persistently_bare persistently_idemp. Qed.

Lemma bare_persistently_sep_dup P :  P   P   P.
Proof. by rewrite {1}persistently_sep_dup bare_sep. Qed.

Lemma persistently_and_bare_sep_l P Q :  P  Q   P  Q.
Proof.
  apply (anti_symm _).
  - by rewrite /bi_bare -(comm bi_and ( P)%I) -persistently_and_sep_assoc left_id.
  - apply and_intro. by rewrite bare_elim sep_elim_l. by rewrite sep_elim_r.
Qed.
Lemma persistently_and_bare_sep_r P Q : P   Q  P   Q.
Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.

(* Conditional bare modality *)
Global Instance bare_if_ne p : NonExpansive (@bi_bare_if PROP p).
Proof. solve_proper. Qed.
Global Instance bare_if_proper p : Proper (() ==> ()) (@bi_bare_if PROP p).
Proof. solve_proper. Qed.
Global Instance bare_if_mono' p : Proper (() ==> ()) (@bi_bare_if PROP p).
Proof. solve_proper. Qed.
Global Instance bare_if_flip_mono' p :
  Proper (flip () ==> flip ()) (@bi_bare_if PROP p).
Proof. solve_proper. Qed.

Lemma bare_if_mono p P Q : (P  Q)  ?p P  ?p Q.
Proof. by intros ->. Qed.

Lemma bare_if_elim p P : ?p P  P.
Proof. destruct p; simpl; auto using bare_elim. Qed.
Lemma bare_bare_if p P :  P  ?p P.
Proof. destruct p; simpl; auto using bare_elim. Qed.
Lemma bare_if_intro' p P Q : (?p P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_intro'. Qed.

Lemma bare_if_emp p : ?p emp  emp.
Proof. destruct p; simpl; auto using bare_emp. Qed.
Lemma bare_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_and. Qed.
Lemma bare_if_or p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_or. Qed.
Lemma bare_if_exist {A} p (Ψ : A  PROP) : (?p  a, Ψ a)   a, ?p Ψ a.
Proof. destruct p; simpl; auto using bare_exist. Qed.
Lemma bare_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_sep. Qed.

Lemma bare_if_idemp p P : ?p ?p P  ?p P.
Proof. destruct p; simpl; auto using bare_idemp. Qed.

(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
Global Instance persistently_if_proper p :
  Proper (() ==> ()) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
Global Instance persistently_if_mono' p :
  Proper (() ==> ()) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
Global Instance persistently_if_flip_mono' p :
  Proper (flip () ==> flip ()) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.

Lemma persistently_if_mono p P Q : (P  Q)  ?p P  ?p Q.
Proof. by intros ->. Qed.

Lemma persistently_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
Lemma persistently_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
Lemma persistently_if_or p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.
Lemma persistently_if_exist {A} p (Ψ : A  PROP) : (?p  a, Ψ a)   a, ?p Ψ a.
Proof. destruct p; simpl; auto using persistently_exist. Qed.
Lemma persistently_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.

Lemma persistently_if_idemp p P : ?p ?p P  ?p P.
Proof. destruct p; simpl; auto using persistently_idemp. Qed.

(* Conditional bare persistently *)
Lemma bare_persistently_if_mono p P Q : (P  Q)  ?p P  ?p Q.
Proof. by intros ->. Qed.

Lemma bare_persistently_if_elim p P : ?p P  P.
Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
Lemma bare_persistently_bare_persistently_if p P :  P  ?p P.
Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
Lemma bare_persistently_if_intro' p P Q : (?p P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_persistently_intro'. Qed.

Lemma bare_persistently_if_emp p : ?p emp  emp.
Proof. destruct p; simpl; auto using bare_persistently_emp. Qed.
Lemma bare_persistently_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_persistently_and. Qed.
Lemma bare_persistently_if_or p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
Lemma bare_persistently_if_exist {A} p (Ψ : A  PROP) :
  (?p  a, Ψ a)   a, ?p Ψ a.
Proof. destruct p; simpl; auto using bare_persistently_exist. Qed.
Lemma bare_persistently_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using bare_persistently_sep. Qed.

Lemma bare_persistently_if_idemp p P : ?p ?p P  ?p P.
Proof. destruct p; simpl; auto using bare_persistently_idemp. Qed.

(* Persistence *)
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent PROP).
Proof. solve_proper. Qed.
Lemma persistent_absorbing P : Persistent P  Absorbing P.
Proof. rewrite /Persistent=> <-. apply _. Qed.
Hint Immediate persistent_absorbing : typeclass_instances.

Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
Proof. by rewrite /Persistent persistently_pure. Qed.
Global Instance emp_persistent `{AffineBI PROP} : Persistent (emp%I : PROP).
Proof. rewrite -True_emp. apply _. Qed.
Global Instance persistently_persistent P : Persistent ( P).
Proof. apply persistently_idemp. Qed.
Global Instance and_persistent P Q :
  Persistent P  Persistent Q  Persistent (P  Q).
Proof. intros. by rewrite /Persistent persistently_and !persistent. Qed.
Global Instance or_persistent P Q :
  Persistent P  Persistent Q  Persistent (P  Q).
Proof. intros. by rewrite /Persistent persistently_or !persistent. Qed.
Global Instance forall_persistent {A} (Ψ : A  PROP) :
  ( x, Persistent (Ψ x))  Persistent ( x, Ψ x).
Proof.
  intros. rewrite /Persistent persistently_forall.
  apply forall_proper=> x. by rewrite !persistent.
Qed.
Global Instance exist_persistent {A} (Ψ : A  PROP) :
  ( x, Persistent (Ψ x))  Persistent ( x, Ψ x).
Proof.
  intros. rewrite /Persistent persistently_exist.
  apply exist_proper=> x. by rewrite !persistent.
Qed.

Global Instance internal_eq_persistent {A