diff --git a/_CoqProject b/_CoqProject index 61631c3ee3821c3c999004ff91d41579c2682a2b..13c296354ff16a778c455e79595df5e381685a62 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index 3c3b1171ca0a40c770e295e5aaff79a7dcecd443..d35386930c066efdd93f16d620dc4efc5c47aa95 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -1,4 +1,5 @@ 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. diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v new file mode 100644 index 0000000000000000000000000000000000000000..a4c6a03a727cd2165fb553fb6b0e148c1ad8de33 --- /dev/null +++ b/theories/algebra/functions.v @@ -0,0 +1,153 @@ +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. diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v deleted file mode 100644 index e3051d27f9b7e4d4fc730c14eb8ac68afde98794..0000000000000000000000000000000000000000 --- a/theories/algebra/iprod.v +++ /dev/null @@ -1,345 +0,0 @@ -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. diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 56d17e71096d71848325e74fce4f1ea7b0b9e2b3..eb422ac9b8a73bb933c48f2cfa10cd34bd47bc6a 100644 --- a/theories/algebra/ofe.v +++ b/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) diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v index a36fb468200f92a5b9abfa9d628d918c11f7f548..8f1768137509da9551500bee52f1be2bfa3b1fe3 100644 --- a/theories/base_logic/lib/iprop.v +++ b/theories/base_logic/lib/iprop.v @@ -1,5 +1,5 @@ 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 Σ := diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v index 9381789f3f1b0956ee893cc142049b105123fd51..ed1ab6073ee9ca2b54dec5a9a74673be0d8fcdb8 100644 --- a/theories/base_logic/lib/own.v +++ b/theories/base_logic/lib/own.v @@ -1,4 +1,4 @@ -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. diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v index 9b5f721e7e6577d6f646ac315cbeaa85a5e47e48..c8ee4d412e4f54b7c796e81be8b1fed293152e78 100644 --- a/theories/base_logic/lib/saved_prop.v +++ b/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. diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v index 1e123fa4bb0058bce0980ab3320647fea1a7f2aa..1c718f84d5de23bb9ba1dd0ba929504d4e661fef 100644 --- a/theories/base_logic/primitive.v +++ b/theories/base_logic/primitive.v @@ -1,4 +1,5 @@ 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.