Merge branch 'robbert/iprod' into 'master'

Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod`

See merge request FP/iris-coq!88

_CoqProject

@@ -14,7 +14,7 @@ theories/algebra/dra.v
 theories/algebra/cofe_solver.v
 theories/algebra/agree.v
 theories/algebra/excl.v
-theories/algebra/iprod.v
+theories/algebra/functions.v
 theories/algebra/frac.v
 theories/algebra/csum.v
 theories/algebra/list.v

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 over a finite domain *)
+Section ofe_fun_cmra.
+  Context `{Hfin : Finite A} {B : A → ucmraT}.
+  Implicit Types f g : ofe_fun B.
+
+  Instance ofe_fun_op : Op (ofe_fun B) := λ f g x, f x ⋅ g x.
+  Instance ofe_fun_pcore : PCore (ofe_fun B) := λ f, Some (λ x, core (f x)).
+  Instance ofe_fun_valid : Valid (ofe_fun B) := λ f, ∀ x, ✓ f x.
+  Instance ofe_fun_validN : ValidN (ofe_fun B) := λ n f, ∀ x, ✓{n} f x.
+
+  Definition ofe_fun_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
+  Definition ofe_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
+
+  Lemma ofe_fun_included_spec (f g : ofe_fun B) : f ≼ g ↔ ∀ x, f x ≼ g x.
+  Proof using Hfin.
+    split; [by intros [h Hh] x; exists (h x); rewrite /op /ofe_fun_op (Hh x)|].
+    intros [h ?]%finite_choice. by exists h.
+  Qed.
+
+  Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B).
+  Proof using Hfin.
+    apply cmra_total_mixin.
+    - eauto.
+    - by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x).
+    - by intros n f1 f2 Hf x; rewrite ofe_fun_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 ofe_fun_lookup_op assoc.
+    - by intros f1 f2 x; rewrite ofe_fun_lookup_op comm.
+    - by intros f x; rewrite ofe_fun_lookup_op ofe_fun_lookup_core cmra_core_l.
+    - by intros f x; rewrite ofe_fun_lookup_core cmra_core_idemp.
+    - intros f1 f2; rewrite !ofe_fun_included_spec=> Hf x.
+      by rewrite ofe_fun_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 ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
+
+  Instance ofe_fun_unit : Unit (ofe_fun B) := λ x, ε.
+  Definition ofe_fun_lookup_empty x : ε x = ε := eq_refl.
+
+  Lemma ofe_fun_ucmra_mixin : UcmraMixin (ofe_fun B).
+  Proof.
+    split.
+    - intros x; apply ucmra_unit_valid.
+    - by intros f x; rewrite ofe_fun_lookup_op left_id.
+    - constructor=> x. apply core_id_core, _.
+  Qed.
+  Canonical Structure ofe_funUR := UcmraT (ofe_fun B) ofe_fun_ucmra_mixin.
+
+  Global Instance ofe_fun_unit_discrete :
+    (∀ i, Discrete (ε : B i)) → Discrete (ε : ofe_fun B).
+  Proof. intros ? f Hf x. by apply: discrete. Qed.
+End ofe_fun_cmra.
+
+Arguments ofe_funR {_ _ _} _.
+Arguments ofe_funUR {_ _ _} _.
+
+Instance ofe_fun_map_cmra_morphism
+    `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
+  (∀ x, CmraMorphism (f x)) → CmraMorphism (ofe_fun_map f).
+Proof.
+  split; first apply _.
+  - intros n g Hg x; rewrite /ofe_fun_map; apply (cmra_morphism_validN (f _)), Hg.
+  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
+  - intros g1 g2 i. by rewrite /ofe_fun_map ofe_fun_lookup_op cmra_morphism_op.
+Qed.
+
+Program Definition ofe_funURF `{Finite 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)
+|}.
+Next Obligation.
+  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).
+  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.
+  apply ofe_fun_map_ext=>y; apply urFunctor_compose.
+Qed.
+Instance ofe_funURF_contractive `{Finite C} (F : C → urFunctor) :
+  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
+Qed.

theories/algebra/functions.v

+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates.
+From stdpp Require Import finite.
+Set Default Proof Using "Type".
+
+Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
+    (x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
+  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
+Instance: Params (@ofe_fun_insert) 5.
+
+Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT} 
+  (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
+Instance: Params (@ofe_fun_singleton) 5.
+
+Section ofe.
+  Context `{Heqdec : EqDecision A} {B : A → ofeT}.
+  Implicit Types x : A.
+  Implicit Types f g : ofe_fun B.
+
+  (** Properties of ofe_fun_insert. *)
+  Global Instance ofe_fun_insert_ne x :
+    NonExpansive2 (ofe_fun_insert (B:=B) x).
+  Proof.
+    intros n y1 y2 ? f1 f2 ? x'; rewrite /ofe_fun_insert.
+    by destruct (decide _) as [[]|].
+  Qed.
+  Global Instance ofe_fun_insert_proper x :
+    Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert x) := ne_proper_2 _.
+
+  Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
+  Proof.
+    rewrite /ofe_fun_insert; destruct (decide _) as [Hx|]; last done.
+    by rewrite (proof_irrel Hx eq_refl).
+  Qed.
+  Lemma ofe_fun_lookup_insert_ne f x x' y :
+    x ≠ x' → (ofe_fun_insert x y f) x' = f x'.
+  Proof. by rewrite /ofe_fun_insert; destruct (decide _). Qed.
+
+  Global Instance ofe_fun_insert_discrete f x y :
+    Discrete f → Discrete y → Discrete (ofe_fun_insert x y f).
+  Proof.
+    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
+    - rewrite ofe_fun_lookup_insert.
+      apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert.
+    - rewrite ofe_fun_lookup_insert_ne //.
+      apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert_ne.
+  Qed.
+End ofe.
+
+Section cmra.
+  Context `{Finite A} {B : A → ucmraT}.
+  Implicit Types x : A.
+  Implicit Types f g : ofe_fun B.
+
+  Global Instance ofe_fun_singleton_ne x :
+    NonExpansive (ofe_fun_singleton x : B x → _).
+  Proof. intros n y1 y2 ?; apply ofe_fun_insert_ne. done. by apply equiv_dist. Qed.
+  Global Instance ofe_fun_singleton_proper x :
+    Proper ((≡) ==> (≡)) (ofe_fun_singleton x) := ne_proper _.
+
+  Lemma ofe_fun_lookup_singleton x (y : B x) : (ofe_fun_singleton x y) x = y.
+  Proof. by rewrite /ofe_fun_singleton ofe_fun_lookup_insert. Qed.
+  Lemma ofe_fun_lookup_singleton_ne x x' (y : B x) :
+    x ≠ x' → (ofe_fun_singleton x y) x' = ε.
+  Proof. intros; by rewrite /ofe_fun_singleton ofe_fun_lookup_insert_ne. Qed.
+
+  Global Instance ofe_fun_singleton_discrete x (y : B x) :
+    (∀ i, Discrete (ε : B i)) →  Discrete y → Discrete (ofe_fun_singleton x y).
+  Proof. apply _. Qed.
+
+  Lemma ofe_fun_singleton_validN n x (y : B x) : ✓{n} ofe_fun_singleton x y ↔ ✓{n} y.
+  Proof.
+    split; [by move=>/(_ x); rewrite ofe_fun_lookup_singleton|].
+    move=>Hx x'; destruct (decide (x = x')) as [->|];
+      rewrite ?ofe_fun_lookup_singleton ?ofe_fun_lookup_singleton_ne //.
+    by apply ucmra_unit_validN.
+  Qed.
+
+  Lemma ofe_fun_core_singleton x (y : B x) :
+    core (ofe_fun_singleton x y) ≡ ofe_fun_singleton x (core y).
+  Proof.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
+      ?ofe_fun_lookup_singleton_ne // (core_id_core ∅).
+  Qed.
+
+  Global Instance ofe_fun_singleton_core_id x (y : B x) :
+    CoreId y → CoreId (ofe_fun_singleton x y).
+  Proof. by rewrite !core_id_total ofe_fun_core_singleton=> ->. Qed.
+
+  Lemma ofe_fun_op_singleton (x : A) (y1 y2 : B x) :
+    ofe_fun_singleton x y1 ⋅ ofe_fun_singleton x y2 ≡ ofe_fun_singleton x (y1 ⋅ y2).
+  Proof.
+    intros x'; destruct (decide (x' = x)) as [->|].
+    - by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton.
+    - by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton_ne // left_id.
+  Qed.
+
+  Lemma ofe_fun_insert_updateP x (P : B x → Prop) (Q : ofe_fun B → Prop) g y1 :
+    y1 ~~>: P → (∀ y2, P y2 → Q (ofe_fun_insert x y2 g)) →
+    ofe_fun_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 ofe_fun_lookup_op ofe_fun_lookup_insert. }
+    exists (ofe_fun_insert x y2 g); split; [auto|].
+    intros x'; destruct (decide (x' = x)) as [->|];
+      rewrite ofe_fun_lookup_op ?ofe_fun_lookup_insert //; [].
+    move: (Hg x'). by rewrite ofe_fun_lookup_op !ofe_fun_lookup_insert_ne.
+  Qed.
+
+  Lemma ofe_fun_insert_updateP' x (P : B x → Prop) g y1 :
+    y1 ~~>: P →
+    ofe_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = ofe_fun_insert x y2 g ∧ P y2.
+  Proof. eauto using ofe_fun_insert_updateP. Qed.
+  Lemma ofe_fun_insert_update g x y1 y2 :
+    y1 ~~> y2 → ofe_fun_insert x y1 g ~~> ofe_fun_insert x y2 g.
+  Proof.
+    rewrite !cmra_update_updateP; eauto using ofe_fun_insert_updateP with subst.
+  Qed.
+
+  Lemma ofe_fun_singleton_updateP x (P : B x → Prop) (Q : ofe_fun B → Prop) y1 :
+    y1 ~~>: P → (∀ y2, P y2 → Q (ofe_fun_singleton x y2)) →
+    ofe_fun_singleton x y1 ~~>: Q.
+  Proof. rewrite /ofe_fun_singleton; eauto using ofe_fun_insert_updateP. Qed.
+  Lemma ofe_fun_singleton_updateP' x (P : B x → Prop) y1 :
+    y1 ~~>: P →
+    ofe_fun_singleton x y1 ~~>: λ g, ∃ y2, g = ofe_fun_singleton x y2 ∧ P y2.
+  Proof. eauto using ofe_fun_singleton_updateP. Qed.
+  Lemma ofe_fun_singleton_update x (y1 y2 : B x) :
+    y1 ~~> y2 → ofe_fun_singleton x y1 ~~> ofe_fun_singleton x y2.
+  Proof. eauto using ofe_fun_insert_update. Qed.
+
+  Lemma ofe_fun_singleton_updateP_empty x (P : B x → Prop) (Q : ofe_fun B → Prop) :
+    ε ~~>: P → (∀ y2, P y2 → Q (ofe_fun_singleton x y2)) → ε ~~>: Q.
+  Proof.
+    intros Hx HQ; apply cmra_total_updateP.
+    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
+    exists (ofe_fun_singleton x y2); split; [by apply HQ|].
+    intros x'; destruct (decide (x' = x)) as [->|].
+    - by rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton.
+    - rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton_ne //. apply Hg.
+  Qed.
+  Lemma ofe_fun_singleton_updateP_empty' x (P : B x → Prop) :
+    ε ~~>: P → ε ~~>: λ g, ∃ y2, g = ofe_fun_singleton x y2 ∧ P y2.
+  Proof. eauto using ofe_fun_singleton_updateP_empty. Qed.
+  Lemma ofe_fun_singleton_update_empty x (y : B x) :
+    ε ~~> y → ε ~~> ofe_fun_singleton x y.
+  Proof.
+    rewrite !cmra_update_updateP;
+      eauto using ofe_fun_singleton_updateP_empty with subst.
+  Qed.
+End cmra.

theories/algebra/iprod.v

-From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
-From stdpp Require Import finite.
-Set Default Proof Using "Type".
-
-(** * Indexed product *)
-(** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod `{Finite A} (B : A → ofeT) := ∀ x, B x.
-Definition iprod_insert `{Finite A} {B : A → ofeT}
-    (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_cofe.
-  Context `{Finite A} {B : A → ofeT}.
-  Implicit Types x : A.
-  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; intros n; apply Hfg.
-    - intros n; split.
-      + by intros f x.
-      + by intros f g ? x.
-      + by intros f g h ?? x; trans (g x).
-    - intros n f g Hfg x; apply dist_S, Hfg.
-  Qed.
-  Canonical Structure iprodC : ofeT := 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. by intros c x n i ?; apply (chain_cauchy c). Qed.
-  Global Program Instance iprod_cofe `{∀ a, Cofe (B a)} : Cofe iprodC :=
-    {| compl c x := compl (iprod_chain c x) |}.
-  Next Obligation.
-    intros ? n c x.
-    rewrite (conv_compl n (iprod_chain c x)).
-    apply (chain_cauchy c); lia.
-  Qed.
-
-  (** Properties of iprod_insert. *)
-  Global Instance iprod_insert_ne x :
-    NonExpansive2 (iprod_insert x).
-  Proof.
-    intros n y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
-    by destruct (decide _) as [[]|].
-  Qed.
-  Global Instance iprod_insert_proper x :
-    Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _.
-
-  Lemma iprod_lookup_insert f x y : (iprod_insert x y f) x = y.
-  Proof.
-    rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
-    by rewrite (proof_irrel Hx eq_refl).
-  Qed.
-  Lemma iprod_lookup_insert_ne f x x' y :
-    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.
-    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.
-    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
-    - rewrite iprod_lookup_insert.
-      apply: discrete. by rewrite -(Heq x') iprod_lookup_insert.
-    - rewrite iprod_lookup_insert_ne //.
-      apply: discrete. by rewrite -(Heq x') iprod_lookup_insert_ne.
-  Qed.
-End iprod_cofe.
-
-Arguments iprodC {_ _ _} _.
-
-Section iprod_cmra.
-  Context `{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.
-    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.
-    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 {_ _ _} _.
-
-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.
-  Context `{Finite A} {B : A → ucmraT}.
-  Implicit Types x : A.
-
-  Global Instance iprod_singleton_ne x :
-    NonExpansive (iprod_singleton x : B x → _).
-  Proof. intros n y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
-  Global Instance iprod_singleton_proper x :
-    Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
-
-  Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
-  Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
-  Lemma iprod_lookup_singleton_ne x x' (y : B x) :
-    x ≠ x' → (iprod_singleton x y) x' = ε.
-  Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
-
-  Global Instance iprod_singleton_discrete x (y : B x) :
-    (∀ i, Discrete (ε : B i)) →  Discrete y → Discrete (iprod_singleton x y).
-  Proof. apply _. Qed.
-
-  Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
-  Proof.
-    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
-    move=>Hx x'; destruct (decide (x = x')) as [->|];
-      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
-    by apply ucmra_unit_validN.
-  Qed.
-
-  Lemma iprod_core_singleton x (y : B x) :
-    core (iprod_singleton x y) ≡ iprod_singleton x (core y).
-  Proof.
-    move=>x'; destruct (decide (x = x')) as [->|];
-      by rewrite iprod_lookup_core ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // (core_id_core ∅).
-  Qed.
-
-  Global Instance iprod_singleton_core_id x (y : B x) :
-    CoreId y → CoreId (iprod_singleton x y).
-  Proof. by rewrite !core_id_total iprod_core_singleton=> ->. Qed.
-
-  Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
-    iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
-  Proof.
-    intros x'; destruct (decide (x' = x)) as [->|].
-    - by rewrite iprod_lookup_op !iprod_lookup_singleton.
-    - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
-  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.
-  Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
-  Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
-    y1 ~~>: P →
-    iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
-  Proof. eauto using iprod_singleton_updateP. Qed.
-  Lemma iprod_singleton_update x (y1 y2 : B x) :
-    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
-  Proof. eauto using iprod_insert_update. Qed.
-
-  Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
-    ε ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ε ~~>: Q.
-  Proof.
-    intros Hx HQ; apply cmra_total_updateP.
-    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
-    exists (iprod_singleton x y2); split; [by apply HQ|].
-    intros x'; destruct (decide (x' = x)) as [->|].
-    - by rewrite iprod_lookup_op iprod_lookup_singleton.
-    - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
-  Qed.
-  Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
-    ε ~~>: P → ε ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
-  Proof. eauto using iprod_singleton_updateP_empty. Qed.
-  Lemma iprod_singleton_update_empty x (y : B x) :
-    ε ~~> y → ε ~~> iprod_singleton x y.
-  Proof.
-    rewrite !cmra_update_updateP;
-      eauto using iprod_singleton_updateP_empty with subst.
-  Qed.
-End iprod_singleton.
-
-(** * Functor *)
-Definition iprod_map `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-
-Lemma iprod_map_ext `{Finite 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 `{Finite A} {B : A → ofeT} (g : iprod B) :
-  iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose `{Finite 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 `{Finite 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.
-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.
-
-Definition iprodC_map `{Finite 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 `{Finite 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 `{Finite 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.
-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 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/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 [ofe_fun] a definition so that we can register it as a canonical
-structure. *)
-Definition ofe_fun (A : Type) (B : ofeT) := A → B.
-
-Section ofe_fun.
-  Context {A : Type} {B : ofeT}.
-  Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, ∀ x, f x ≡ g x.
-  Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A 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 ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
-
-  Program Definition ofe_fun_chain `(c : chain ofe_funC)
-    (x : A) : chain B := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
-  Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
-    { compl c x := compl (ofe_fun_chain c x) }.
-  Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
-End ofe_fun.
-
-Arguments ofe_funC : clear implicits.
-Notation "A -c> B" :=
-  (ofe_funC A B) (at level 99, B at level 200, right associativity).
-Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
-  Inhabited (A -c> B) := populate (λ _, inhabitant).
-
 (** Non-expansive function space *)
 Record ofe_mor (A B : ofeT) : Type := CofeMor {
   ofe_mor_car :> A → B;
@@ -762,37 +726,6 @@ Proof.
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
-Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') :
-  NonExpansive (compose f : (A -c> B) → A -c> B').
-Proof. intros n g g' Hf x; simpl. by rewrite (Hf x). Qed.
-
-Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
-  @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
-Instance ofe_funC_map_ne {A B B'} :
-  NonExpansive (@ofe_funC_map A B B').
-Proof. intros n f f' Hf g x. apply Hf. Qed.
-
-Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne.
-Qed.
-Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
-Next Obligation.
-  intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
-  by rewrite !cFunctor_compose.
-Qed.
-Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
-
-Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
-  cFunctorContractive F → cFunctorContractive (ofe_funCF T F).
-Proof.
-  intros ?? A1 A2 B1 B2 n ???;
-    by apply ofe_funC_map_ne; 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 :=
@@ -1154,6 +1087,106 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
+(* Dependently-typed functions over a discrete domain *)
+(* We make [ofe_fun] a definition so that we can register it as a canonical
+structure. *)
+Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.
+
+Section ofe_fun.
+  Context {A : Type} {B : A → ofeT}.
+  Implicit Types f g : ofe_fun B.
+
+  Instance ofe_fun_equiv : Equiv (ofe_fun B) := λ f g, ∀ x, f x ≡ g x.
+  Instance ofe_fun_dist : Dist (ofe_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+  Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun 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 ofe_funC := OfeT (ofe_fun B) ofe_fun_ofe_mixin.
+
+  Program Definition ofe_fun_chain `(c : chain ofe_funC)
+    (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 ofe_fun_cofe `{∀ x, Cofe (B x)} : Cofe ofe_funC :=
+    { compl c x := compl (ofe_fun_chain c x) }.
+  Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
+
+  Global Instance ofe_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited ofe_funC :=
+    populate (λ _, inhabitant).
+  Global Instance ofe_fun_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 ofe_fun.
+
+Arguments ofe_funC {_} _.
+Notation "A -c> B" :=
+  (@ofe_funC A (λ _, B)) (at level 99, B at level 200, right associativity).
+
+Definition ofe_fun_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
+  (g : ofe_fun B1) : ofe_fun B2 := λ x, f _ (g x).
+
+Lemma ofe_fun_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
+  (g : ofe_fun B1) :
+  (∀ x, f1 x (g x) ≡ f2 x (g x)) → ofe_fun_map f1 g ≡ ofe_fun_map f2 g.
+Proof. done. Qed.
+Lemma ofe_fun_map_id {A} {B : A → ofeT} (g : ofe_fun B) :
+  ofe_fun_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma ofe_fun_map_compose {A} {B1 B2 B3 : A → ofeT}
+    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : ofe_fun B1) :
+  ofe_fun_map (λ x, f2 x ∘ f1 x) g = ofe_fun_map f2 (ofe_fun_map f1 g).
+Proof. done. Qed.
+
+Instance ofe_fun_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) (ofe_fun_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /ofe_fun_map (Hy x). Qed.
+
+Definition ofe_funC_map {A} {B1 B2 : A → ofeT} (f : ofe_fun (λ x, B1 x -n> B2 x)) :
+  ofe_funC B1 -n> ofe_funC B2 := CofeMor (ofe_fun_map f).
+Instance ofe_funC_map_ne {A} {B1 B2 : A → ofeT} :
+  NonExpansive (@ofe_funC_map A B1 B2).
+Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
+
+Program Definition ofe_funCF {C} (F : C → cFunctor) : cFunctor := {|
+  cFunctor_car A B := ofe_funC (λ c, cFunctor_car (F c) A B);
+  cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, cFunctor_map (F c) fg)
+|}.
+Next Obligation.
+  intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
+Qed.
+Next Obligation.
+  intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+  apply ofe_fun_map_ext=> y; apply cFunctor_id.
+Qed.
+Next Obligation.
+  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 cFunctor_compose.
+Qed.
+
+Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
+
+Instance ofe_funCF_contractive `{Finite C} (F : C → cFunctor) :
+  (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply ofe_funC_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/iprop.v

 From iris.base_logic Require Export base_logic.
-From iris.algebra Require Import iprod gmap.
+From iris.algebra Require Import gmap.
 From iris.algebra Require cofe_solver.
 Set Default Proof Using "Type".
 
@@ -47,7 +47,7 @@ Definition gname := positive.
 
 (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
 Definition iResF (Σ : gFunctors) : urFunctor :=
-  iprodURF (λ i, gmapURF gname (Σ i)).
+  ofe_funURF (λ i, gmapURF gname (Σ i)).
 
 
 (** We define functions for the empty list of functors, the singleton list of
@@ -116,7 +116,7 @@ construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
   Parameter iPreProp : gFunctors → ofeT.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
 
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
@@ -134,7 +134,7 @@ Module Export iProp_solution : iProp_solution_sig.
 
   Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
 
   Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=

theories/base_logic/lib/own.v

-From iris.algebra Require Import iprod gmap.
+From iris.algebra Require Import functions gmap.
 From iris.base_logic Require Import big_op.
 From iris.base_logic Require Export iprop.
 From iris.proofmode Require Import classes.
@@ -49,7 +49,7 @@ Ltac solve_inG :=
 
 (** * Definition of the connective [own] *)
 Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
-  iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
+  ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
 Instance: Params (@iRes_singleton) 4.
 
 Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
@@ -68,11 +68,11 @@ Implicit Types a : A.
 (** ** Properties of [iRes_singleton] *)
 Global Instance iRes_singleton_ne γ :
   NonExpansive (@iRes_singleton Σ A _ γ).
-Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+Proof. by intros n a a' Ha; apply ofe_fun_singleton_ne; rewrite Ha. Qed.
 Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
 Proof.
-  by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
+  by rewrite /iRes_singleton ofe_fun_op_singleton op_singleton cmra_transport_op.
 Qed.
 
 (** ** Properties of [own] *)
@@ -92,7 +92,7 @@ Proof. intros a1 a2. apply own_mono. Qed.
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
   rewrite !own_eq /own_def ownM_valid /iRes_singleton.
-  rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
+  rewrite ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
   rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
   (* implicit arguments differ a bit *)
   by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
@@ -120,7 +120,7 @@ Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
   - rewrite /uPred_valid ownM_unit.
-    eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
+    eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
@@ -137,7 +137,7 @@ Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∧ ow
 Proof.
   intros Ha. rewrite !own_eq.
   rewrite -(bupd_mono (∃ m, ⌜∃ a', m = iRes_singleton γ a' ∧ P a'⌝ ∧ uPred_ownM m)%I).
-  - eapply bupd_ownM_updateP, iprod_singleton_updateP;
+  - eapply bupd_ownM_updateP, ofe_fun_singleton_updateP;
       first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
   - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
@@ -170,7 +170,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
 Proof.
   rewrite /uPred_valid ownM_unit !own_eq /own_def.
-  apply bupd_ownM_update, iprod_singleton_update_empty.
+  apply bupd_ownM_update, ofe_fun_singleton_update_empty.
   apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.

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 (ofe_fun_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 ofe_fun_equivI `{B : A → ofeT} (g1 g2 : ofe_fun B) : g1 ≡ g2 ⊣⊢ ∀ i, g1 i ≡ g2 i.
+Proof. by uPred.unseal. Qed.
+
+Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun 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.