Merge branch 'ofe' into 'master'

split completion from COFEs and only require it for the solver

This is the OFE part of !22 

Cc @robbertkrebbers @jjourdan

See merge request !26

CHANGELOG.md

@@ -9,6 +9,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
   is proven in the logic.
+* Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
+  recursive domain equation.  As a consequence, CMRAs no longer need a proof
+  of completeness.
 * Renaming and moving things around: uPred and the rest of the base logic are
   in [base_logic], while [program_logic] is for everything involving the
   general Iris notion of a language.

_CoqProject

@@ -43,7 +43,7 @@ algebra/cmra_tactics.v
 algebra/sts.v
 algebra/auth.v
 algebra/gmap.v
-algebra/cofe.v
+algebra/ofe.v
 algebra/base.v
 algebra/dra.v
 algebra/cofe_solver.v

algebra/agree.v

@@ -12,7 +12,7 @@ Arguments agree_car {_} _ _.
 Arguments agree_is_valid {_} _ _.
 
 Section agree.
-Context {A : cofeT}.
+Context {A : ofeT}.
 
 Instance agree_validN : ValidN (agree A) := λ n x,
   agree_is_valid x n ∧ ∀ n', n' ≤ n → agree_car x n ≡{n'}≡ agree_car x n'.
@@ -28,13 +28,7 @@ Instance agree_equiv : Equiv (agree A) := λ x y,
 Instance agree_dist : Dist (agree A) := λ n x y,
   (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
   (∀ n', n' ≤ n → agree_is_valid x n' → agree_car x n' ≡{n'}≡ agree_car y n').
-Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := agree_car (c n) n;
-     agree_is_valid n := agree_is_valid (c n) n |}.
-Next Obligation.
-  intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
-Qed.
-Definition agree_cofe_mixin : CofeMixin (agree A).
+Definition agree_ofe_mixin : OfeMixin (agree A).
 Proof.
   split.
   - intros x y; split.
@@ -47,10 +41,21 @@ Proof.
       * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
       * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
   - intros n x y Hxy; split; intros; apply Hxy; auto.
-  - intros n c; apply and_wlog_r; intros;
-      symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
-Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
+Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.
+
+Program Definition agree_compl : Compl agreeC := λ c,
+  {| agree_car n := agree_car (c n) n;
+     agree_is_valid n := agree_is_valid (c n) n |}.
+Next Obligation.
+  intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
+Qed.
+Global Program Instance agree_cofe : Cofe agreeC :=
+  {| compl := agree_compl |}.
+Next Obligation.
+  intros n c; apply and_wlog_r; intros;
+    symmetry; apply (chain_cauchy c); naive_solver.
+Qed.
 
 Program Instance agree_op : Op (agree A) := λ x y,
   {| agree_car := agree_car x;
@@ -113,7 +118,7 @@ Proof.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
 Canonical Structure agreeR : cmraT :=
-  CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
+  CMRAT (agree A) agree_ofe_mixin agree_cmra_mixin.
 
 Global Instance agree_total : CMRATotal agreeR.
 Proof. rewrite /CMRATotal; eauto. Qed.
@@ -159,7 +164,7 @@ Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
 Proof. done. Qed.
 
 Section agree_map.
-  Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Context {A B : ofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
   Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
   Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
   Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.

algebra/auth.v

@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
 
 (* COFE *)
 Section cofe.
-Context {A : cofeT}.
+Context {A : ofeT}.
 Implicit Types a : excl' A.
 Implicit Types b : A.
 Implicit Types x y : auth A.
@@ -37,9 +37,7 @@ Proof. by destruct 1. Qed.
 Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
 Proof. by destruct 1. Qed.
 
-Instance auth_compl : Compl (auth A) := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
-Definition auth_cofe_mixin : CofeMixin (auth A).
+Definition auth_ofe_mixin : OfeMixin (auth A).
 Proof.
   split.
   - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
@@ -49,10 +47,17 @@ Proof.
     + by intros ?? [??]; split; symmetry.
     + intros ??? [??] [??]; split; etrans; eauto.
   - by intros ? [??] [??] [??]; split; apply dist_S.
-  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
-    apply (conv_compl n (chain_map auth_own c)).
 Qed.
-Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
+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)).
+Qed.
 
 Global Instance Auth_timeless a b :
   Timeless a → Timeless b → Timeless (Auth a b).
@@ -151,7 +156,7 @@ Proof.
       as (b1&b2&?&?&?); auto using auth_own_validN.
     by exists (Auth ea1 b1), (Auth ea2 b2).
 Qed.
-Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
+Canonical Structure authR := CMRAT (auth A) auth_ofe_mixin auth_cmra_mixin.
 
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
@@ -171,7 +176,7 @@ Proof.
   - do 2 constructor; simpl; apply (persistent_core _).
 Qed.
 Canonical Structure authUR :=
-  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
+  UCMRAT (auth A) auth_ofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
 Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
 Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
@@ -235,13 +240,13 @@ Proof. by destruct x as [[[]|]]. Qed.
 Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
   auth_map (g ∘ f) x = auth_map g (auth_map f x).
 Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_map_ext {A B : cofeT} (f g : A → B) x :
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
   apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
 Qed.
-Instance auth_map_ne {A B : cofeT} n :
+Instance auth_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
 Proof.
   intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].

algebra/cmra.v

-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
@@ -61,34 +61,32 @@ Structure cmraT := CMRAT' {
   cmra_car :> Type;
   cmra_equiv : Equiv cmra_car;
   cmra_dist : Dist cmra_car;
-  cmra_compl : Compl cmra_car;
   cmra_pcore : PCore cmra_car;
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
-  cmra_cofe_mixin : CofeMixin cmra_car;
+  cmra_ofe_mixin : OfeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car;
   _ : Type
 }.
-Arguments CMRAT' _ {_ _ _ _ _ _ _} _ _ _.
+Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
 Notation CMRAT A m m' := (CMRAT' A m m' A).
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
-Arguments cmra_compl : simpl never.
 Arguments cmra_pcore : simpl never.
 Arguments cmra_op : simpl never.
 Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
-Arguments cmra_cofe_mixin : simpl never.
+Arguments cmra_ofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
 Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
 Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
 Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
 Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
-Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
-Canonical Structure cmra_cofeC.
+Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
+Canonical Structure cmra_ofeC.
 
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
@@ -160,36 +158,34 @@ Structure ucmraT := UCMRAT' {
   ucmra_car :> Type;
   ucmra_equiv : Equiv ucmra_car;
   ucmra_dist : Dist ucmra_car;
-  ucmra_compl : Compl ucmra_car;
   ucmra_pcore : PCore ucmra_car;
   ucmra_op : Op ucmra_car;
   ucmra_valid : Valid ucmra_car;
   ucmra_validN : ValidN ucmra_car;
   ucmra_empty : Empty ucmra_car;
-  ucmra_cofe_mixin : CofeMixin ucmra_car;
+  ucmra_ofe_mixin : OfeMixin ucmra_car;
   ucmra_cmra_mixin : CMRAMixin ucmra_car;
   ucmra_mixin : UCMRAMixin ucmra_car;
   _ : Type;
 }.
-Arguments UCMRAT' _ {_ _ _ _ _ _ _ _} _ _ _ _.
+Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
 Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
 Arguments ucmra_car : simpl never.
 Arguments ucmra_equiv : simpl never.
 Arguments ucmra_dist : simpl never.
-Arguments ucmra_compl : simpl never.
 Arguments ucmra_pcore : simpl never.
 Arguments ucmra_op : simpl never.
 Arguments ucmra_valid : simpl never.
 Arguments ucmra_validN : simpl never.
-Arguments ucmra_cofe_mixin : simpl never.
+Arguments ucmra_ofe_mixin : simpl never.
 Arguments ucmra_cmra_mixin : simpl never.
 Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmraT.
 Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
-Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
-Canonical Structure ucmra_cofeC.
+Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
+Canonical Structure ucmra_ofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
-  CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
+  CMRAT A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
 Canonical Structure ucmra_cmraR.
 
 (** Lifting properties from the mixin *)
@@ -687,7 +683,7 @@ Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
 
 (** Functors *)
 Structure rFunctor := RFunctor {
-  rFunctor_car : cofeT → cofeT → cmraT;
+  rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
   rFunctor_ne A1 A2 B1 B2 n :
@@ -705,7 +701,7 @@ Instance: Params (@rFunctor_map) 5.
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
 
-Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
+Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
@@ -716,7 +712,7 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
 Structure urFunctor := URFunctor {
-  urFunctor_car : cofeT → cofeT → ucmraT;
+  urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
   urFunctor_ne A1 A2 B1 B2 n :
@@ -734,7 +730,7 @@ Instance: Params (@urFunctor_map) 5.
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
 
-Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
+Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
 Coercion urFunctor_diag : urFunctor >-> Funclass.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
@@ -790,7 +786,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 Section discrete.
   Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
   Context (ra_mix : RAMixin A).
-  Existing Instances discrete_dist discrete_compl.
+  Existing Instances discrete_dist.
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -802,9 +798,9 @@ Section discrete.
 End discrete.
 
 Notation discreteR A ra_mix :=
-  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
+  (CMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix)).
 Notation discreteUR A ra_mix ucmra_mix :=
-  (UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
+  (UCMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
 
 Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
   @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
@@ -843,13 +839,13 @@ Section unit.
   Instance unit_op : Op () := λ x y, ().
   Lemma unit_cmra_mixin : CMRAMixin ().
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
-  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
+  Canonical Structure unitR : cmraT := CMRAT () unit_ofe_mixin unit_cmra_mixin.
 
   Instance unit_empty : Empty () := ().
   Lemma unit_ucmra_mixin : UCMRAMixin ().
   Proof. done. Qed.
   Canonical Structure unitUR : ucmraT :=
-    UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.
+    UCMRAT () unit_ofe_mixin unit_cmra_mixin unit_ucmra_mixin.
 
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. done. Qed.
@@ -993,7 +989,7 @@ Section prod.
       by exists (z11,z21), (z12,z22).
   Qed.
   Canonical Structure prodR :=
-    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
+    CMRAT (A * B) prod_ofe_mixin prod_cmra_mixin.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
   Proof. done. Qed.
@@ -1032,7 +1028,7 @@ Section prod_unit.
     - rewrite prod_pcore_Some'; split; apply (persistent _).
   Qed.
   Canonical Structure prodUR :=
-    UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.
+    UCMRAT (A * B) prod_ofe_mixin prod_cmra_mixin prod_ucmra_mixin.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
@@ -1166,7 +1162,7 @@ Section option.
       + exists None, None; repeat constructor.
   Qed.
   Canonical Structure optionR :=
-    CMRAT (option A) option_cofe_mixin option_cmra_mixin.
+    CMRAT (option A) option_ofe_mixin option_cmra_mixin.
 
   Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
   Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
@@ -1175,7 +1171,7 @@ Section option.
   Lemma option_ucmra_mixin : UCMRAMixin optionR.
   Proof. split. done. by intros []. done. Qed.
   Canonical Structure optionUR :=
-    UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
+    UCMRAT (option A) option_ofe_mixin option_cmra_mixin option_ucmra_mixin.
 
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.

algebra/cofe_solver.v

-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 
 Record solution (F : cFunctor) := Solution {
-  solution_car :> cofeT;
+  solution_car :> ofeT;
+  solution_cofe : Cofe solution_car;
   solution_unfold : solution_car -n> F solution_car;
   solution_fold : F solution_car -n> solution_car;
   solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
@@ -9,14 +10,17 @@ Record solution (F : cFunctor) := Solution {
 }.
 Arguments solution_unfold {_} _.
 Arguments solution_fold {_} _.
+Existing Instance solution_cofe.
 
 Module solver. Section solver.
 Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
-        `{Finhab : Inhabited (F unitC)}.
+        `{Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)} `{Finh : Inhabited (F unitC)}.
 Notation map := (cFunctor_map F).
 
-Fixpoint A (k : nat) : cofeT :=
+Fixpoint A (k : nat) : ofeT :=
   match k with 0 => unitC | S k => F (A k) end.
+Local Instance: ∀ k, Cofe (A k).
+Proof. induction 0; apply _. Defined.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
@@ -47,17 +51,7 @@ Record tower := {
 }.
 Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
 Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
-Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) :=
-  {| chain_car i := c i k |}.
-Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
-Program Instance tower_compl : Compl tower := λ c,
-  {| tower_car n := compl (tower_chain c n) |}.
-Next Obligation.
-  intros c k; apply equiv_dist=> n.
-  by rewrite (conv_compl n (tower_chain c k))
-    (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
-Qed.
-Definition tower_cofe_mixin : CofeMixin tower.
+Definition tower_ofe_mixin : OfeMixin tower.
 Proof.
   split.
   - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
@@ -68,10 +62,24 @@ Proof.
     + by intros X Y Z ?? n; trans (Y n).
   - intros k X Y HXY n; apply dist_S.
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
-  - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
-    apply (chain_cauchy c); lia.
 Qed.
-Definition T : cofeT := CofeT tower tower_cofe_mixin.
+Definition T : ofeT := OfeT tower tower_ofe_mixin.
+
+Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
+  {| chain_car i := c i k |}.
+Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
+Program Definition tower_compl : Compl T := λ c,
+  {| tower_car n := compl (tower_chain c n) |}.
+Next Obligation.
+  intros c k; apply equiv_dist=> n.
+  by rewrite (conv_compl n (tower_chain c k))
+    (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
+Qed.
+Global Program Instance tower_cofe : Cofe T := { compl := tower_compl }.
+Next Obligation.
+  intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
+  apply (chain_cauchy c); lia.
+Qed.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
   match i with 0 => cid | S i => f (i + k) ◎ ff i end.
@@ -197,7 +205,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
 Proof.
-  apply (Solution F T (CofeMor unfold) (CofeMor fold)).
+  apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).

algebra/csum.v

@@ -22,7 +22,7 @@ Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
   match x with Cinr b => Some b | _ => None end.
 
 Section cofe.
-Context {A B : cofeT}.
+Context {A B : ofeT}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -55,19 +55,7 @@ Proof. by inversion_clear 1. Qed.
 Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
 Proof. by inversion_clear 1. Qed.
 
-Program Definition csum_chain_l (c : chain (csum A B)) (a : A) : chain A :=
-  {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
-Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Program Definition csum_chain_r (c : chain (csum A B)) (b : B) : chain B :=
-  {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
-Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Instance csum_compl : Compl (csum A B) := λ c,
-  match c 0 with
-  | Cinl a => Cinl (compl (csum_chain_l c a))
-  | Cinr b => Cinr (compl (csum_chain_r c b))
-  | CsumBot => CsumBot
-  end.
-Definition csum_cofe_mixin : CofeMixin (csum A B).
+Definition csum_ofe_mixin : OfeMixin (csum A B).
 Proof.
   split.
   - intros mx my; split.
@@ -79,12 +67,30 @@ Proof.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
-  - intros n c; rewrite /compl /csum_compl.
-    feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-    + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
-    + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure csumC : cofeT := CofeT (csum A B) csum_cofe_mixin.
+Canonical Structure csumC : ofeT := OfeT (csum A B) csum_ofe_mixin.
+
+Program Definition csum_chain_l (c : chain csumC) (a : A) : chain A :=
+  {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
+Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+Program Definition csum_chain_r (c : chain csumC) (b : B) : chain B :=
+  {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
+Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+Definition csum_compl `{Cofe A, Cofe B} : Compl csumC := λ c,
+  match c 0 with
+  | Cinl a => Cinl (compl (csum_chain_l c a))
+  | Cinr b => Cinr (compl (csum_chain_r c b))
+  | CsumBot => CsumBot
+  end.
+Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumC :=
+  {| compl := csum_compl |}.
+Next Obligation.
+  intros ?? n c; rewrite /compl /csum_compl.
+  feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+  + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
+  + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
+Qed.
+
 Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC.
 Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
 Global Instance csum_leibniz :
@@ -115,10 +121,10 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
                        (g : B → B') (g' : B' → B'') (x : csum A B) :
   csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
 Proof. by destruct x. Qed.
-Lemma csum_map_ext {A A' B B' : cofeT} (f f' : A → A') (g g' : B → B') x :
+Lemma csum_map_ext {A A' B B' : ofeT} (f f' : A → A') (g g' : B → B') x :
   (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
 Proof. by destruct x; constructor. Qed.
-Instance csum_map_cmra_ne {A A' B B' : cofeT} n :
+Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
          (@csum_map A A' B B').
 Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
@@ -224,7 +230,7 @@ Proof.
     + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
 Qed.
 Canonical Structure csumR :=
-  CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
+  CMRAT (csum A B) csum_ofe_mixin csum_cmra_mixin.
 
 Global Instance csum_cmra_discrete :
   CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.

algebra/dec_agree.v

@@ -20,7 +20,7 @@ Implicit Types x y : dec_agree A.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
+Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
   match x, y with

algebra/dra.v

@@ -114,7 +114,7 @@ Proof.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; trans y]; tauto.
 Qed.
-Canonical Structure validityC : cofeT := discreteC (validity A).
+Canonical Structure validityC : ofeT := discreteC (validity A).