From 965852ff6c063dcb0178ba5eac1b8e19c5bf3ea4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Dec 2016 12:54:18 +0100
Subject: [PATCH] derive internal_eq_rewrite_contractive inside the logic

---
 algebra/ofe.v          |  7 +++++++
 base_logic/derived.v   |  8 ++++++++
 base_logic/primitive.v | 10 +---------
 3 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index 8812dc5ff..7b08c03cc 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -770,6 +770,13 @@ Section later.
   Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
+
+  Lemma later_car_compose_ne {B : ofeT} (f : A → B) :
+    (Contractive f) → ∀ n, Proper (dist n ==> dist n) (f ∘ later_car).
+  Proof.
+    move=> Hcont n [x] [y] /= Hxy. apply Hcont. intros m Hmn.
+    destruct n; first by (exfalso; omega). eapply dist_le', Hxy. omega.
+  Qed.
 End later.
 
 Arguments laterC : clear implicits.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index b85c482be..81d253997 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -287,6 +287,14 @@ Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. 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. solve_proper. Qed.
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
+  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+  rewrite -later_equivI. intros Heq.
+  change ((P ⊢ (Ψ ∘ later_car) (Next a)) → P ⊢ (Ψ ∘ later_car) (Next b)).
+  apply internal_eq_rewrite; last done.
+  exact: later_car_compose_ne.
+Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index ed8841b31..033d562e5 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -375,14 +375,6 @@ Proof.
   - by symmetry; apply Hab with x.
   - by apply Ha.
 Qed.
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
-    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
-  - by apply Ha.
-Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
@@ -565,7 +557,7 @@ Proof. by unseal. Qed.
 Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
-(* Later *)
+(* Type-level Later *)
 Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.
 
-- 
GitLab