derive internal_eq_rewrite_contractive inside the logic

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.

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.

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.