From 9312ad020577331548775205f94ce26297971f0a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 6 Aug 2019 19:34:10 +0200
Subject: [PATCH] Clearer statement for propositional extensionality

- And use prop_ext instead of prop_ext_2 in other proofs.
---
 CHANGELOG.md          |  2 ++
 theories/bi/monpred.v |  2 +-
 theories/bi/plainly.v | 15 ++++++++++++---
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 81f2ec071..658317801 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 3ae1afcc4..0cb22093c 100644
--- a/theories/bi/monpred.v
+++ b/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_2 !(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 /=.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index e8d391113..c270a8422 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -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_2. 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_2. 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_2. 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.
-- 
GitLab