Merge branch 'robbert/functor_cofe' into 'master'

Turn the arguments of functors into COFEs + write some docs See merge request iris/iris!257

Merge branch 'robbert/functor_cofe' into 'master'
Turn the arguments of functors into COFEs + write some docs See merge request iris/iris!257
643508b8 · Ralf Jung · 2cfaec5d · cb5834a8 · 643508b8 · 643508b8
Commit 643508b8 authored Jun 04, 2019 by Ralf Jung
17 changed files
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,8 @@ Changes in and extensions of the theory:
  describes the postcondition of each forked-off thread (instead of it being
  `True`). Additionally, there is a stronger variant of the adequacy theorem
  that allows to make use of the postconditions of the forked-off threads.
+* The user-chosen functor used to instantiate the Iris logic now goes from
+  COFEs to Cameras (it was OFEs to Cameras).

 Changes in Coq:


--- a/ProofGuide.md
+++ b/ProofGuide.md
@@ -6,16 +6,71 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
 [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
 the [style guide](StyleGuide.md).

+## Combinators for functors
+
+In Iris, the type of propositions [iProp] is described by the solution to the
+recursive domain equation:
+
+```
+iProp ≅ uPred (F (iProp))
+```
+
+Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
+Camaras (a step-indexed generalization of unital resource algebras). To make it
+convenient to construct such functors out of smaller pieces, we provide a number
+of abstractions:
+
+- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
+- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
+- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
+  cameras.
+
+Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
+`urFunctorContractive` which describe the subset of the above functors that
+are contractive.
+
+To compose these functors, we provide a number of combinators, e.g.:
+
+- `constCF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
+- `idCF : cFunctor                         := λ (B,B⁻), B`
+- `prodCF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
+- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
+- `laterCF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
+- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
+- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
+
+Using these combinators, one can easily construct bigger functors in point-free
+style, e.g:
+
+```
+F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
+```
+
+which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
+
+Furthermore, for functors written using these combinators like the functor `F`
+above, Coq can automatically `urFunctorContractive F`.
+
+To make it a little bit more convenient to write down such functors, we make
+the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
+provide the usual notation for products, etc. So the above functor can be
+written as follows (which is similar to the effective definition of `F` above):
+
+```
+F := gmapURF K (agreeRF (natC * ▶ ∙))
+```
+
 ## Resource algebra management

 When using ghost state in Iris, you have to make sure that the resource algebras
 you need are actually available.  Every Iris proof is carried out using a
 universally quantified list `Σ: gFunctors` defining which resource algebras are
 available.  You can think of this as a list of resource algebras, though in
-reality it is a list of functors from OFEs to Cameras (where Cameras are a
-step-indexed generalization of resource algebras).  This is the *global* list of
-resources that the entire proof can use.  We keep it universally quantified to
-enable composition of proofs.  The formal side of this is described in §7.4 of
+reality it is a list of locally contractive functors from COFEs to Cameras,
+which are typically defined using the combinators for functors described above.
+The `Σ` is the *global* list of resources that the entire proof can use.  We
+keep the `Σ` universally quantified to enable composition of proofs.  The formal
+side of this is described in §7.4 of
 [The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
 describe the Coq aspects of this approach.


--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -174,7 +174,7 @@ The purpose of this section is to describe how we solve these issues.

 \paragraph{Picking the resources.}
 The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
-To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs^\op \times \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
 (This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)

 From this, we construct the bifunctor defining the overall resources as follows:

--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -306,24 +306,24 @@ Proof.
 Qed.

 Program Definition agreeRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A B := agreeR (cFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
+  rFunctor_car A _ B _ := agreeR (cFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
+  intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
  apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
  apply (agree_map_ext _)=>y; apply cFunctor_compose.
 Qed.

 Instance agreeRF_contractive F :
  cFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
-  intros ? A1 A2 B1 B2 n ???; simpl.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
  by apply agreeC_map_ne, cFunctor_contractive.
 Qed.
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -403,13 +403,13 @@ Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. 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. destruct x as [[[]|] ];  by rewrite // /auth_map /= agree_map_compose. Qed.
-Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{_ : NonExpansive f} x :
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{!NonExpansive f} x :
  (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
  constructor; simpl; auto.
  apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
 Qed.
-Instance auth_map_ne {A B : ofeT} (f : A -> B) {Hf : NonExpansive f} :
+Instance auth_map_ne {A B : ofeT} (f : A -> B) `{Hf : !NonExpansive f} :
  NonExpansive (auth_map f).
 Proof.
  intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
@@ -437,45 +437,45 @@ Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
  apply agreeC_map_ne; auto. Qed.

 Program Definition authRF (F : urFunctor) : rFunctor := {|
-  rFunctor_car A B := authR (urFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y. apply _. apply urFunctor_id.
+  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
+  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
 Qed.

 Instance authRF_contractive F :
  urFunctorContractive F → rFunctorContractive (authRF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
 Qed.

 Program Definition authURF (F : urFunctor) : urFunctor := {|
-  urFunctor_car A B := authUR (urFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y. apply _. apply urFunctor_id.
+  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
+  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
 Qed.

 Instance authURF_contractive F :
  urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
 Qed.
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -766,16 +766,18 @@ End cmra_morphism.

 (** Functors *)
 Record rFunctor := RFunctor {
-  rFunctor_car : ofeT → ofeT → cmraT;
-  rFunctor_map {A1 A2 B1 B2} :
+  rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
+  rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne A1 A2 B1 B2 :
-    NonExpansive (@rFunctor_map A1 A2 B1 B2);
-  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
-  rFunctor_compose {A1 A2 A3 B1 B2 B3}
+  rFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+    NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
+  rFunctor_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
+    rFunctor_map (cid,cid) x ≡ x;
+  rFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
-  rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+  rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
+      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mor.
@@ -785,13 +787,15 @@ Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.

 Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
+  rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+    Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).

-Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
+Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
+  rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.

 Program Definition constRF (B : cmraT) : rFunctor :=
-  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
+  {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constRF : cmraT >-> rFunctor.

@@ -799,16 +803,18 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.

 Record urFunctor := URFunctor {
-  urFunctor_car : ofeT → ofeT → ucmraT;
-  urFunctor_map {A1 A2 B1 B2} :
+  urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
+  urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne A1 A2 B1 B2 :
-    NonExpansive (@urFunctor_map A1 A2 B1 B2);
-  urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x;
-  urFunctor_compose {A1 A2 A3 B1 B2 B3}
+  urFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+    NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
+  urFunctor_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
+    urFunctor_map (cid,cid) x ≡ x;
+  urFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
-  urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+  urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
+      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (urFunctor_map fg)
 }.
 Existing Instances urFunctor_ne urFunctor_mor.
@@ -818,13 +824,15 @@ Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.

 Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
+  urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+    Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).

-Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
+Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
+  urFunctor_car F A A.
 Coercion urFunctor_diag : urFunctor >-> Funclass.

 Program Definition constURF (B : ucmraT) : urFunctor :=
-  {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
+  {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constURF : ucmraT >-> urFunctor.

@@ -1189,16 +1197,16 @@ Proof.
 Qed.

 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
-  rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
-  rFunctor_map A1 A2 B1 B2 fg :=
+  rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply rFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply rFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
  by rewrite !rFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
@@ -1207,21 +1215,21 @@ Instance prodRF_contractive F1 F2 :
  rFunctorContractive F1 → rFunctorContractive F2 →
  rFunctorContractive (prodRF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodC_map_ne; apply rFunctor_contractive.
 Qed.

 Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
-  urFunctor_car A B := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
-  urFunctor_map A1 A2 B1 B2 fg :=
+  urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply urFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply urFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !urFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
  by rewrite !urFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
@@ -1230,7 +1238,7 @@ Instance prodURF_contractive F1 F2 :
  urFunctorContractive F1 → urFunctorContractive F2 →
  urFunctorContractive (prodURF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodC_map_ne; apply urFunctor_contractive.
 Qed.

@@ -1450,47 +1458,47 @@ Proof.
 Qed.

 Program Definition optionRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A B := optionR (rFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.

 Instance optionRF_contractive F :
  rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.

 Program Definition optionURF (F : rFunctor) : urFunctor := {|
-  urFunctor_car A B := optionUR (rFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+  urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.

 Instance optionURF_contractive F :
  rFunctorContractive F → urFunctorContractive (optionURF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.

 (* Dependently-typed functions over a discrete domain *)
@@ -1573,23 +1581,23 @@ Proof.
 Qed.

 Program Definition ofe_funURF {C} (F : C → urFunctor) : urFunctor := {|
-  urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B);
-  urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
+  urFunctor_car A _ B _ := ofe_funUR (λ c, urFunctor_car (F c) A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
 Qed.
 Next Obligation.
-  intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+  intros C F A ? B ? g; simpl. rewrite -{2}(ofe_fun_map_id g).
  apply ofe_fun_map_ext=> y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
+  intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
  apply ofe_fun_map_ext=>y; apply urFunctor_compose.
 Qed.
 Instance ofe_funURF_contractive {C} (F : C → urFunctor) :
  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F).
 Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
 Qed.
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -4,8 +4,8 @@ Set Default Proof Using "Type".
 Record solution (F : cFunctor) := Solution {
  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_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;
  solution_unfold_fold X : solution_unfold (solution_fold X) ≡ X
 }.
@@ -14,21 +14,25 @@ Arguments solution_fold {_} _.
 Existing Instance solution_cofe.

 Module solver. Section solver.
-Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
-        `{Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)} `{Finh : Inhabited (F unitC)}.
+Context (F : cFunctor) `{Fcontr : cFunctorContractive F}.
+Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
+Context `{Finh : Inhabited (F unitC _)}.
 Notation map := (cFunctor_map F).

-Fixpoint A (k : nat) : ofeT :=
-  match k with 0 => unitC | S k => F (A k) end.
-Local Instance: ∀ k, Cofe (A k).
-Proof using Fcofe. induction k; apply _. Defined.
+Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
+  match k with
+  | 0 => existT (P:=Cofe) unitC _
+  | S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
+  end.
+Notation A k := (projT1 (A' k)).
+Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
+
 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 :=
  match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
 Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
 Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
-Arguments A : simpl never.
 Arguments f : simpl never.
 Arguments g : simpl never.

@@ -177,7 +181,7 @@ Proof.
  - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.

-Program Definition unfold_chain (X : T) : chain (F T) :=
+Program Definition unfold_chain (X : T) : chain (F T _) :=
  {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
  intros X n i Hi.
@@ -187,14 +191,14 @@ Next Obligation.
  rewrite f_S -cFunctor_compose.
  by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
-Definition unfold (X : T) : F T := compl (unfold_chain X).
+Definition unfold (X : T) : F T _ := compl (unfold_chain X).
 Instance unfold_ne : NonExpansive unfold.
 Proof.
  intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
    (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
 Qed.

-Program Definition fold (X : F T) : T :=
+Program Definition fold (X : F T _) : T :=
  {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
  intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).

--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -100,7 +100,7 @@ Global Instance csum_ofe_discrete :
  OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC.
 Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
 Global Instance csum_leibniz :
-  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B).
+  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumC.
 Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.

 Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
@@ -367,18 +367,18 @@ Proof.
 Qed.

 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
-  rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
-  rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
+  rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
+  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
 Qed.
 Next Obligation.