From b61305aee93e71c5aaa2e92e944acbf00ce2c05b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 May 2018 15:07:10 +0200
Subject: [PATCH] factor out entails_eq_True as its own lemma

---
 theories/bi/derived_laws_bi.v | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 0143774a7..ff5a64e6f 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -113,6 +113,16 @@ Lemma True_intro P : P ⊢ True.
 Proof. by apply pure_intro. Qed.
 Hint Immediate False_elim.
 
+Lemma entails_eq_True P Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I).
+Proof.
+  split=>EQ.
+  - apply bi.equiv_spec; split; [by apply True_intro|].
+    apply impl_intro_r. rewrite and_elim_r //.
+  - trans (P ∧ True)%I.
+    + apply and_intro; first done. by apply pure_intro.
+    + rewrite -EQ impl_elim_r. done.
+Qed.
+
 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'.
@@ -1428,13 +1438,8 @@ Qed.
 Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x).
 Proof.
-  intros HΦ HΨ c Hc.
-  assert (Heq : ∀ P Q : PROP, (∀ n, (P → Q)%I ≡{n}≡ True%I) ↔ (P -∗ Q)).
-  { intros ??. rewrite -equiv_dist. split=>EQ.
-    - by rewrite -(left_id True%I bi_and P) -EQ impl_elim_l.
-    - apply bi.equiv_spec; split; [by apply True_intro|].
-      apply impl_intro_l. by rewrite right_id. }
-  apply Heq=>n. rewrite conv_compl. by apply Heq.
+  intros HΦ HΨ c Hc. apply entails_eq_True, equiv_dist=>n.
+  rewrite conv_compl. apply equiv_dist, entails_eq_True. done.
 Qed.
 Lemma limit_preserving_equiv {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
-- 
GitLab