From ecd304f24f42f7a6d22bc279318e76c484e93409 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Dec 2016 17:20:47 +0100
Subject: [PATCH] Internal definition of contractive and use it to prove
 internal_eq_rewrite.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This removes Ralf's hack of using later_car, which is not function in the logic.

Thanks to Aleš for suggesting this.
---
 algebra/ofe.v          |  7 -------
 base_logic/derived.v   |  6 ++----
 base_logic/primitive.v | 10 ++++++++++
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index 7b08c03cc..8812dc5ff 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -770,13 +770,6 @@ 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 81d253997..7361ad147 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -290,10 +290,8 @@ Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qe
 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.
+  move: HΨ=> /contractiveI HΨ Heq ?.
+  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
 Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 033d562e5..510424fe4 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -581,6 +581,16 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. unseal. by destruct mx. Qed.
 
+(* Contractive functions *)
+Lemma contractiveI {A B : ofeT} (f : A → B) :
+  Contractive f ↔ (∀ x y, ▷ (x ≡ y) ⊢ f x ≡ f y).
+Proof.
+  split; unseal; intros Hf.
+  - intros x y; split=> -[|n] z _ /=; eauto using contractive_0, contractive_S.
+  - intros [|i] x y Hxy; apply (uPred_in_entails _ _ (Hf x y) _ ∅);
+      simpl; eauto using ucmra_unit_validN.
+Qed.
+
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
-- 
GitLab