Merge branch 'prop_ext_clearer' into 'master'

Clearer statement for propositional extensionality

See merge request iris/iris!296

CHANGELOG.md

@@ -159,6 +159,8 @@ Changes in Coq:
   fractional camera (`frac_auth`) with unbounded fractions.
 * Changed `frac_auth` notation from `●!`/`◯!` to `●F`/`◯F`. sed script:
   `s/◯!/◯F/g; s/●!/●F/g;`.
+* Lemma `prop_ext` works in both directions; its default direction is the
+  opposite of what it used to be.
 * Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
   rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
   `-d>`. The renaming can be automatically done using the following script (on

theories/base_logic/bi.v

@@ -121,7 +121,7 @@ Proof.
     etrans; first exact: sep_comm'.
     apply sep_mono; last done.
     exact: pure_intro.
-  - exact: prop_ext.
+  - exact: prop_ext_2.
   - exact: later_plainly_1.
   - exact: later_plainly_2.
 Qed.

theories/base_logic/upred.v

@@ -617,7 +617,7 @@ Proof. by unseal. Qed.
 Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
 Proof. by unseal. Qed.
 
-Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
 Proof.
   unseal; split=> n x ? /= HPQ. split=> n' x' ??.
     move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.

theories/bi/monpred.v

@@ -923,7 +923,7 @@ Proof.
   - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q. split=> i /=. rewrite (monPred_equivI P Q). f_equiv=> j.
-    by rewrite -prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+    by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
   - intros P. split=> i /=.
     rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
   - intros P. split=> i /=.

theories/bi/plainly.v

@@ -29,7 +29,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■ emp;
   bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■ P ∗ Q ⊢ ■ P;
 
-  bi_plainly_mixin_prop_ext (P Q : PROP) : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
+  bi_plainly_mixin_prop_ext_2 (P Q : PROP) : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
 
   bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■ P ⊢ ■ ▷ P;
   bi_plainly_mixin_later_plainly_2 (P : PROP) : ■ ▷ P ⊢ ▷ ■ P;
@@ -74,8 +74,8 @@ Section plainly_laws.
   Lemma plainly_emp_intro P : P ⊢ ■ emp.
   Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
 
-  Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-  Proof. eapply bi_plainly_mixin_prop_ext, bi_plainly_mixin. Qed.
+  Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+  Proof. eapply bi_plainly_mixin_prop_ext_2, bi_plainly_mixin. Qed.
 
   Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
   Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
@@ -467,10 +467,19 @@ Proof.
   rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
 Qed.
 
+Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+Proof.
+  apply (anti_symm (⊢)); last exact: prop_ext_2.
+  apply (internal_eq_rewrite' P Q (λ Q, ■ (P ∗-∗ Q))%I);
+    [ solve_proper | done | ].
+  rewrite (plainly_emp_intro (P ≡ Q)%I).
+  apply plainly_mono, wand_iff_refl.
+Qed.
+
 Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
 Proof.
   rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
     + by rewrite affinely_elim_emp left_id.
     + by rewrite left_id.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
@@ -480,7 +489,7 @@ Qed.
 Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
     by rewrite plainly_pure True_impl.
 Qed.
@@ -488,7 +497,7 @@ Qed.
 Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
     by rewrite wand_elim_r.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _
       (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.