Move the `iprod` CMRA definition into `cmra.v`.

In same spirit as the other 'primitive' types like `option`, `prod`, ...

theories/algebra/cmra.v

 From iris.algebra Require Export ofe monoid.
+From stdpp Require Import finite.
 Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
@@ -1462,3 +1463,103 @@ Instance optionURF_contractive F :
 Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
+
+(* Dependently-typed functions *)
+Section iprod_cmra.
+  Context `{Hfin : Finite A} {B : A → ucmraT}.
+  Implicit Types f g : iprod B.
+
+  Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
+  Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
+  Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
+  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
+
+  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
+  Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
+
+  Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
+  Proof using Hfin.
+    split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
+    intros [h ?]%finite_choice. by exists h.
+  Qed.
+
+  Lemma iprod_cmra_mixin : CmraMixin (iprod B).
+  Proof using Hfin.
+    apply cmra_total_mixin.
+    - eauto.
+    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
+    - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
+    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
+    - intros g; split.
+      + intros Hg n i; apply cmra_valid_validN, Hg.
+      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
+    - intros n f Hf x; apply cmra_validN_S, Hf.
+    - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
+    - by intros f1 f2 x; rewrite iprod_lookup_op comm.
+    - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
+    - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
+    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
+      by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
+    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
+    - intros n f f1 f2 Hf Hf12.
+      destruct (finite_choice (λ x (yy : B x * B x),
+        f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
+      { intros x. specialize (Hf12 x).
+        destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
+        exists (y1,y2); eauto. }
+      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
+  Qed.
+  Canonical Structure iprodR := CmraT (iprod B) iprod_cmra_mixin.
+
+  Instance iprod_unit : Unit (iprod B) := λ x, ε.
+  Definition iprod_lookup_empty x : ε x = ε := eq_refl.
+
+  Lemma iprod_ucmra_mixin : UcmraMixin (iprod B).
+  Proof.
+    split.
+    - intros x; apply ucmra_unit_valid.
+    - by intros f x; rewrite iprod_lookup_op left_id.
+    - constructor=> x. apply core_id_core, _.
+  Qed.
+  Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
+
+  Global Instance iprod_unit_discrete :
+    (∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
+  Proof. intros ? f Hf x. by apply: discrete. Qed.
+End iprod_cmra.
+
+Arguments iprodR {_ _ _} _.
+Arguments iprodUR {_ _ _} _.
+
+Instance iprod_map_cmra_morphism
+    `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
+  (∀ x, CmraMorphism (f x)) → CmraMorphism (iprod_map f).
+Proof.
+  split; first apply _.
+  - intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
+  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
+  - intros g1 g2 i. by rewrite /iprod_map iprod_lookup_op cmra_morphism_op.
+Qed.
+
+Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
+  urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
+  urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
+|}.
+Next Obligation.
+  intros C ?? F A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>?; apply urFunctor_ne.
+Qed.
+Next Obligation.
+  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
+  apply iprod_map_ext=> y; apply urFunctor_id.
+Qed.
+Next Obligation.
+  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
+  apply iprod_map_ext=>y; apply urFunctor_compose.
+Qed.
+Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) :
+  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply urFunctor_contractive.
+Qed.

theories/algebra/iprod.v

 From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 
-(** * Indexed product *)
 Definition iprod_insert `{EqDecision A} {B : A → ofeT}
-    (x : A) (y : B x) (f : iprodC B) : iprodC B := λ x',
+    (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Instance: Params (@iprod_insert) 5.
 
-Section iprod_operations.
+Definition iprod_singleton `{Finite A} {B : A → ucmraT} 
+  (x : A) (y : B x) : iprod B := iprod_insert x y ε.
+Instance: Params (@iprod_singleton) 5.
+
+Section ofe.
   Context `{Heqdec : EqDecision A} {B : A → ofeT}.
   Implicit Types x : A.
   Implicit Types f g : iprod B.
@@ -33,14 +36,6 @@ Section iprod_operations.
     x ≠ x' → (iprod_insert x y f) x' = f x'.
   Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
 
-  Global Instance iprod_lookup_discrete f x : Discrete f → Discrete (f x).
-  Proof using Heqdec.
-    intros ? y ?.
-    cut (f ≡ iprod_insert x y f).
-    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
-    apply (discrete _)=> x'; destruct (decide (x = x')) as [->|];
-      by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
-  Qed.
   Global Instance iprod_insert_discrete f x y :
     Discrete f → Discrete y → Discrete (iprod_insert x y f).
   Proof.
@@ -50,111 +45,12 @@ Section iprod_operations.
     - rewrite iprod_lookup_insert_ne //.
       apply: discrete. by rewrite -(Heq x') iprod_lookup_insert_ne.
   Qed.
-End iprod_operations.
-
-Section iprod_cmra.
-  Context `{Hfin : Finite A} {B : A → ucmraT}.
-  Implicit Types f g : iprod B.
-
-  Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
-  Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
-  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-
-  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
-  Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
-
-  Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
-  Proof using Hfin.
-    split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
-    intros [h ?]%finite_choice. by exists h.
-  Qed.
-
-  Lemma iprod_cmra_mixin : CmraMixin (iprod B).
-  Proof using Hfin.
-    apply cmra_total_mixin.
-    - eauto.
-    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
-    - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
-    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
-    - intros g; split.
-      + intros Hg n i; apply cmra_valid_validN, Hg.
-      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
-    - intros n f Hf x; apply cmra_validN_S, Hf.
-    - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
-    - by intros f1 f2 x; rewrite iprod_lookup_op comm.
-    - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
-    - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
-    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
-    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
-    - intros n f f1 f2 Hf Hf12.
-      destruct (finite_choice (λ x (yy : B x * B x),
-        f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
-      { intros x. specialize (Hf12 x).
-        destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
-        exists (y1,y2); eauto. }
-      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
-  Qed.
-  Canonical Structure iprodR := CmraT (iprod B) iprod_cmra_mixin.
-
-  Instance iprod_unit : Unit (iprod B) := λ x, ε.
-  Definition iprod_lookup_empty x : ε x = ε := eq_refl.
-
-  Lemma iprod_ucmra_mixin : UcmraMixin (iprod B).
-  Proof.
-    split.
-    - intros x; apply ucmra_unit_valid.
-    - by intros f x; rewrite iprod_lookup_op left_id.
-    - constructor=> x. apply core_id_core, _.
-  Qed.
-  Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
-
-  Global Instance iprod_unit_discrete :
-    (∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
-  Proof. intros ? f Hf x. by apply: discrete. Qed.
-
-  (** Internalized properties *)
-  Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
-  Proof. by uPred.unseal. Qed.
-  Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M).
-  Proof. by uPred.unseal. Qed.
-
-  (** Properties of iprod_insert. *)
-  Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
-    y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
-    iprod_insert x y1 g ~~>: Q.
-  Proof.
-    intros Hy1 HP; apply cmra_total_updateP.
-    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
-    { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
-    exists (iprod_insert x y2 g); split; [auto|].
-    intros x'; destruct (decide (x' = x)) as [->|];
-      rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
-    move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
-  Qed.
-
-  Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 :
-    y1 ~~>: P →
-    iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2.
-  Proof. eauto using iprod_insert_updateP. Qed.
-  Lemma iprod_insert_update g x y1 y2 :
-    y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
-  Proof.
-    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
-  Qed.
-End iprod_cmra.
-
-Arguments iprodR {_ _ _} _.
-Arguments iprodUR {_ _ _} _.
+End ofe.
 
-Definition iprod_singleton `{Finite A} {B : A → ucmraT} 
-  (x : A) (y : B x) : iprod B := iprod_insert x y ε.
-Instance: Params (@iprod_singleton) 5.
-
-Section iprod_singleton.
+Section cmra.
   Context `{Finite A} {B : A → ucmraT}.
   Implicit Types x : A.
+  Implicit Types f g : iprod B.
 
   Global Instance iprod_singleton_ne x :
     NonExpansive (iprod_singleton x : B x → _).
@@ -200,6 +96,29 @@ Section iprod_singleton.
     - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
   Qed.
 
+  Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
+    y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
+    iprod_insert x y1 g ~~>: Q.
+  Proof.
+    intros Hy1 HP; apply cmra_total_updateP.
+    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
+    { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
+    exists (iprod_insert x y2 g); split; [auto|].
+    intros x'; destruct (decide (x' = x)) as [->|];
+      rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
+    move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
+  Qed.
+
+  Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 :
+    y1 ~~>: P →
+    iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2.
+  Proof. eauto using iprod_insert_updateP. Qed.
+  Lemma iprod_insert_update g x y1 y2 :
+    y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
+  Proof.
+    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
+  Qed.
+
   Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
     iprod_singleton x y1 ~~>: Q.
@@ -231,38 +150,4 @@ Section iprod_singleton.
     rewrite !cmra_update_updateP;
       eauto using iprod_singleton_updateP_empty with subst.
   Qed.
-End iprod_singleton.
-
-(** * Functor *)
-Instance iprod_map_cmra_morphism
-    `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
-  (∀ x, CmraMorphism (f x)) → CmraMorphism (iprod_map f).
-Proof.
-  split; first apply _.
-  - intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
-  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
-  - intros g1 g2 i. by rewrite /iprod_map iprod_lookup_op cmra_morphism_op.
-Qed.
-
-Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
-  urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
-  urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
-|}.
-Next Obligation.
-  intros C ?? F A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>?; apply urFunctor_ne.
-Qed.
-Next Obligation.
-  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
-  apply iprod_map_ext=> y; apply urFunctor_id.
-Qed.
-Next Obligation.
-  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
-  apply iprod_map_ext=>y; apply urFunctor_compose.
-Qed.
-Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) :
-  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply urFunctor_contractive.
-Qed.
+End cmra.

theories/algebra/ofe.v

@@ -511,42 +511,6 @@ Section fixpointAB_ne.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
 End fixpointAB_ne.
 
-(** Function space *)
-(* We make [iprod] a definition so that we can register it as a canonical
-structure. *)
-Definition iprod {A} (B : A → ofeT) := ∀ x : A, B x.
-
-Section iprod.
-  Context {A : Type} {B : A → ofeT}.
-  Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
-  Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Definition iprod_ofe_mixin : OfeMixin (iprod B).
-  Proof.
-    split.
-    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
-      intros Hfg k; apply equiv_dist=> n; apply Hfg.
-    - intros n; split.
-      + by intros f x.
-      + by intros f g ? x.
-      + by intros f g h ?? x; trans (g x).
-    - by intros n f g ? x; apply dist_S.
-  Qed.
-  Canonical Structure iprodC := OfeT (iprod B) iprod_ofe_mixin.
-
-  Program Definition iprod_chain `(c : chain iprodC)
-    (x : A) : chain (B x) := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
-  Global Program Instance iprod_cofe `{∀ x, Cofe (B x)} : Cofe iprodC :=
-    { compl c x := compl (iprod_chain c x) }.
-  Next Obligation. intros ? n c x. apply (conv_compl n (iprod_chain c x)). Qed.
-End iprod.
-
-Arguments iprodC {_} _.
-Notation "A -c> B" :=
-  (@iprodC A (λ _, B)) (at level 99, B at level 200, right associativity).
-Instance iprod_inhabited {A} {B : A → ofeT} `{∀ x, Inhabited (B x)} :
-  Inhabited (iprodC B) := populate (λ _, inhabitant).
-
 (** Non-expansive function space *)
 Record ofe_mor (A B : ofeT) : Type := CofeMor {
   ofe_mor_car :> A → B;
@@ -762,58 +726,6 @@ Proof.
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
-Definition iprod_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-
-Lemma iprod_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
-  (g : iprod B1) :
-  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id {A} {B : A → ofeT} (g : iprod B) :
-  iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose {A} {B1 B2 B3 : A → ofeT}
-    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
-  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
-Proof. done. Qed.
-
-Instance iprod_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
-  (∀ x, Proper (dist n ==> dist n) (f x)) →
-  Proper (dist n ==> dist n) (iprod_map f).
-Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-
-Definition iprodC_map {A} {B1 B2 : A → ofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
-  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne {A} {B1 B2 : A → ofeT} :
-  NonExpansive (@iprodC_map A B1 B2).
-Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
-
-Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
-  cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
-  cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
-|}.
-Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
-Qed.
-Next Obligation.
-  intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
-  apply iprod_map_ext=> y; apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
-  apply iprod_map_ext=>y; apply cFunctor_compose.
-Qed.
-
-Notation "T -c> F" := (@iprodCF T%type (λ _, F%CF)) : cFunctor_scope.
-
-Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
-  (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
-Qed.
-
-
 Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
   cFunctor_map A1 A2 B1 B2 fg :=
@@ -1175,6 +1087,106 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
+(* Dependently-typed functions *)
+(* We make [iprod] a definition so that we can register it as a canonical
+structure. *)
+Definition iprod {A} (B : A → ofeT) := ∀ x : A, B x.
+
+Section iprod.
+  Context {A : Type} {B : A → ofeT}.
+  Implicit Types f g : iprod B.
+
+  Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
+  Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+  Definition iprod_ofe_mixin : OfeMixin (iprod B).
+  Proof.
+    split.
+    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
+      intros Hfg k; apply equiv_dist=> n; apply Hfg.
+    - intros n; split.
+      + by intros f x.
+      + by intros f g ? x.
+      + by intros f g h ?? x; trans (g x).
+    - by intros n f g ? x; apply dist_S.
+  Qed.
+  Canonical Structure iprodC := OfeT (iprod B) iprod_ofe_mixin.
+
+  Program Definition iprod_chain `(c : chain iprodC)
+    (x : A) : chain (B x) := {| chain_car n := c n x |}.
+  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+  Global Program Instance iprod_cofe `{∀ x, Cofe (B x)} : Cofe iprodC :=
+    { compl c x := compl (iprod_chain c x) }.
+  Next Obligation. intros ? n c x. apply (conv_compl n (iprod_chain c x)). Qed.
+
+  Global Instance iprod_inhabited `{∀ x, Inhabited (B x)} : Inhabited iprodC :=
+    populate (λ _, inhabitant).
+  Global Instance iprod_lookup_discrete `{EqDecision A} f x :
+    Discrete f → Discrete (f x).
+  Proof.
+    intros Hf y ?.
+    set (g x' := if decide (x = x') is left H then eq_rect _ B y _ H else f x').
+    trans (g x).
+    { apply Hf=> x'. unfold g. by destruct (decide _) as [[]|]. }
+    unfold g. destruct (decide _) as [Hx|]; last done.
+    by rewrite (proof_irrel Hx eq_refl).
+  Qed.
+End iprod.
+
+Arguments iprodC {_} _.
+Notation "A -c> B" :=
+  (@iprodC A (λ _, B)) (at level 99, B at level 200, right associativity).
+
+Definition iprod_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
+  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
+
+Lemma iprod_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
+  (g : iprod B1) :
+  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
+Proof. done. Qed.
+Lemma iprod_map_id {A} {B : A → ofeT} (g : iprod B) :
+  iprod_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma iprod_map_compose {A} {B1 B2 B3 : A → ofeT}
+    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
+  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
+Proof. done. Qed.
+
+Instance iprod_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
+  (∀ x, Proper (dist n ==> dist n) (f x)) →
+  Proper (dist n ==> dist n) (iprod_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
+
+Definition iprodC_map {A} {B1 B2 : A → ofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
+  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
+Instance iprodC_map_ne {A} {B1 B2 : A → ofeT} :
+  NonExpansive (@iprodC_map A B1 B2).
+Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
+
+Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
+  cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
+  cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
+|}.
+Next Obligation.
+  intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
+Qed.
+Next Obligation.
+  intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
+  apply iprod_map_ext=> y; apply cFunctor_id.
+Qed.
+Next Obligation.
+  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
+  apply iprod_map_ext=>y; apply cFunctor_compose.
+Qed.
+
+Notation "T -c> F" := (@iprodCF T%type (λ _, F%CF)) : cFunctor_scope.
+
+Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
+  (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
+Qed.
+
 (** Constructing isomorphic OFEs *)
 Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A)
   (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)

theories/base_logic/lib/saved_prop.v

@@ -111,8 +111,7 @@ Proof. iApply saved_anything_alloc. Qed.
 Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
   saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
 Proof.
-  iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
-  iDestruct (ofe_funC_equivI (CofeMor Next ∘ Φ) (CofeMor Next ∘ Ψ)) as "[FE _]".
-  simpl. iApply ("FE" with "[-]").
-  iApply (saved_anything_agree with "HΦ HΨ").
+  unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
+  iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq".
+  by iDestruct (iprod_equivI with "Heq") as "?".
 Qed.

theories/base_logic/primitive.v

 From iris.base_logic Require Export upred.
+From stdpp Require Import finite.
 From iris.algebra Require Export updates.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -651,12 +652,15 @@ Proof.
 Qed.
 
 (* Function extensionality *)
-Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof. by unseal. Qed.
 Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
+Lemma iprod_equivI `{B : A → ofeT} (g1 g2 : iprod B) : g1 ≡ g2 ⊣⊢ ∀ i, g1 i ≡ g2 i.
+Proof. by uPred.unseal. Qed.
+
+Lemma iprod_validI `{Finite A} {B : A → ucmraT} (g : iprod B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. by uPred.unseal. Qed.
 
-(* Sig ofes *)
+(* Sigma OFE *)
 Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sigC P) :
   x ≡ y ⊣⊢ proj1_sig x ≡ proj1_sig y.
 Proof. by unseal. Qed.