Easier way to construct OFEs that are isomorphic to an existing OFE.

theories/algebra/auth.v

@@ -37,25 +37,13 @@ Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
 Proof. by destruct 1. Qed.
 
 Definition auth_ofe_mixin : OfeMixin (auth A).
-Proof.
-  split.
-  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
-    rewrite !equiv_dist; naive_solver.
-  - intros n; split.
-    + by intros ?; split.
-    + by intros ?? [??]; split; symmetry.
-    + intros ??? [??] [??]; split; etrans; eauto.
-  - by intros ? [??] [??] [??]; split; apply dist_S.
-Qed.
+Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
 Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
 
-Definition auth_compl `{Cofe A} : Compl authC := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
-Global Program Instance auth_cofe `{Cofe A} : Cofe authC :=
-  {| compl := auth_compl |}.
-Next Obligation.
-  intros ? n c; split. apply (conv_compl n (chain_map authoritative c)).
-  apply (conv_compl n (chain_map auth_own c)).
+Global Instance auth_cofe `{Cofe A} : Cofe authC.
+Proof.
+  apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
+    (λ x, (authoritative x, auth_own x))); by repeat intro.
 Qed.
 
 Global Instance Auth_timeless a b :

theories/algebra/excl.v

@@ -46,29 +46,16 @@ Proof. by inversion_clear 1. Qed.
 
 Definition excl_ofe_mixin : OfeMixin (excl A).
 Proof.
-  split.
-  - intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
-    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
-    by intros n; feed inversion (Hxy n).
-  - intros n; split.
-    + by intros []; constructor.
-    + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
+  apply (iso_ofe_mixin (maybe Excl)).
+  - by intros [a|] [b|]; split; inversion_clear 1; constructor.
+  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
 Qed.
 Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
 
-Program Definition excl_chain (c : chain exclC) (a : A) : chain A :=
-  {| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
-Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Definition excl_compl `{Cofe A} : Compl exclC := λ c,
-  match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end.
-Global Program Instance excl_cofe `{Cofe A} : Cofe exclC :=
-  {| compl := excl_compl |}.
-Next Obligation.
-  intros ? n c; rewrite /compl /excl_compl.
-  feed inversion (chain_cauchy c 0 n); auto with omega.
-  rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
+Global Instance excl_cofe `{Cofe A} : Cofe exclC.
+Proof.
+  apply (iso_cofe (from_option Excl ExclBot) (maybe Excl));
+    [by destruct 1; constructor..|by intros []; constructor].
 Qed.
 
 Global Instance excl_discrete : Discrete A → Discrete exclC.

theories/algebra/ofe.v

@@ -553,6 +553,26 @@ Section unit.
   Proof. done. Qed.
 End unit.
 
+Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A)
+  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
+  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
+Proof.
+  split.
+  - intros y1 y2. rewrite g_equiv. setoid_rewrite g_dist. apply equiv_dist.
+  - split.
+    + intros y. by apply g_dist.
+    + intros y1 y2. by rewrite !g_dist.
+    + intros y1 y2 y3. rewrite !g_dist. intros ??; etrans; eauto.
+  - intros n y1 y2. rewrite !g_dist. apply dist_S.
+Qed.
+
+Program Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A)
+    `(!NonExpansive g, !NonExpansive f) (fg : ∀ y, f (g y) ≡ y) : Cofe B :=
+  {| compl c := f (compl (chain_map g c)) |}.
+Next Obligation.
+  intros A B ? f g ?? fg n c. by rewrite /= conv_compl /= fg.
+Qed.
+
 (** Product *)
 Section product.
   Context {A B : ofeT}.
@@ -1084,14 +1104,7 @@ Section sigma.
   Global Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
   Proof. by intros n [a Ha] [b Hb] ?. Qed.
   Definition sig_ofe_mixin : OfeMixin (sig P).
-  Proof.
-    split.
-    - intros [a ?] [b ?]. rewrite /dist /sig_dist /equiv /sig_equiv /=.
-      apply equiv_dist.
-    - intros n. rewrite /dist /sig_dist.
-      split; [intros []| intros [] []| intros [] [] []]=> //= -> //.
-    - intros n [a ?] [b ?]. rewrite /dist /sig_dist /=. apply dist_S.
-  Qed.
+  Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
   Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
 
   (* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving