Commit 2855d1f5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Replace `C`s with `O`s since we use OFEs instead of COFEs.

Used the following script:

sed '
s/\bCofeMor/OfeMor/g;
s/\-c>/\-d>/g;
s/\bcFunctor/oFunctor/g;
s/\bCFunctor/OFunctor/g;
s/\b\%CF/\%OF/g;
s/\bconstCF/constOF/g;
s/\bidCF/idOF/g
s/\bdiscreteC/discreteO/g;
s/\bleibnizC/leibnizO/g;
s/\bunitC/unitO/g;
s/\bprodC/prodO/g;
s/\bsumC/sumO/g;
s/\bboolC/boolO/g;
s/\bnatC/natO/g;
s/\bpositiveC/positiveO/g;
s/\bNC/NO/g;
s/\bZC/ZO/g;
s/\boptionC/optionO/g;
s/\blaterC/laterO/g;
s/\bofe\_fun/discrete\_fun/g;
s/\bdiscrete\_funC/discrete\_funO/g;
s/\bofe\_morC/ofe\_morO/g;
s/\bsigC/sigO/g;
s/\buPredC/uPredO/g;
s/\bcsumC/csumO/g;
s/\bagreeC/agreeO/g;
s/\bauthC/authO/g;
s/\bnamespace_mapC/namespace\_mapO/g;
s/\bcmra\_ofeC/cmra\_ofeO/g;
s/\bucmra\_ofeC/ucmra\_ofeO/g;
s/\bexclC/exclO/g;
s/\bgmapC/gmapO/g;
s/\blistC/listO/g;
s/\bvecC/vecO/g;
s/\bgsetC/gsetO/g;
s/\bgset\_disjC/gset\_disjO/g;
s/\bcoPsetC/coPsetO/g;
s/\bgmultisetC/gmultisetO/g;
s/\bufracC/ufracO/g
s/\bfracC/fracO/g;
s/\bvalidityC/validityO/g;
s/\bbi\_ofeC/bi\_ofeO/g;
s/\bsbi\_ofeC/sbi\_ofeO/g;
s/\bmonPredC/monPredO/g;
s/\bstateC/stateO/g;
s/\bvalC/valO/g;
s/\bexprC/exprO/g;
s/\blocC/locO/g;
' -i $(find theories -name "*.v")
parent d4d61110
......@@ -132,7 +132,7 @@ Section M.
Arguments op _ _ !_ !_/.
Arguments core _ _ !_/.
Canonical Structure M_C : ofeT := leibnizC M.
Canonical Structure M_O : ofeT := leibnizO M.
Instance M_valid : Valid M := λ x, x Bot.
Instance M_op : Op M := λ x y,
......
......@@ -21,7 +21,7 @@ Definition one_shot_example : val := λ: <>,
end
end)).
Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
Definition Pending : one_shotR := Cinl (Excl ()).
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
......
......@@ -75,7 +75,7 @@ Proof.
destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
- intros n x y [??]; split; naive_solver eauto using dist_S.
Qed.
Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.
Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
......@@ -251,7 +251,7 @@ Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
End agree.
Instance: Params (@to_agree) 1 := {}.
Arguments agreeC : clear implicits.
Arguments agreeO : clear implicits.
Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B :=
......@@ -297,33 +297,33 @@ Section agree_map.
Qed.
End agree_map.
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
CofeMor (agree_map f : agreeC A agreeC B).
Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
OfeMor (agree_map f : agreeO A agreeO B).
Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
Proof.
intros n f g Hfg x; split=> b /=;
setoid_rewrite elem_of_list_fmap; naive_solver.
Qed.
Program Definition agreeRF (F : cFunctor) : rFunctor := {|
rFunctor_car A _ B _ := agreeR (cFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeC_map (cFunctor_map F fg)
Program Definition agreeRF (F : oFunctor) : rFunctor := {|
rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
|}.
Next Obligation.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
apply (agree_map_ext _)=>y; apply cFunctor_compose.
apply (agree_map_ext _)=>y; apply oFunctor_compose.
Qed.
Instance agreeRF_contractive F :
cFunctorContractive F rFunctorContractive (agreeRF F).
oFunctorContractive F rFunctorContractive (agreeRF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
by apply agreeC_map_ne, cFunctor_contractive.
by apply agreeO_map_ne, oFunctor_contractive.
Qed.
......@@ -62,16 +62,16 @@ Proof. by destruct 1. Qed.
Definition auth_ofe_mixin : OfeMixin (auth A).
Proof. by apply (iso_ofe_mixin (λ x, (auth_auth_proj x, auth_frag_proj x))). Qed.
Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
Canonical Structure authO := OfeT (auth A) auth_ofe_mixin.
Global Instance Auth_discrete a b :
Discrete a Discrete b Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A OfeDiscrete authC.
Global Instance auth_ofe_discrete : OfeDiscrete A OfeDiscrete authO.
Proof. intros ? [??]; apply _. Qed.
End ofe.
Arguments authC : clear implicits.
Arguments authO : clear implicits.
(* Camera *)
Section cmra.
......@@ -430,18 +430,18 @@ Proof.
- intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; try by rewrite cmra_morphism_op.
by rewrite -Some_op pair_op cmra_morphism_op.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
Definition authO_map {A B} (f : A -n> B) : authO A -n> authO B :=
OfeMor (auth_map f).
Lemma authO_map_ne A B : NonExpansive (@authO_map A B).
Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
apply agreeC_map_ne; auto. Qed.
apply agreeO_map_ne; auto. Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_car A _ B _ := authR (urFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
......@@ -455,15 +455,15 @@ Qed.
Instance authRF_contractive F :
urFunctorContractive F rFunctorContractive (authRF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
......@@ -477,5 +477,5 @@ Qed.
Instance authURF_contractive F :
urFunctorContractive F urFunctorContractive (authURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
Qed.
......@@ -98,8 +98,8 @@ Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac A) : CmraMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
......@@ -221,8 +221,8 @@ Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
Canonical Structure ucmra_cmraR.
......@@ -1199,10 +1199,10 @@ Qed.
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply rFunctor_ne.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation.
......@@ -1216,16 +1216,16 @@ Instance prodRF_contractive F1 F2 :
rFunctorContractive (prodRF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply rFunctor_contractive.
by apply prodO_map_ne; apply rFunctor_contractive.
Qed.
Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply urFunctor_ne.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
Next Obligation.
......@@ -1239,7 +1239,7 @@ Instance prodURF_contractive F1 F2 :
urFunctorContractive (prodURF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply urFunctor_contractive.
by apply prodO_map_ne; apply urFunctor_contractive.
Qed.
(** ** CMRA for the option type *)
......@@ -1459,10 +1459,10 @@ Qed.
Program Definition optionRF (F : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
......@@ -1476,15 +1476,15 @@ Qed.
Instance optionRF_contractive F :
rFunctorContractive F rFunctorContractive (optionRF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
......@@ -1498,106 +1498,106 @@ Qed.
Instance optionURF_contractive F :
rFunctorContractive F urFunctorContractive (optionURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
Qed.
(* Dependently-typed functions over a discrete domain *)
Section ofe_fun_cmra.
Section discrete_fun_cmra.
Context `{B : A ucmraT}.
Implicit Types f g : ofe_fun B.
Implicit Types f g : discrete_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.
Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x g x.
Instance discrete_fun_pcore : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
Instance discrete_fun_valid : Valid (discrete_fun B) := λ f, x, f x.
Instance discrete_fun_validN : ValidN (discrete_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.
Definition discrete_fun_lookup_op f g x : (f g) x = f x g x := eq_refl.
Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
Lemma ofe_fun_included_spec_1 (f g : ofe_fun B) x : f g f x g x.
Proof. by intros [h Hh]; exists (h x); rewrite /op /ofe_fun_op (Hh x). Qed.
Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f g f x g x.
Proof. by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op (Hh x). Qed.
Lemma ofe_fun_included_spec `{Hfin : Finite A} (f g : ofe_fun B) : f g x, f x g x.
Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) : f g x, f x g x.
Proof.
split; [by intros; apply ofe_fun_included_spec_1|].
split; [by intros; apply discrete_fun_included_spec_1|].
intros [h ?]%finite_choice; by exists h.
Qed.
Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B).
Lemma discrete_fun_cmra_mixin : CmraMixin (discrete_fun B).
Proof.
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 f3 Hf x; rewrite discrete_fun_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite discrete_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 Hf12. exists (core f2)=>x. rewrite ofe_fun_lookup_op.
apply (ofe_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
rewrite !ofe_fun_lookup_core. destruct Hf12 as [? ->].
- by intros f1 f2 f3 x; rewrite discrete_fun_lookup_op assoc.
- by intros f1 f2 x; rewrite discrete_fun_lookup_op comm.
- by intros f x; rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
- by intros f x; rewrite discrete_fun_lookup_core cmra_core_idemp.
- intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
rewrite assoc -cmra_core_dup //.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))).
split; [|split]=>x; [rewrite ofe_fun_lookup_op| |];
split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
by destruct (FUN x) as (?&?&?&?&?).
Qed.
Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
Canonical Structure discrete_funR := CmraT (discrete_fun B) discrete_fun_cmra_mixin.
Instance ofe_fun_unit : Unit (ofe_fun B) := λ x, ε.
Definition ofe_fun_lookup_empty x : ε x = ε := eq_refl.
Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
Lemma ofe_fun_ucmra_mixin : UcmraMixin (ofe_fun B).
Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite ofe_fun_lookup_op left_id.
- by intros f x; rewrite discrete_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
Canonical Structure ofe_funUR := UcmraT (ofe_fun B) ofe_fun_ucmra_mixin.
Canonical Structure discrete_funUR := UcmraT (discrete_fun B) discrete_fun_ucmra_mixin.
Global Instance ofe_fun_unit_discrete :
( i, Discrete (ε : B i)) Discrete (ε : ofe_fun B).
Global Instance discrete_fun_unit_discrete :
( i, Discrete (ε : B i)) Discrete (ε : discrete_fun B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
End ofe_fun_cmra.
End discrete_fun_cmra.
Arguments ofe_funR {_} _.
Arguments ofe_funUR {_} _.
Arguments discrete_funR {_} _.
Arguments discrete_funUR {_} _.
Instance ofe_fun_map_cmra_morphism {A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) :
( x, CmraMorphism (f x)) CmraMorphism (ofe_fun_map f).
Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) :
( x, CmraMorphism (f x)) CmraMorphism (discrete_fun_map f).
Proof.
split; first apply _.
- intros n g Hg x; rewrite /ofe_fun_map; apply (cmra_morphism_validN (f _)), Hg.
- intros n g Hg x; rewrite /discrete_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.
- intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.
Program Definition ofe_funURF {C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := ofe_funUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
Program Definition discrete_funURF {C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := discrete_funUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_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.
intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
apply discrete_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.
intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_compose.
Qed.
Instance ofe_funURF_contractive {C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (ofe_funURF F).
Instance discrete_funURF_contractive {C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (discrete_funURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
by apply discrete_funO_map_ne=>c; apply urFunctor_contractive.
Qed.
......@@ -9,7 +9,7 @@ generalize the construction without breaking canonical structures. *)
Section coPset.
Implicit Types X Y : coPset.
Canonical Structure coPsetC := discreteC coPset.
Canonical Structure coPsetO := discreteO coPset.
Instance coPset_valid : Valid coPset := λ _, True.
Instance coPset_unit : Unit coPset := ( : coPset).
......@@ -67,7 +67,7 @@ Inductive coPset_disj :=
Section coPset_disj.
Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjC := leibnizC coPset_disj.
Canonical Structure coPset_disjC := leibnizO coPset_disj.
Instance coPset_disj_valid : Valid coPset_disj := λ X,
match X with CoPset _ => True | CoPsetBot => False end.
......
From iris.algebra Require Export ofe.
Set Default Proof Using "Type".
Record solution (F : cFunctor) := Solution {
Record solution (F : oFunctor) := Solution {
solution_car :> ofeT;
solution_cofe : Cofe solution_car;
solution_unfold : solution_car -n> F solution_car _;
......@@ -14,23 +14,23 @@ Arguments solution_fold {_} _.
Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : cFunctor) `{Fcontr : cFunctorContractive F}.
Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
Context `{Fcofe : (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
Context `{Finh : Inhabited (F unitC _)}.
Notation map := (cFunctor_map F).
Context `{Finh : Inhabited (F unitO _)}.
Notation map := (oFunctor_map F).
Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
match k with
| 0 => existT (P:=Cofe) unitC _
| 0 => existT (P:=Cofe) unitO _
| S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
end.
Notation A k := (projT1 (A' k)).
Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
match k with 0 => OfeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments f : simpl never.
......@@ -39,14 +39,14 @@ Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x.
Proof using Fcontr.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map).
rewrite -oFunctor_compose -{2}[x]oFunctor_id. by apply (contractive_proper map).
Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Proof using Fcontr.
induction k as [|k IH]; simpl.
- rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
- rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
apply (contractive_0 map).
- rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
- rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
by apply (contractive_S map).
Qed.
......@@ -104,7 +104,7 @@ Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
Proof. by intros X Y HX. Qed.
Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).
Definition project (k : nat) : T -n> A k := OfeMor (λ X : T, tower_car X k).
Definition coerce {i j} (H : i = j) : A i -n> A j :=
eq_rect _ (λ i', A i -n> A i') cid _ H.
......@@ -158,7 +158,7 @@ Next Obligation. intros k x i. apply g_embed_coerce. Qed.
Instance: Params (@embed) 1 := {}.
Instance embed_ne k : NonExpansive (embed k).
Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
Definition embed' (k : nat) : A k -n> T := OfeMor (embed k).
Lemma embed_f k (x : A k) : embed (S k) (f k x) embed k x.
Proof.
rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
......@@ -188,7 +188,7 @@ Next Obligation.
assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
induction k as [|k IH]; simpl; first done.
rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
rewrite f_S -cFunctor_compose.
rewrite f_S -oFunctor_compose.
by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
Definition unfold (X : T) : F T _ := compl (unfold_chain X).
......@@ -202,7 +202,7 @@ Program Definition fold (X : F T _) : T :=
{| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation.
intros X k. apply (_ : Proper (() ==> ()) (g k)).
rewrite g_S -cFunctor_compose.
rewrite g_S -oFunctor_compose.