Internal definition of contractive and use it to prove internal_eq_rewrite.

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

@@ -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.

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).

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.