Simplify persistent predicates as Robbert suggested

theories/logrel/persistent_pred.v

@@ -18,42 +18,26 @@ Section persistent_pred.
   Global Instance persistent_pred_dist : Dist persistent_pred :=
     λ n Φ Φ', ∀ x, Φ x ≡{n}≡ Φ' x.
   Definition persistent_pred_ofe_mixin : OfeMixin persistent_pred.
-  Proof.
-    split.
-    - intros ? ?; split; first by intros Heq ? ?; rewrite Heq.
-      intros Heq ?; apply equiv_dist; intros ?; apply Heq.
-    - intros n; split.
-      + by intros ? ?.
-      + by intros ? ? ? ?.
-      + by intros ? ? ? ? ? ?; etrans; eauto.
-    - intros ? ? ? ? ?; apply dist_S; done.
-  Qed.
-
+  Proof. by apply (iso_ofe_mixin (pers_pred_car : _ → A -d> _)). Qed.
   Global Canonical Structure persistent_predC :=
     OfeT persistent_pred persistent_pred_ofe_mixin.
 
-  Program Definition persistent_pred_chain (c : chain persistent_predC) (x : A)
-    : chain (uPredO M) := {| chain_car n := c n x |}.
-  Next Obligation. intros c vv n i ?. by apply (chain_cauchy c). Qed.
-  Program Definition persistent_pred_compl : Compl persistent_predC := λ c,
-    {| pers_pred_car x := compl (persistent_pred_chain c x) |}.
-  Next Obligation. intros c x. eapply @limit_preserving; apply _. Qed.
-
-  Global Program Instance persistent_pred_cofe : Cofe persistent_predC :=
-    {| compl := persistent_pred_compl |}.
-  Next Obligation.
-    intros ? ? ?.
-    rewrite /persistent_pred_compl /pers_pred_car /=.
-    rewrite conv_compl; done.
+  Global Instance persistent_pred_cofe : Cofe persistent_predC.
+  Proof.
+    apply (iso_cofe_subtype' (λ Φ : A -d> uPredO M, ∀ w, Persistent (Φ w))
+      PersPred pers_pred_car)=> //.
+    - apply _.
+    - apply limit_preserving_forall=> w.
+      by apply bi.limit_preserving_Persistent=> n ??.
   Qed.
 
   Global Instance pers_pred_car_ne n :
-    Proper (dist n ==> @dist A (@discrete_dist A (@equivL A)) n ==> dist n)
+    Proper (dist n ==> (=) ==> dist n)
       pers_pred_car.
-  Proof. intros f g Hfg ? ? ->; apply Hfg. Qed.
+  Proof. by intros ? ? ? ? ? ->. Qed.
   Global Instance pers_pred_car_proper :
-    Proper ((≡) ==> @equivL A ==> (≡)) pers_pred_car :=
-    (@ne_proper_2 _ (leibnizO A) _ pers_pred_car _).
+    Proper ((≡) ==> (=) ==> (≡)) pers_pred_car.
+  Proof. by intros ? ? ? ? ? ->. Qed.
 
   Lemma domain_ext (f g : persistent_pred) : f ≡ g ↔ ∀ x, f x ≡ g x.
   Proof. done. Qed.