Skip to content
GitLab
Commit cec05125 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `iprod` into `ofe_fun`.

parent c93ee508
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ cec05125
......@@ -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
View file @ cec05125
......@@ -1465,41 +1465,41 @@ Proof.
Qed.
(* Dependently-typed functions *)
Section iprod_cmra.
Section ofe_fun_cmra.
Context `{Hfin : Finite A} {B : A → ucmraT}.
Implicit Types f g : iprod B.
Implicit Types f g : ofe_fun 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.
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 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.
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 iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
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 /iprod_op (Hh x)|].
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 iprod_cmra_mixin : CmraMixin (iprod B).
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 iprod_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
- 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 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.
- 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),
......@@ -1509,57 +1509,57 @@ Section iprod_cmra.
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.
Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
Instance iprod_unit : Unit (iprod B) := λ x, ε.
Definition iprod_lookup_empty x : ε x = ε := eq_refl.
Instance ofe_fun_unit : Unit (ofe_fun B) := λ x, ε.
Definition ofe_fun_lookup_empty x : ε x = ε := eq_refl.
Lemma iprod_ucmra_mixin : UcmraMixin (iprod B).
Lemma ofe_fun_ucmra_mixin : UcmraMixin (ofe_fun B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- by intros f x; rewrite ofe_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
Canonical Structure ofe_funUR := UcmraT (ofe_fun B) ofe_fun_ucmra_mixin.
Global Instance iprod_unit_discrete :
(∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
Global Instance ofe_fun_unit_discrete :
(∀ i, Discrete (ε : B i)) → Discrete (ε : ofe_fun B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
End iprod_cmra.
End ofe_fun_cmra.
Arguments iprodR {_ _ _} _.
Arguments iprodUR {_ _ _} _.
Arguments ofe_funR {_ _ _} _.
Arguments ofe_funUR {_ _ _} _.
Instance iprod_map_cmra_morphism
Instance ofe_fun_map_cmra_morphism
`{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
(∀ x, CmraMorphism (f x)) → CmraMorphism (iprod_map f).
(∀ x, CmraMorphism (f x)) → CmraMorphism (ofe_fun_map f).
Proof.
split; first apply _.
- intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
- 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 /iprod_map iprod_lookup_op cmra_morphism_op.
- intros g1 g2 i. by rewrite /ofe_fun_map ofe_fun_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)
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 iprodC_map_ne=>?; apply urFunctor_ne.
by apply ofe_funC_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.
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 /=-iprod_map_compose.
apply iprod_map_ext=>y; apply urFunctor_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 iprodURF_contractive `{Finite C} (F : C → urFunctor) :
(∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
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 iprodC_map_ne=>c; apply urFunctor_contractive.
by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
Qed.
theories/algebra/functions.v 0 → 100644
View file @ cec05125
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 deleted 100644 → 0
View file @ c93ee508
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Definition iprod_insert `{EqDecision 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.
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.
(** Properties of iprod_insert. *)
Global Instance iprod_insert_ne x :
NonExpansive2 (iprod_insert (B:=B) 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_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 ofe.
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 → _).
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_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.
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 cmra.
theories/algebra/ofe.v
View file @ cec05125
......@@ -1088,17 +1088,17 @@ Proof.
Qed.
(* Dependently-typed functions *)
(* We make [iprod] a definition so that we can register it as a canonical
(* We make [ofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition iprod {A} (B : A → ofeT) := ∀ x : A, B x.
Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.
Section iprod.
Section ofe_fun.
Context {A : Type} {B : A → ofeT}.
Implicit Types f g : iprod B.
Implicit Types f g : ofe_fun 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).
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|].
......@@ -1109,18 +1109,18 @@ Section iprod.
+ 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.
Canonical Structure ofe_funC := OfeT (ofe_fun B) ofe_fun_ofe_mixin.
Program Definition iprod_chain `(c : chain iprodC)
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 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 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 iprod_inhabited `{∀ x, Inhabited (B x)} : Inhabited iprodC :=
Global Instance ofe_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited ofe_funC :=
populate (λ _, inhabitant).
Global Instance iprod_lookup_discrete `{EqDecision A} f x :
Global Instance ofe_fun_lookup_discrete `{EqDecision A} f x :
Discrete f → Discrete (f x).
Proof.
intros Hf y ?.
......@@ -1130,61 +1130,61 @@ Section iprod.
unfold g. destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).