From 05817be7741e8ce6db55ff76d74c1da40814e039 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 19 May 2016 15:08:57 +0200
Subject: [PATCH] show that we can rewrite below a contractive function even if
 we have an equality only later

---
 algebra/upred.v | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index c69ac0146..c44d09318 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -497,10 +497,11 @@ Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 Lemma eq_refl {A : cofeT} (a : A) : True ⊢ (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
 Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
-  `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊢ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
+  {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊢ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
 Proof.
-  unseal; intros Hab Ha; split=> n x ??.
-  apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
+  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
+  - by symmetry; apply Hab with x.
+  - by apply Ha.
 Qed.
 Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
   True ⊢ (a ≡ b) → a ≡ b.
@@ -508,6 +509,14 @@ Proof.
   unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
   apply cmra_valid_validN, cmra_unit_valid.
 Qed.
+Lemma eq_rewrite_contractive {A : cofeT} 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.
 
 (* Derived logical stuff *)
 Lemma False_elim P : False ⊢ P.
-- 
GitLab