diff --git a/StyleGuide.md b/StyleGuide.md
index 56d55f39e62fc4e028ab607bb0afa4c8679a36d0..9665f3fe07eaf01055a8da499a932017c6f0b19a 100644
--- a/StyleGuide.md
+++ b/StyleGuide.md
@@ -36,8 +36,8 @@ is used by clients.
### small letters
-* a : A = cmraT or cofeT
-* b : B = cmraT or cofeT
+* a : A = cmraT or ofeT
+* b : B = cmraT or ofeT
* c
* d
* e : expr = expressions
@@ -67,8 +67,8 @@ is used by clients.
### capital letters
-* A : Type, cmraT or cofeT
-* B : Type, cmraT or cofeT
+* A : Type, cmraT or ofeT
+* B : Type, cmraT or ofeT
* C
* D
* E : coPset = Viewshift masks
@@ -110,9 +110,9 @@ is used by clients.
### Suffixes
-* C: OFEs
+* O: OFEs
* R: cameras
* UR: unital cameras or resources algebras
-* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
+* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
* G: global camera functor management
* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 7dcf6bde7a50056b557a72b1d901a08eb7872ab6..3db32f442b61ca098c2ee674eda27e4449bd1bd5 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -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,
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1b5ff38cf77ec3858493cc39e831978068d0bf90..8230e955044672960fb51fa289432b2e1f856c65 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -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).
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 0392aaf6a8d7865765aa33f2a0b8a884e35e829c..26a513024936fb1617226ccb622c57be43e663c3 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -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.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 1d6337816ca6b3234e34a8b677f88fcf1716b9d1..d3de7271a31c127d45323854cc624fb28316cc7a 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -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.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 45559286228f8fcf71b137b1da25b91e99557acf..f2641cd16cf1b8cccf65c19cefec4f9d8879d78a 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -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.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 445ea071a3e7452b906a82be4bbedb0311b3b818..e3e717a6ec1c40ec205ffea1d1dbb4bccd5c025c 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -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.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 33bfebd875ecf222ccbe703d9e653a0a78598f5c..eb85e390096886927603315ade17aee080ecea41 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,7 +1,7 @@
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.
apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed.
Instance fold_ne : NonExpansive fold.
@@ -210,14 +210,14 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof using Type*.
- apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
+ apply (Solution F T _ (OfeMor unfold) (OfeMor fold)).
- move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
trans (map (ff n, gg n) (X (S (n + k)))).
{ rewrite /unfold (conv_compl n (unfold_chain X)).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
- rewrite f_S -!cFunctor_compose; apply (contractive_ne map); split=> Y.
+ rewrite f_S -!oFunctor_compose; apply (contractive_ne map); split=> Y.
+ rewrite /embed' /= /embed_coerce.
destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -227,14 +227,14 @@ Proof using Type*.
assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
{ intros i; induction i as [|i IH]; intros k' x H; simpl.
- { by rewrite coerce_id cFunctor_id. }
- rewrite cFunctor_compose g_coerce; apply IH. }
+ { by rewrite coerce_id oFunctor_id. }
+ rewrite oFunctor_compose g_coerce; apply IH. }
assert (H: S n + k = n + S k) by lia.
rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- intros X; rewrite equiv_dist=> n /=.
rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
- rewrite g_S -!cFunctor_compose -{2}[X]cFunctor_id.
+ rewrite g_S -!oFunctor_compose -{2}[X]oFunctor_id.
apply (contractive_ne map); split => Y /=.
+ rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 805a9309b1a5947983981265e5939417d03f686e..d3ff72dcf73b73d03d1bdd96f50f4666ac38e72a 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -73,21 +73,21 @@ Proof.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
Qed.
-Canonical Structure csumC : ofeT := OfeT (csum A B) csum_ofe_mixin.
+Canonical Structure csumO : ofeT := OfeT (csum A B) csum_ofe_mixin.
-Program Definition csum_chain_l (c : chain csumC) (a : A) : chain A :=
+Program Definition csum_chain_l (c : chain csumO) (a : A) : chain A :=
{| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Program Definition csum_chain_r (c : chain csumC) (b : B) : chain B :=
+Program Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Definition csum_compl `{Cofe A, Cofe B} : Compl csumC := λ c,
+Definition csum_compl `{Cofe A, Cofe B} : Compl csumO := λ c,
match c 0 with
| Cinl a => Cinl (compl (csum_chain_l c a))
| Cinr b => Cinr (compl (csum_chain_r c b))
| CsumBot => CsumBot
end.
-Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumC :=
+Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
{| compl := csum_compl |}.
Next Obligation.
intros ?? n c; rewrite /compl /csum_compl.
@@ -97,10 +97,10 @@ Next Obligation.
Qed.
Global Instance csum_ofe_discrete :
- OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC.
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumO.
Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
Global Instance csum_leibniz :
- LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumC.
+ LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumO.
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
@@ -109,7 +109,7 @@ Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
End cofe.
-Arguments csumC : clear implicits.
+Arguments csumO : clear implicits.
(* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
@@ -134,11 +134,11 @@ Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
-Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
- csumC A B -n> csumC A' B' :=
- CofeMor (csum_map f g).
-Instance csumC_map_ne A A' B B' :
- NonExpansive2 (@csumC_map A A' B B').
+Definition csumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+ csumO A B -n> csumO A' B' :=
+ OfeMor (csum_map f g).
+Instance csumO_map_ne A A' B B' :
+ NonExpansive2 (@csumO_map A A' B B').
Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
Section cmra.
@@ -368,10 +368,10 @@ Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
- rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
+ rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}.
Next Obligation.
- by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
+ by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_ne.
Qed.
Next Obligation.
intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
@@ -387,5 +387,5 @@ Instance csumRF_contractive Fa Fb :
rFunctorContractive (csumRF Fa Fb).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
- by apply csumC_map_ne; try apply rFunctor_contractive.
+ by apply csumO_map_ne; try apply rFunctor_contractive.
Qed.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 2c8165cf10bff603132c3f7e054bee0c1129537d..5f9732894073ab1b9c373c7dcce59feb6a9ae3ec 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -29,7 +29,7 @@ Implicit Types x y : dec_agree A.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
+Canonical Structure dec_agreeC : ofeT := leibnizO (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 8f65c8eb7c937810c28fec208e4366ab718d370c..f162ca23e6fce3ee8a9f08d60454eb98d40d5399 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -118,7 +118,7 @@ Proof.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
split; [|intros; trans y]; tauto.
Qed.
-Canonical Structure validityC : ofeT := discreteC (validity A).
+Canonical Structure validityO : ofeT := discreteO (validity A).
Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
Proof. by split; apply: dra_valid_proper. Qed.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 8d99dec9ddeb8a90009c26a1c98958fca2813f52..6467624323e8915259dde9528e4a56be58ad5d90 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -50,16 +50,16 @@ Proof.
- by intros [a|] [b|]; split; inversion_clear 1; constructor.
- by intros n [a|] [b|]; split; inversion_clear 1; constructor.
Qed.
-Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
+Canonical Structure exclO : ofeT := OfeT (excl A) excl_ofe_mixin.
-Global Instance excl_cofe `{!Cofe A} : Cofe exclC.
+Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
Proof.
apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
- by intros n [a|] [b|]; split; inversion_clear 1; constructor.
- by intros []; constructor.
Qed.
-Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclC.
+Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclO.
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
@@ -124,7 +124,7 @@ Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
End excl.
-Arguments exclC : clear implicits.
+Arguments exclO : clear implicits.
Arguments exclR : clear implicits.
(* Functor *)
@@ -144,29 +144,29 @@ Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
-Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
- CofeMor (excl_map f).
-Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
+Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
+ OfeMor (excl_map f).
+Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
-Program Definition exclRF (F : cFunctor) : rFunctor := {|
- rFunctor_car A _ B _ := (exclR (cFunctor_car F A B));
- rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclC_map (cFunctor_map F fg)
+Program Definition exclRF (F : oFunctor) : rFunctor := {|
+ rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
+ rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
|}.
Next Obligation.
- intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
+ intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
- apply excl_map_ext=>y. by rewrite cFunctor_id.
+ apply excl_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 -excl_map_compose.
- apply excl_map_ext=>y; apply cFunctor_compose.
+ apply excl_map_ext=>y; apply oFunctor_compose.
Qed.
Instance exclRF_contractive F :
- cFunctorContractive F → rFunctorContractive (exclRF F).
+ oFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
- intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
+ intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_contractive.
Qed.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index f5f84eb01cf3f4fb43fcde9ef143018548e7da74..737208fd782cbdde15c2bb482b3692257e1613cf 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -14,7 +14,7 @@ Set Default Proof Using "Type".
Notation frac := Qp (only parsing).
Section frac.
-Canonical Structure fracC := leibnizC frac.
+Canonical Structure fracO := leibnizO frac.
Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
Instance frac_pcore : PCore frac := λ _, None.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 4ace8f8f7f88b43f6c969ebf5107126deff23b6d..3e66c877b8d091658989405848a03a337687daab 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -3,159 +3,159 @@ 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',
+Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
+ (x : A) (y : B x) (f : discrete_fun B) : discrete_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 := {}.
+Instance: Params (@discrete_fun_insert) 5 := {}.
-Definition ofe_fun_singleton `{EqDecision A} {B : A → ucmraT}
- (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
-Instance: Params (@ofe_fun_singleton) 5 := {}.
+Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmraT}
+ (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
+Instance: Params (@discrete_fun_singleton) 5 := {}.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A → ofeT}.
Implicit Types x : A.
- Implicit Types f g : ofe_fun B.
+ Implicit Types f g : discrete_fun B.
- Global Instance ofe_funC_ofe_discrete :
- (∀ i, OfeDiscrete (B i)) → OfeDiscrete (ofe_funC B).
+ Global Instance discrete_funO_ofe_discrete :
+ (∀ i, OfeDiscrete (B i)) → OfeDiscrete (discrete_funO B).
Proof. intros HB f f' Heq i. apply HB, Heq. Qed.
- (** Properties of ofe_fun_insert. *)
- Global Instance ofe_fun_insert_ne x :
- NonExpansive2 (ofe_fun_insert (B:=B) x).
+ (** Properties of discrete_fun_insert. *)
+ Global Instance discrete_fun_insert_ne x :
+ NonExpansive2 (discrete_fun_insert (B:=B) x).
Proof.
- intros n y1 y2 ? f1 f2 ? x'; rewrite /ofe_fun_insert.
+ intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert.
by destruct (decide _) as [[]|].
Qed.
- Global Instance ofe_fun_insert_proper x :
- Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert (B:=B) x) := ne_proper_2 _.
+ Global Instance discrete_fun_insert_proper x :
+ Proper ((≡) ==> (≡) ==> (≡)) (discrete_fun_insert (B:=B) x) := ne_proper_2 _.
- Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
+ Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y.
Proof.
- rewrite /ofe_fun_insert; destruct (decide _) as [Hx|]; last done.
+ rewrite /discrete_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.
+ Lemma discrete_fun_lookup_insert_ne f x x' y :
+ x ≠x' → (discrete_fun_insert x y f) x' = f x'.
+ Proof. by rewrite /discrete_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).
+ Global Instance discrete_fun_insert_discrete f x y :
+ Discrete f → Discrete y → Discrete (discrete_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.
+ - rewrite discrete_fun_lookup_insert.
+ apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert.
+ - rewrite discrete_fun_lookup_insert_ne //.
+ apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne.
Qed.
End ofe.
Section cmra.
Context `{EqDecision A} {B : A → ucmraT}.
Implicit Types x : A.
- Implicit Types f g : ofe_fun B.
+ Implicit Types f g : discrete_fun B.
- Global Instance ofe_funR_cmra_discrete:
- (∀ i, CmraDiscrete (B i)) → CmraDiscrete (ofe_funR B).
+ Global Instance discrete_funR_cmra_discrete:
+ (∀ i, CmraDiscrete (B i)) → CmraDiscrete (discrete_funR B).
Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.
- 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 _.
+ Global Instance discrete_fun_singleton_ne x :
+ NonExpansive (discrete_fun_singleton x : B x → _).
+ Proof. intros n y1 y2 ?; apply discrete_fun_insert_ne. done. by apply equiv_dist. Qed.
+ Global Instance discrete_fun_singleton_proper x :
+ Proper ((≡) ==> (≡)) (discrete_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.
+ Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y.
+ Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed.
+ Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) :
+ x ≠x' → (discrete_fun_singleton x y) x' = ε.
+ Proof. intros; by rewrite /discrete_fun_singleton discrete_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).
+ Global Instance discrete_fun_singleton_discrete x (y : B x) :
+ (∀ i, Discrete (ε : B i)) → Discrete y → Discrete (discrete_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.
+ Lemma discrete_fun_singleton_validN n x (y : B x) : ✓{n} discrete_fun_singleton x y ↔ ✓{n} y.
Proof.
- split; [by move=>/(_ x); rewrite ofe_fun_lookup_singleton|].
+ split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
- rewrite ?ofe_fun_lookup_singleton ?ofe_fun_lookup_singleton_ne //.
+ rewrite ?discrete_fun_lookup_singleton ?discrete_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).
+ Lemma discrete_fun_core_singleton x (y : B x) :
+ core (discrete_fun_singleton x y) ≡ discrete_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 ∅).
+ by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
+ ?discrete_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.
+ Global Instance discrete_fun_singleton_core_id x (y : B x) :
+ CoreId y → CoreId (discrete_fun_singleton x y).
+ Proof. by rewrite !core_id_total discrete_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).
+ Lemma discrete_fun_op_singleton (x : A) (y1 y2 : B x) :
+ discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_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.
+ - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton.
+ - by rewrite discrete_fun_lookup_op !discrete_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.
+ Lemma discrete_fun_insert_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) g y1 :
+ y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_insert x y2 g)) →
+ discrete_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|].
+ { move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. }
+ exists (discrete_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.
+ rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; [].
+ move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne.
Qed.
- Lemma ofe_fun_insert_updateP' x (P : B x → Prop) g y1 :
+ Lemma discrete_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.
+ discrete_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = discrete_fun_insert x y2 g ∧ P y2.
+ Proof. eauto using discrete_fun_insert_updateP. Qed.
+ Lemma discrete_fun_insert_update g x y1 y2 :
+ y1 ~~> y2 → discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g.
Proof.
- rewrite !cmra_update_updateP; eauto using ofe_fun_insert_updateP with subst.
+ rewrite !cmra_update_updateP; eauto using discrete_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 :
+ Lemma discrete_fun_singleton_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) y1 :
+ y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) →
+ discrete_fun_singleton x y1 ~~>: Q.
+ Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed.
+ Lemma discrete_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.
+ discrete_fun_singleton x y1 ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
+ Proof. eauto using discrete_fun_singleton_updateP. Qed.
+ Lemma discrete_fun_singleton_update x (y1 y2 : B x) :
+ y1 ~~> y2 → discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2.
+ Proof. eauto using discrete_fun_insert_update. Qed.
+
+ Lemma discrete_fun_singleton_updateP_empty x (P : B x → Prop) (Q : discrete_fun B → Prop) :
+ ε ~~>: P → (∀ y2, P y2 → Q (discrete_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|].
+ exists (discrete_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.
+ - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
+ - rewrite discrete_fun_lookup_op discrete_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.
+ Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
+ ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
+ Proof. eauto using discrete_fun_singleton_updateP_empty. Qed.
+ Lemma discrete_fun_singleton_update_empty x (y : B x) :
+ ε ~~> y → ε ~~> discrete_fun_singleton x y.
Proof.
rewrite !cmra_update_updateP;
- eauto using ofe_fun_singleton_updateP_empty with subst.
+ eauto using discrete_fun_singleton_updateP_empty with subst.
Qed.
End cmra.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 02df4be9695adb0e754b1416c847457b9d526ab2..b41d6458a13b1cedbf814f7d541a25d35d4e8adc 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -24,14 +24,14 @@ Proof.
+ by intros m1 m2 m3 ?? k; trans (m2 !! k).
- by intros n m1 m2 ? k; apply dist_S.
Qed.
-Canonical Structure gmapC : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
+Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
-Program Definition gmap_chain (c : chain gmapC)
- (k : K) : chain (optionC A) := {| chain_car n := c n !! k |}.
+Program Definition gmap_chain (c : chain gmapO)
+ (k : K) : chain (optionO A) := {| chain_car n := c n !! k |}.
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Definition gmap_compl `{Cofe A} : Compl gmapC := λ c,
+Definition gmap_compl `{Cofe A} : Compl gmapO := λ c,
map_imap (λ i _, compl (gmap_chain c i)) (c 0).
-Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapC :=
+Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapO :=
{| compl := gmap_compl |}.
Next Obligation.
intros ? n c k. rewrite /compl /gmap_compl lookup_imap.
@@ -39,10 +39,10 @@ Next Obligation.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
-Global Instance gmap_ofe_discrete : OfeDiscrete A → OfeDiscrete gmapC.
+Global Instance gmap_ofe_discrete : OfeDiscrete A → OfeDiscrete gmapO.
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
(* why doesn't this go automatic? *)
-Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC.
+Global Instance gmapO_leibniz: LeibnizEquiv A → LeibnizEquiv gmapO.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance lookup_ne k :
@@ -98,7 +98,7 @@ Lemma insert_idN n m i x :
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
End cofe.
-Arguments gmapC _ {_ _} _.
+Arguments gmapO _ {_ _} _.
(* CMRA *)
Section cmra.
@@ -548,42 +548,42 @@ Proof.
case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
- intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
Qed.
-Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
- gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
-Instance gmapC_map_ne `{Countable K} {A B} :
- NonExpansive (@gmapC_map K _ _ A B).
+Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
+ gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A → gmapO K B).
+Instance gmapO_map_ne `{Countable K} {A B} :
+ NonExpansive (@gmapO_map K _ _ A B).
Proof.
intros n f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
-Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := gmapC K (cFunctor_car F A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (cFunctor_map F fg)
+Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := gmapO K (oFunctor_car F A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
|}.
Next Obligation.
- by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
+ by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
- apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
+ apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
Qed.
Next Obligation.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
- apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
+ apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
Qed.
-Instance gmapCF_contractive K `{Countable K} F :
- cFunctorContractive F → cFunctorContractive (gmapCF K F).
+Instance gmapOF_contractive K `{Countable K} F :
+ oFunctorContractive F → oFunctorContractive (gmapOF K F).
Proof.
- by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_contractive.
Qed.
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
- urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (rFunctor_map F fg)
+ urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
|}.
Next Obligation.
- by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
+ by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
@@ -596,5 +596,5 @@ Qed.
Instance gmapRF_contractive K `{Countable K} F :
rFunctorContractive F → urFunctorContractive (gmapURF K F).
Proof.
- by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_contractive.
Qed.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 245c6ae9dfad267521daa7e6622ba764942f202e..a9acacd07a2b3ad33384181bd0bf615a5b4f4fbb 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -8,7 +8,7 @@ Section gmultiset.
Context `{Countable K}.
Implicit Types X Y : gmultiset K.
- Canonical Structure gmultisetC := discreteC (gmultiset K).
+ Canonical Structure gmultisetO := discreteO (gmultiset K).
Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
@@ -79,6 +79,6 @@ Section gmultiset.
Qed.
End gmultiset.
-Arguments gmultisetC _ {_ _}.
+Arguments gmultisetO _ {_ _}.
Arguments gmultisetR _ {_ _}.
Arguments gmultisetUR _ {_ _}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index cdfbfdbd77f4de7fede17ac3774a1747839bc562..b0b7fc5121f062bb799434d4978f9f6951b9d646 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -8,7 +8,7 @@ Section gset.
Context `{Countable K}.
Implicit Types X Y : gset K.
- Canonical Structure gsetC := discreteC (gset K).
+ Canonical Structure gsetO := discreteO (gset K).
Instance gset_valid : Valid (gset K) := λ _, True.
Instance gset_unit : Unit (gset K) := (∅ : gset K).
@@ -62,7 +62,7 @@ Section gset.
Proof. by apply core_id_total; rewrite gset_core_self. Qed.
End gset.
-Arguments gsetC _ {_ _}.
+Arguments gsetO _ {_ _}.
Arguments gsetR _ {_ _}.
Arguments gsetUR _ {_ _}.
@@ -79,7 +79,7 @@ Section gset_disj.
Arguments cmra_op _ !_ !_ /.
Arguments ucmra_op _ !_ !_ /.
- Canonical Structure gset_disjC := leibnizC (gset_disj K).
+ Canonical Structure gset_disjO := leibnizO (gset_disj K).
Instance gset_disj_valid : Valid (gset_disj K) := λ X,
match X with GSet _ => True | GSetBot => False end.
@@ -227,6 +227,6 @@ Section gset_disj.
Qed.
End gset_disj.
-Arguments gset_disjC _ {_ _}.
+Arguments gset_disjO _ {_ _}.
Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index c6d5a137cbeb79448097146b85be0dfe8942c7e3..0d3d22a06c7fb097755cb758cccdd9ed41f2bdef 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -61,7 +61,7 @@ Proof.
- apply _.
- rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
Qed.
-Canonical Structure listC := OfeT (list A) list_ofe_mixin.
+Canonical Structure listO := OfeT (list A) list_ofe_mixin.
(** To define [compl : chain (list A) → list A] we make use of the fact that
given a given chain [c0, c1, c2, ...] of lists, the list [c0] completely
@@ -69,13 +69,13 @@ determines the shape (i.e. the length) of all lists in the chain. So, the
[compl] operation is defined by structural recursion on [c0], and takes the
completion of the elements of all lists in the chain point-wise. We use [head]
and [tail] as the inverse of [cons]. *)
-Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listC) : listC :=
+Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listO) : listO :=
match c0 with
| [] => []
| x :: c0 => compl (chain_map (default x ∘ head) c) :: list_compl_go c0 (chain_map tail c)
end.
-Global Program Instance list_cofe `{!Cofe A} : Cofe listC :=
+Global Program Instance list_cofe `{!Cofe A} : Cofe listO :=
{| compl c := list_compl_go (c 0) c |}.
Next Obligation.
intros ? n c; rewrite /compl.
@@ -89,7 +89,7 @@ Next Obligation.
- rewrite IH /= ?Hcn //.
Qed.
-Global Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listC.
+Global Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listO.
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Global Instance nil_discrete : Discrete (@nil A).
@@ -98,7 +98,7 @@ Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x ::
Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
End cofe.
-Arguments listC : clear implicits.
+Arguments listO : clear implicits.
(** Functor *)
Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
@@ -107,31 +107,31 @@ Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
Instance list_fmap_ne {A B : ofeT} (f : A → B) n:
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
-Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
- CofeMor (fmap f : listC A → listC B).
-Instance listC_map_ne A B : NonExpansive (@listC_map A B).
+Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
+ OfeMor (fmap f : listO A → listO B).
+Instance listO_map_ne A B : NonExpansive (@listO_map A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
-Program Definition listCF (F : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := listC (cFunctor_car F A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (cFunctor_map F fg)
+Program Definition listOF (F : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := listO (oFunctor_car F A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
|}.
Next Obligation.
- by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_ne.
+ by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
- apply list_fmap_equiv_ext=>y. apply cFunctor_id.
+ apply list_fmap_equiv_ext=>y. apply oFunctor_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
- apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
+ apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
Qed.
-Instance listCF_contractive F :
- cFunctorContractive F → cFunctorContractive (listCF F).
+Instance listOF_contractive F :
+ oFunctorContractive F → oFunctorContractive (listOF F).
Proof.
- by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
Qed.
(* CMRA *)
@@ -463,10 +463,10 @@ Qed.
Program Definition listURF (F : urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
- urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (urFunctor_map F fg)
+ urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
|}.
Next Obligation.
- by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_ne.
+ by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
@@ -480,5 +480,5 @@ Qed.
Instance listURF_contractive F :
urFunctorContractive F → urFunctorContractive (listURF F).
Proof.
- by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
Qed.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 6285c2ab0493ac21efb46d09dac30205f8702d0b..93c2ff11755541bd73630f61c0ed5e7799a44d4a 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -62,18 +62,18 @@ Proof.
by apply (iso_ofe_mixin
(λ x, (namespace_map_data_proj x, namespace_map_token_proj x))).
Qed.
-Canonical Structure namespace_mapC :=
+Canonical Structure namespace_mapO :=
OfeT (namespace_map A) namespace_map_ofe_mixin.
Global Instance NamespaceMap_discrete a b :
Discrete a → Discrete b → Discrete (NamespaceMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
Global Instance namespace_map_ofe_discrete :
- OfeDiscrete A → OfeDiscrete namespace_mapC.
+ OfeDiscrete A → OfeDiscrete namespace_mapO.
Proof. intros ? [??]; apply _. Qed.
End ofe.
-Arguments namespace_mapC : clear implicits.
+Arguments namespace_mapO : clear implicits.
(* Camera *)
Section cmra.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 3bded308f0628a9d89e42cbd54a993c1b31fdbfd..61dc5698696761f3f7da82d7d198b1a0e2a89093 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -509,16 +509,16 @@ Section fixpointAB_ne.
End fixpointAB_ne.
(** Non-expansive function space *)
-Record ofe_mor (A B : ofeT) : Type := CofeMor {
+Record ofe_mor (A B : ofeT) : Type := OfeMor {
ofe_mor_car :> A → B;
ofe_mor_ne : NonExpansive ofe_mor_car
}.
-Arguments CofeMor {_ _} _ {_}.
+Arguments OfeMor {_ _} _ {_}.
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
Notation "'λne' x .. y , t" :=
- (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
+ (@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t) _) ..) _)
(at level 200, x binder, y binder, right associativity).
Section ofe_mor.
@@ -538,18 +538,18 @@ Section ofe_mor.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
- Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
+ Canonical Structure ofe_morO := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
- Program Definition ofe_mor_chain (c : chain ofe_morC)
+ Program Definition ofe_mor_chain (c : chain ofe_morO)
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
- Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morC := λ c,
+ Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morO := λ c,
{| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
Next Obligation.
intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
(conv_compl n (ofe_mor_chain c y)) /= Hx.
Qed.
- Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morC :=
+ Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morO :=
{| compl := ofe_mor_compl |}.
Next Obligation.
intros ? n c x; simpl.
@@ -565,20 +565,20 @@ Section ofe_mor.
Proof. done. Qed.
End ofe_mor.
-Arguments ofe_morC : clear implicits.
+Arguments ofe_morO : clear implicits.
Notation "A -n> B" :=
- (ofe_morC A B) (at level 99, B at level 200, right associativity).
+ (ofe_morO A B) (at level 99, B at level 200, right associativity).
Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
Inhabited (A -n> B) := populate (λne _, inhabitant).
(** Identity and composition and constant function *)
-Definition cid {A} : A -n> A := CofeMor id.
+Definition cid {A} : A -n> A := OfeMor id.
Instance: Params (@cid) 1 := {}.
-Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
+Definition cconst {A B : ofeT} (x : B) : A -n> B := OfeMor (const x).
Instance: Params (@cconst) 2 := {}.
Definition ccompose {A B C}
- (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
+ (f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).
Instance: Params (@ccompose) 3 := {}.
Infix "â—Ž" := ccompose (at level 40, left associativity).
Global Instance ccompose_ne {A B C} :
@@ -592,10 +592,10 @@ Instance ofe_mor_map_ne {A A' B B'} n :
Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
-Definition ofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
- (A -n> B) -n> (A' -n> B') := CofeMor (ofe_mor_map f g).
-Instance ofe_morC_map_ne {A A' B B'} :
- NonExpansive2 (@ofe_morC_map A A' B B').
+Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
+ (A -n> B) -n> (A' -n> B') := OfeMor (ofe_mor_map f g).
+Instance ofe_morO_map_ne {A A' B B'} :
+ NonExpansive2 (@ofe_morO_map A A' B B').
Proof.
intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
by repeat apply ccompose_ne.
@@ -606,12 +606,12 @@ Section unit.
Instance unit_dist : Dist unit := λ _ _ _, True.
Definition unit_ofe_mixin : OfeMixin unit.
Proof. by repeat split; try exists 0. Qed.
- Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
+ Canonical Structure unitO : ofeT := OfeT unit unit_ofe_mixin.
- Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
+ Global Program Instance unit_cofe : Cofe unitO := { compl x := () }.
Next Obligation. by repeat split; try exists 0. Qed.
- Global Instance unit_ofe_discrete : OfeDiscrete unitC.
+ Global Instance unit_ofe_discrete : OfeDiscrete unitO.
Proof. done. Qed.
End unit.
@@ -632,9 +632,9 @@ Section product.
- apply _.
- by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Qed.
- Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin.
+ Canonical Structure prodO : ofeT := OfeT (A * B) prod_ofe_mixin.
- Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC :=
+ Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
{ compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
Next Obligation.
intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
@@ -645,115 +645,115 @@ Section product.
Discrete (x.1) → Discrete (x.2) → Discrete x.
Proof. by intros ???[??]; split; apply (discrete _). Qed.
Global Instance prod_ofe_discrete :
- OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodC.
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodO.
Proof. intros ?? [??]; apply _. Qed.
End product.
-Arguments prodC : clear implicits.
+Arguments prodO : clear implicits.
Typeclasses Opaque prod_dist.
Instance prod_map_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@prod_map A A' B B').
Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
-Definition prodC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
- prodC A B -n> prodC A' B' := CofeMor (prod_map f g).
-Instance prodC_map_ne {A A' B B'} :
- NonExpansive2 (@prodC_map A A' B B').
+Definition prodO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+ prodO A B -n> prodO A' B' := OfeMor (prod_map f g).
+Instance prodO_map_ne {A A' B B'} :
+ NonExpansive2 (@prodO_map A A' B B').
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** Functors *)
-Record cFunctor := CFunctor {
- cFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
- cFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
- ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
- cFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
- NonExpansive (@cFunctor_map A1 _ A2 _ B1 _ B2 _);
- cFunctor_id `{!Cofe A, !Cofe B} (x : cFunctor_car A B) :
- cFunctor_map (cid,cid) x ≡ x;
- cFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+Record oFunctor := OFunctor {
+ oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
+ oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+ ((A2 -n> A1) * (B1 -n> B2)) → oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
+ oFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+ NonExpansive (@oFunctor_map A1 _ A2 _ B1 _ B2 _);
+ oFunctor_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
+ oFunctor_map (cid,cid) x ≡ x;
+ oFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
- cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
+ oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
-Existing Instance cFunctor_ne.
-Instance: Params (@cFunctor_map) 9 := {}.
+Existing Instance oFunctor_ne.
+Instance: Params (@oFunctor_map) 9 := {}.
-Delimit Scope cFunctor_scope with CF.
-Bind Scope cFunctor_scope with cFunctor.
+Delimit Scope oFunctor_scope with OF.
+Bind Scope oFunctor_scope with oFunctor.
-Class cFunctorContractive (F : cFunctor) :=
- cFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
- Contractive (@cFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Hint Mode cFunctorContractive ! : typeclass_instances.
+Class oFunctorContractive (F : oFunctor) :=
+ oFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+ Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
+Hint Mode oFunctorContractive ! : typeclass_instances.
-Definition cFunctor_diag (F: cFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
- cFunctor_car F A A.
+Definition oFunctor_diag (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
+ oFunctor_car F A A.
(** Note that the implicit argument [Cofe A] is not taken into account when
-[cFunctor_diag] is used as a coercion. So, given [F : cFunctor] and [A : ofeT]
+[oFunctor_diag] is used as a coercion. So, given [F : oFunctor] and [A : ofeT]
one has to write [F A _]. *)
-Coercion cFunctor_diag : cFunctor >-> Funclass.
+Coercion oFunctor_diag : oFunctor >-> Funclass.
-Program Definition constCF (B : ofeT) : cFunctor :=
- {| cFunctor_car A1 A2 _ _ := B; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
+Program Definition constOF (B : ofeT) : oFunctor :=
+ {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
-Coercion constCF : ofeT >-> cFunctor.
+Coercion constOF : ofeT >-> oFunctor.
-Instance constCF_contractive B : cFunctorContractive (constCF B).
-Proof. rewrite /cFunctorContractive; apply _. Qed.
+Instance constOF_contractive B : oFunctorContractive (constOF B).
+Proof. rewrite /oFunctorContractive; apply _. Qed.
-Program Definition idCF : cFunctor :=
- {| cFunctor_car A1 _ A2 _ := A2; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}.
+Program Definition idOF : oFunctor :=
+ {| oFunctor_car A1 _ A2 _ := A2; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}.
Solve Obligations with done.
-Notation "∙" := idCF : cFunctor_scope.
+Notation "∙" := idOF : oFunctor_scope.
-Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
- prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
+Program Definition prodOF (F1 F2 : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := prodO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+ prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
- intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodC_map_ne; apply cFunctor_ne.
+ intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_ne.
Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !cFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
- by rewrite !cFunctor_compose.
+ by rewrite !oFunctor_compose.
Qed.
-Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
+Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
-Instance prodCF_contractive F1 F2 :
- cFunctorContractive F1 → cFunctorContractive F2 →
- cFunctorContractive (prodCF F1 F2).
+Instance prodOF_contractive F1 F2 :
+ oFunctorContractive F1 → oFunctorContractive F2 →
+ oFunctorContractive (prodOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
- by apply prodC_map_ne; apply cFunctor_contractive.
+ by apply prodO_map_ne; apply oFunctor_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 :=
- ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
+Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := oFunctor_car F1 B A -n> oFunctor_car F2 A B;
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+ ofe_morO_map (oFunctor_map F1 (fg.2, fg.1)) (oFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
- apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
+ apply ofe_morO_map_ne; apply oFunctor_ne; split; by apply Hfg.
Qed.
Next Obligation.
- intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !cFunctor_id.
- apply (ne_proper f). apply cFunctor_id.
+ intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_id.
+ apply (ne_proper f). apply oFunctor_id.
Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
- rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
+ rewrite -!oFunctor_compose. do 2 apply (ne_proper _). apply oFunctor_compose.
Qed.
-Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
+Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
-Instance ofe_morCF_contractive F1 F2 :
- cFunctorContractive F1 → cFunctorContractive F2 →
- cFunctorContractive (ofe_morCF F1 F2).
+Instance ofe_morOF_contractive F1 F2 :
+ oFunctorContractive F1 → oFunctorContractive F2 →
+ oFunctorContractive (ofe_morOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
- apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split.
+ apply ofe_morO_map_ne; apply oFunctor_contractive; destruct n, Hfg; by split.
Qed.
(** Sum *)
@@ -775,21 +775,21 @@ Section sum.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
- Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin.
+ Canonical Structure sumO : ofeT := OfeT (A + B) sum_ofe_mixin.
- Program Definition inl_chain (c : chain sumC) (a : A) : chain A :=
+ Program Definition inl_chain (c : chain sumO) (a : A) : chain A :=
{| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Program Definition inr_chain (c : chain sumC) (b : B) : chain B :=
+ Program Definition inr_chain (c : chain sumO) (b : B) : chain B :=
{| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Definition sum_compl `{Cofe A, Cofe B} : Compl sumC := λ c,
+ Definition sum_compl `{Cofe A, Cofe B} : Compl sumO := λ c,
match c 0 with
| inl a => inl (compl (inl_chain c a))
| inr b => inr (compl (inr_chain c b))
end.
- Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumC :=
+ Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumO :=
{ compl := sum_compl }.
Next Obligation.
intros ?? n c; rewrite /compl /sum_compl.
@@ -803,11 +803,11 @@ Section sum.
Global Instance inr_discrete (y : B) : Discrete y → Discrete (inr y).
Proof. inversion_clear 2; constructor; by apply (discrete _). Qed.
Global Instance sum_ofe_discrete :
- OfeDiscrete A → OfeDiscrete B → OfeDiscrete sumC.
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete sumO.
Proof. intros ?? [?|?]; apply _. Qed.
End sum.
-Arguments sumC : clear implicits.
+Arguments sumO : clear implicits.
Typeclasses Opaque sum_dist.
Instance sum_map_ne {A A' B B' : ofeT} n :
@@ -816,33 +816,33 @@ Instance sum_map_ne {A A' B B' : ofeT} n :
Proof.
intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg].
Qed.
-Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
- sumC A B -n> sumC A' B' := CofeMor (sum_map f g).
-Instance sumC_map_ne {A A' B B'} :
- NonExpansive2 (@sumC_map A A' B B').
+Definition sumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+ sumO A B -n> sumO A' B' := OfeMor (sum_map f g).
+Instance sumO_map_ne {A A' B B'} :
+ NonExpansive2 (@sumO_map A A' B B').
Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
-Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
- sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
+Program Definition sumOF (F1 F2 : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := sumO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+ sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
- intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumC_map_ne; apply cFunctor_ne.
+ intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_ne.
Qed.
-Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !cFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
- by rewrite !cFunctor_compose.
+ by rewrite !oFunctor_compose.
Qed.
-Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
+Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
-Instance sumCF_contractive F1 F2 :
- cFunctorContractive F1 → cFunctorContractive F2 →
- cFunctorContractive (sumCF F1 F2).
+Instance sumOF_contractive F1 F2 :
+ oFunctorContractive F1 → oFunctorContractive F2 →
+ oFunctorContractive (sumOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
- by apply sumC_map_ne; apply cFunctor_contractive.
+ by apply sumO_map_ne; apply oFunctor_contractive.
Qed.
(** Discrete OFE *)
@@ -869,8 +869,8 @@ Section discrete_ofe.
Qed.
End discrete_ofe.
-Notation discreteC A := (OfeT A (discrete_ofe_mixin _)).
-Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
+Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
+Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
(** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
we need to determine the [Equivalence A] proof that was used to construct the
@@ -885,14 +885,14 @@ Notation discrete_ofe_equivalence_of A := ltac:(
| discrete_ofe_mixin ?H => exact H
end) (only parsing).
-Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
+Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.
-Canonical Structure boolC := leibnizC bool.
-Canonical Structure natC := leibnizC nat.
-Canonical Structure positiveC := leibnizC positive.
-Canonical Structure NC := leibnizC N.
-Canonical Structure ZC := leibnizC Z.
+Canonical Structure boolO := leibnizO bool.
+Canonical Structure natO := leibnizO nat.
+Canonical Structure positiveO := leibnizO positive.
+Canonical Structure NO := leibnizO N.
+Canonical Structure ZO := leibnizO Z.
(* Option *)
Section option.
@@ -911,14 +911,14 @@ Section option.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
- Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
+ Canonical Structure optionO := OfeT (option A) option_ofe_mixin.
- Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
+ Program Definition option_chain (c : chain optionO) (x : A) : chain A :=
{| chain_car n := default x (c n) |}.
Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Definition option_compl `{Cofe A} : Compl optionC := λ c,
+ Definition option_compl `{Cofe A} : Compl optionO := λ c,
match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
- Global Program Instance option_cofe `{Cofe A} : Cofe optionC :=
+ Global Program Instance option_cofe `{Cofe A} : Cofe optionO :=
{ compl := option_compl }.
Next Obligation.
intros ? n c; rewrite /compl /option_compl.
@@ -927,7 +927,7 @@ Section option.
destruct (c n); naive_solver.
Qed.
- Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionC.
+ Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionO.
Proof. destruct 2; constructor; by apply (discrete _). Qed.
Global Instance Some_ne : NonExpansive (@Some A).
@@ -960,7 +960,7 @@ Section option.
End option.
Typeclasses Opaque option_dist.
-Arguments optionC : clear implicits.
+Arguments optionO : clear implicits.
Instance option_fmap_ne {A B : ofeT} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
@@ -972,31 +972,31 @@ Instance option_mjoin_ne {A : ofeT} n:
Proper (dist n ==> dist n) (@mjoin option _ A).
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
-Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
- CofeMor (fmap f : optionC A → optionC B).
-Instance optionC_map_ne A B : NonExpansive (@optionC_map A B).
+Definition optionO_map {A B} (f : A -n> B) : optionO A -n> optionO B :=
+ OfeMor (fmap f : optionO A → optionO B).
+Instance optionO_map_ne A B : NonExpansive (@optionO_map A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
-Program Definition optionCF (F : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := optionC (cFunctor_car F A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (cFunctor_map F fg)
+Program Definition optionOF (F : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := optionO (oFunctor_car F A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (oFunctor_map F fg)
|}.
Next Obligation.
- by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_ne.
+ by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
- apply option_fmap_equiv_ext=>y; apply cFunctor_id.
+ apply option_fmap_equiv_ext=>y; apply oFunctor_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
- apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
+ apply option_fmap_equiv_ext=>y; apply oFunctor_compose.
Qed.
-Instance optionCF_contractive F :
- cFunctorContractive F → cFunctorContractive (optionCF F).
+Instance optionOF_contractive F :
+ oFunctorContractive F → oFunctorContractive (optionOF F).
Proof.
- by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_contractive.
Qed.
(** Later *)
@@ -1026,12 +1026,12 @@ Section later.
+ by intros [x] [y] [z] ??; trans y.
- intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
Qed.
- Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
+ Canonical Structure laterO : ofeT := OfeT (later A) later_ofe_mixin.
- Program Definition later_chain (c : chain laterC) : chain A :=
+ Program Definition later_chain (c : chain laterO) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
- Global Program Instance later_cofe `{Cofe A} : Cofe laterC :=
+ Global Program Instance later_cofe `{Cofe A} : Cofe laterO :=
{ compl c := Next (compl (later_chain c)) }.
Next Obligation.
intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
@@ -1058,7 +1058,7 @@ Section later.
Qed.
End later.
-Arguments laterC : clear implicits.
+Arguments laterO : clear implicits.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
Next (f (later_car x)).
@@ -1074,47 +1074,50 @@ Proof. by destruct x. Qed.
Lemma later_map_ext {A B : ofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
Proof. destruct x; intros Hf; apply Hf. Qed.
-Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
- CofeMor (later_map f).
-Instance laterC_map_contractive (A B : ofeT) : Contractive (@laterC_map A B).
+Definition laterO_map {A B} (f : A -n> B) : laterO A -n> laterO B :=
+ OfeMor (later_map f).
+Instance laterO_map_contractive (A B : ofeT) : Contractive (@laterO_map A B).
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
-Program Definition laterCF (F : cFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := laterC (cFunctor_car F A B);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterC_map (cFunctor_map F fg)
+Program Definition laterOF (F : oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := laterO (oFunctor_car F A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterO_map (oFunctor_map F fg)
|}.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
- by apply (contractive_ne laterC_map), cFunctor_ne.
+ by apply (contractive_ne laterO_map), oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(later_map_id x).
- apply later_map_ext=>y. by rewrite cFunctor_id.
+ apply later_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 -later_map_compose.
- apply later_map_ext=>y; apply cFunctor_compose.
+ apply later_map_ext=>y; apply oFunctor_compose.
Qed.
-Notation "â–¶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
+Notation "â–¶ F" := (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
-Instance laterCF_contractive F : cFunctorContractive (laterCF F).
+Instance laterOF_contractive F : oFunctorContractive (laterOF F).
Proof.
- intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterC_map_contractive.
- destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
+ intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
+ destruct n as [|n]; simpl in *; first done. apply oFunctor_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.
+(** Dependently-typed functions over a discrete domain *)
+(** We make [discrete_fun] a definition so that we can register it as a
+canonical structure. Note that non-dependent functions over a discrete domain,
+[discrete_fun (λ _, A) B] (or [A -d> B] following the notation we introduce
+below) are isomorphic to [leibnizC A -n> B]. In other words, since the domain
+is discrete, we get non-expansiveness for free. *)
+Definition discrete_fun {A} (B : A → ofeT) := ∀ x : A, B x.
-Section ofe_fun.
+Section discrete_fun.
Context {A : Type} {B : A → ofeT}.
- Implicit Types f g : ofe_fun B.
+ Implicit Types f g : discrete_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).
+ Instance discrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.
+ Instance discrete_fun_dist : Dist (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Definition discrete_fun_ofe_mixin : OfeMixin (discrete_fun B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -1125,18 +1128,18 @@ Section ofe_fun.
+ 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.
+ Canonical Structure discrete_funO := OfeT (discrete_fun B) discrete_fun_ofe_mixin.
- Program Definition ofe_fun_chain `(c : chain ofe_funC)
+ Program Definition discrete_fun_chain `(c : chain discrete_funO)
(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 Program Instance discrete_fun_cofe `{∀ x, Cofe (B x)} : Cofe discrete_funO :=
+ { compl c x := compl (discrete_fun_chain c x) }.
+ Next Obligation. intros ? n c x. apply (conv_compl n (discrete_fun_chain c x)). Qed.
- Global Instance ofe_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited ofe_funC :=
+ Global Instance discrete_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited discrete_funO :=
populate (λ _, inhabitant).
- Global Instance ofe_fun_lookup_discrete `{EqDecision A} f x :
+ Global Instance discrete_fun_lookup_discrete `{EqDecision A} f x :
Discrete f → Discrete (f x).
Proof.
intros Hf y ?.
@@ -1146,62 +1149,62 @@ Section ofe_fun.
unfold g. destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).
Qed.
-End ofe_fun.
+End discrete_fun.
-Arguments ofe_funC {_} _.
-Notation "A -c> B" :=
- (@ofe_funC A (λ _, B)) (at level 99, B at level 200, right associativity).
+Arguments discrete_funO {_} _.
+Notation "A -d> B" :=
+ (@discrete_funO 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).
+Definition discrete_fun_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
+ (g : discrete_fun B1) : discrete_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.
+Lemma discrete_fun_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
+ (g : discrete_fun B1) :
+ (∀ x, f1 x (g x) ≡ f2 x (g x)) → discrete_fun_map f1 g ≡ discrete_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.
+Lemma discrete_fun_map_id {A} {B : A → ofeT} (g : discrete_fun B) :
+ discrete_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).
+Lemma discrete_fun_map_compose {A} {B1 B2 B3 : A → ofeT}
+ (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : discrete_fun B1) :
+ discrete_fun_map (λ x, f2 x ∘ f1 x) g = discrete_fun_map f2 (discrete_fun_map f1 g).
Proof. done. Qed.
-Instance ofe_fun_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
+Instance discrete_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.
+ Proper (dist n ==> dist n) (discrete_fun_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /discrete_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).
+Definition discrete_funO_map {A} {B1 B2 : A → ofeT} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
+ discrete_funO B1 -n> discrete_funO B2 := OfeMor (discrete_fun_map f).
+Instance discrete_funO_map_ne {A} {B1 B2 : A → ofeT} :
+ NonExpansive (@discrete_funO_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)
+Program Definition discrete_funOF {C} (F : C → oFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := discrete_funO (λ c, oFunctor_car (F c) A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
|}.
Next Obligation.
- intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
+ intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply oFunctor_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.
+ intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
+ apply discrete_fun_map_ext=> y; apply oFunctor_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.
+ rewrite /= -discrete_fun_map_compose.
+ apply discrete_fun_map_ext=>y; apply oFunctor_compose.
Qed.
-Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
+Notation "T -d> F" := (@discrete_funOF T%type (λ _, F%OF)) : oFunctor_scope.
-Instance ofe_funCF_contractive {C} (F : C → cFunctor) :
- (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
+Instance discrete_funOF_contractive {C} (F : C → oFunctor) :
+ (∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
- by apply ofe_funC_map_ne=>c; apply cFunctor_contractive.
+ by apply discrete_funO_map_ne=>c; apply oFunctor_contractive.
Qed.
(** Constructing isomorphic OFEs *)
@@ -1268,15 +1271,15 @@ Section sigma.
Proof. by intros n [a Ha] [b Hb] ?. Qed.
Definition sig_ofe_mixin : OfeMixin (sig P).
Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
- Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
+ Canonical Structure sigO : ofeT := OfeT (sig P) sig_ofe_mixin.
- Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigC.
+ Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
Global Instance sig_discrete (x : sig P) : Discrete (`x) → Discrete x.
Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (discrete _). Qed.
- Global Instance sig_ofe_discrete : OfeDiscrete A → OfeDiscrete sigC.
+ Global Instance sig_ofe_discrete : OfeDiscrete A → OfeDiscrete sigO.
Proof. intros ??. apply _. Qed.
End sigma.
-Arguments sigC {_} _.
+Arguments sigO {_} _.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index fc51c1906ac32de936e8aad269f9fdaf0704748b..c5d07b8579261248035aa23d6daff46d0e58cf8a 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -272,7 +272,7 @@ End sts_dra.
(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
-Notation stsC sts := (validityC (stsDR sts)).
+Notation stsC sts := (validityO (stsDR sts)).
Notation stsR sts := (validityR (stsDR sts)).
Section sts_definitions.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 1b378db332bf62a98772e3e548dd6322c7e64d77..42d9645d7bf3d47fee58e245c3692957ba9c3797 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -11,7 +11,7 @@ infers the [frac] camera by default when using the [Qp] type. *)
Definition ufrac := Qp.
Section ufrac.
-Canonical Structure ufracC := leibnizC ufrac.
+Canonical Structure ufracO := leibnizO ufrac.
Instance ufrac_valid : Valid ufrac := λ x, True.
Instance ufrac_pcore : PCore ufrac := λ _, None.
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index f8d073ba13ea447141006d1fffc88308673ca7df..a03666a98fd1a81da963d4f2ee7ab08129fce155 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -11,9 +11,9 @@ Section ofe.
Definition vec_ofe_mixin m : OfeMixin (vec A m).
Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
- Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m).
+ Canonical Structure vecO m : ofeT := OfeT (vec A m) (vec_ofe_mixin m).
- Global Instance list_cofe `{Cofe A} m : Cofe (vecC m).
+ Global Instance list_cofe `{Cofe A} m : Cofe (vecO m).
Proof.
apply: (iso_cofe_subtype (λ l : list A, length l = m)
(λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
@@ -29,11 +29,11 @@ Section ofe.
intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
constructor. by apply discrete. change (v ≡ v'). by apply discrete.
Qed.
- Global Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecC m).
+ Global Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecO m).
Proof. intros ? v. induction v; apply _. Qed.
End ofe.
-Arguments vecC : clear implicits.
+Arguments vecO : clear implicits.
Typeclasses Opaque vec_dist.
Section proper.
@@ -66,7 +66,7 @@ Section proper.
End proper.
(** Functor *)
-Definition vec_map {A B : ofeT} m (f : A → B) : vecC A m → vecC B m :=
+Definition vec_map {A B : ofeT} m (f : A → B) : vecO A m → vecO B m :=
@vmap A B f m.
Lemma vec_map_ext_ne {A B : ofeT} m (f g : A → B) (v : vec A m) n :
(∀ x, f x ≡{n}≡ g x) → vec_map m f v ≡{n}≡ vec_map m g v.
@@ -81,33 +81,33 @@ Proof.
intros ? v v' H. eapply list_fmap_ne in H; last done.
by rewrite -!vec_to_list_map in H.
Qed.
-Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m :=
- CofeMor (vec_map m f).
-Instance vecC_map_ne {A A'} m :
- NonExpansive (@vecC_map A A' m).
+Definition vecO_map {A B : ofeT} m (f : A -n> B) : vecO A m -n> vecO B m :=
+ OfeMor (vec_map m f).
+Instance vecO_map_ne {A A'} m :
+ NonExpansive (@vecO_map A A' m).
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
-Program Definition vecCF (F : cFunctor) m : cFunctor := {|
- cFunctor_car A _ B _ := vecC (cFunctor_car F A B) m;
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecC_map m (cFunctor_map F fg)
+Program Definition vecOF (F : oFunctor) m : oFunctor := {|
+ oFunctor_car A _ B _ := vecO (oFunctor_car F A B) m;
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
|}.
Next Obligation.
- intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
+ intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F m A ? B ? l.
- change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l) ≡ l).
- rewrite vec_to_list_map. apply listCF.
+ change (vec_to_list (vec_map m (oFunctor_map F (cid, cid)) l) ≡ l).
+ rewrite vec_to_list_map. apply listOF.
Qed.
Next Obligation.
intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
- change (vec_to_list (vec_map m (cFunctor_map F (f â—Ž g, g' â—Ž f')) l)
- ≡ vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)).
- rewrite !vec_to_list_map. by apply: (cFunctor_compose (listCF F) f g f' g').
+ change (vec_to_list (vec_map m (oFunctor_map F (f â—Ž g, g' â—Ž f')) l)
+ ≡ vec_map m (oFunctor_map F (g, g')) (vec_map m (oFunctor_map F (f, f')) l)).
+ rewrite !vec_to_list_map. by apply: (oFunctor_compose (listOF F) f g f' g').
Qed.
-Instance vecCF_contractive F m :
- cFunctorContractive F → cFunctorContractive (vecCF F m).
+Instance vecOF_contractive F m :
+ oFunctorContractive F → oFunctorContractive (vecOF F m).
Proof.
- by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecC_map_ne; first apply cFunctor_contractive.
+ by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_contractive.
Qed.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 72c3ea3e31e2fe3fc2e5b651e1dc8f8b4deee30c..1d3758f02a1bceae2473ca4906726732970aa97e 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -202,8 +202,8 @@ Lemma option_validI {A : cmraT} (mx : option A) :
Proof. exact: uPred_primitive.option_validI. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
+Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
(** Consistency/soundness statement *)
Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌠→ φ.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 600b2ad191f6afbad0626db89af71faa5e87d2eb..9d71aab4d32667404baedee3bf0f20126cbbc41b 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -7,10 +7,10 @@ Import uPred.
(** The CMRAs we need. *)
Class boxG Σ :=
boxG_inG :> inG Σ (prodR
- (authR (optionUR (exclR boolC)))
- (optionR (agreeR (laterC (iPreProp Σ))))).
+ (authR (optionUR (exclR boolO)))
+ (optionR (agreeR (laterO (iPreProp Σ))))).
-Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
+Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
optionRF (agreeRF (▶ ∙)) ) ].
Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 4ae29954887ec45b41c6609ad833ff92505d66c1..0efa3739a8a3ade1804870814ccfae15b6943bd4 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -58,12 +58,12 @@ of both values and ghost names for meta information, for example:
this RA would be quite inconvenient to deal with. *)
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
- gmapUR L (prodR fracR (agreeR (leibnizC V))).
+ gmapUR L (prodR fracR (agreeR (leibnizO V))).
Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
gmapUR L (agreeR gnameC).
Definition to_gen_heap {L V} `{Countable L} : gmap L V → gen_heapUR L V :=
- fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
+ fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
Definition to_gen_meta `{Countable L} : gmap L gname → gen_metaUR L :=
fmap to_agree.
@@ -71,7 +71,7 @@ Definition to_gen_meta `{Countable L} : gmap L gname → gen_metaUR L :=
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_meta_inG :> inG Σ (authR (gen_metaUR L));
- gen_meta_data_inG :> inG Σ (namespace_mapR (agreeR positiveC));
+ gen_meta_data_inG :> inG Σ (namespace_mapR (agreeR positiveO));
gen_heap_name : gname;
gen_meta_name : gname
}.
@@ -81,13 +81,13 @@ Arguments gen_meta_name {_ _ _ _ _} _ : assert.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
- gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveC));
+ gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveO));
}.
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
GFunctor (authR (gen_heapUR L V));
GFunctor (authR (gen_metaUR L));
- GFunctor (namespace_mapR (agreeR positiveC))
+ GFunctor (namespace_mapR (agreeR positiveO))
].
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
@@ -105,7 +105,7 @@ Section definitions.
own (gen_meta_name hG) (â— (to_gen_meta m)))%I.
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
- own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
+ own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizO V)) ]}).
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
@@ -151,7 +151,7 @@ Section to_gen_heap.
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed.
Lemma to_gen_heap_insert l v σ :
- to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
+ to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO V))]> (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_insert. Qed.
Lemma to_gen_meta_valid m : ✓ to_gen_meta m.
@@ -304,7 +304,7 @@ Section gen_heap.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
- (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
+ (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizO _)))=> //.
by apply lookup_to_gen_heap_None. }
iMod (own_alloc (namespace_map_token ⊤)) as (γm) "Hγm".
{ apply namespace_map_token_valid. }
@@ -350,7 +350,7 @@ Section gen_heap.
as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
- (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
+ (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizO _)))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 34945d66892760632936bbb4ffa197d9d5b2d61a..0062aa9cd71de7e1ffbfcb5f7462272423bd786d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -45,11 +45,11 @@ Definition gFunctors_lookup (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
Coercion gFunctors_lookup : gFunctors >-> Funclass.
Definition gname := positive.
-Canonical Structure gnameC := leibnizC gname.
+Canonical Structure gnameC := leibnizO gname.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor :=
- ofe_funURF (λ i, gmapURF gname (Σ i)).
+ discrete_funURF (λ i, gmapURF gname (Σ i)).
(** We define functions for the empty list of functors, the singleton list of
@@ -120,8 +120,8 @@ Module Type iProp_solution_sig.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
Definition iResUR (Σ : gFunctors) : ucmraT :=
- ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
- Notation iProp Σ := (uPredC (iResUR Σ)).
+ discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
+ Notation iProp Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)).
@@ -136,13 +136,13 @@ End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Σ : gFunctors) :
- solution (uPredCF (iResF Σ)) := solver.result _.
+ solution (uPredOF (iResF Σ)) := solver.result _.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT :=
- ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
- Notation iProp Σ := (uPredC (iResUR Σ)).
+ discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
+ Notation iProp Σ := (uPredO (iResUR Σ)).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
solution_fold (iProp_result Σ).
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 4540dc68f1946e536437665cd3a7abc37b768590..822b32f30330798256bdd1240fb75abd38ad84dd 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -48,7 +48,7 @@ Ltac solve_inG :=
(** * Definition of the connective [own] *)
Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
- ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
+ discrete_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4 := {}.
Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
@@ -67,11 +67,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 ofe_fun_singleton_ne; rewrite Ha. Qed.
+Proof. by intros n a a' Ha; apply discrete_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 ofe_fun_op_singleton op_singleton cmra_transport_op.
+ by rewrite /iRes_singleton discrete_fun_op_singleton op_singleton cmra_transport_op.
Qed.
(** ** Properties of [own] *)
@@ -91,7 +91,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 ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
+ rewrite discrete_fun_validI (forall_elim (inG_id _)) discrete_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.
@@ -116,7 +116,7 @@ Proof.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
- rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
+ rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
{ by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
rewrite -except_0_intro -(exist_intro (cmra_transport (eq_sym inG_prf) b)).
@@ -125,15 +125,15 @@ Proof.
cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
by (by intros ?? ->).
apply ownM_mono=> /=.
- exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
- intros i'. rewrite ofe_fun_lookup_op.
+ exists (discrete_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
+ intros i'. rewrite discrete_fun_lookup_op.
destruct (decide (i' = inG_id _)) as [->|?].
- + rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
+ + rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
* by rewrite lookup_singleton lookup_delete Hb.
* by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
- + rewrite ofe_fun_lookup_insert_ne //.
- by rewrite ofe_fun_lookup_singleton_ne // left_id.
+ + rewrite discrete_fun_lookup_insert_ne //.
+ by rewrite discrete_fun_lookup_singleton_ne // left_id.
- apply later_mono.
by assert (∀ {A A' : cmraT} (Heq : A' = A) (a' : A') (a : A),
cmra_transport Heq a' ≡ a ⊢@{iPropI Σ}
@@ -150,7 +150,7 @@ Proof.
intros HP Ha.
rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ a⌠∧ uPred_ownM m)%I).
- rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
- eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
+ eapply bupd_ownM_updateP, (discrete_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 ->]].
@@ -176,7 +176,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, ofe_fun_singleton_updateP;
+ - eapply bupd_ownM_updateP, discrete_fun_singleton_updateP;
first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
@@ -209,7 +209,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
- apply bupd_ownM_update, ofe_fun_singleton_update_empty.
+ apply bupd_ownM_update, discrete_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/proph_map.v b/theories/base_logic/lib/proph_map.v
index 1158cd502259be76be9d0af2917ae52c5ac74b7c..28962d6cb847994872931281ec300323e14fd12b 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -8,10 +8,10 @@ Local Notation proph_map P V := (gmap P (list V)).
Definition proph_val_list (P V : Type) := list (P * V).
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
- gmapUR P $ exclR $ listC $ leibnizC V.
+ gmapUR P $ exclR $ listO $ leibnizO V.
Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
- fmap (λ vs, Excl (vs : list (leibnizC V))) pvs.
+ fmap (λ vs, Excl (vs : list (leibnizO V))) pvs.
(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
@@ -88,7 +88,7 @@ Section to_proph_map.
Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
Lemma to_proph_map_insert p vs R :
- to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizC V))]> (to_proph_map R).
+ to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizO V))]> (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_insert. Qed.
Lemma to_proph_map_delete p R :
@@ -170,7 +170,7 @@ Section proph_map.
{ (* FIXME: FIXME(Coq #6294): needs new unification *)
eapply auth_update. apply: singleton_local_update.
- by rewrite /to_proph_map lookup_fmap HR.
- - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
+ - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizO V)))). }
rewrite /to_proph_map -fmap_insert.
iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
- iPureIntro. done.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index f844bcc0bb63f6d6e8c150f87a74ab2ad95c6bd2..2af2c2712b171376218f3f8f27131dceac20591b 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -8,20 +8,20 @@ Import uPred.
(* "Saved anything" -- this can give you saved propositions, saved predicates,
saved whatever-you-like. *)
-Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := SavedAnythingG {
+Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _));
- saved_anything_contractive : cFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
+ saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
-Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ].
-Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
+Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ) _) : iProp Σ :=
- own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
+ own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4 := {}.
@@ -57,11 +57,11 @@ Section saved_anything.
iIntros "Hx Hy". rewrite /saved_anything_own.
iDestruct (own_valid_2 with "Hx Hy") as "Hv".
rewrite agree_validI agree_equivI.
- set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
- set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
+ set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
+ set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert (∀ z, G2 (G1 z) ≡ z) as help.
- { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
- apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
+ { intros z. rewrite /G1 /G2 -oFunctor_compose -{2}[z]oFunctor_id.
+ apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
Qed.
End saved_anything.
@@ -99,14 +99,14 @@ Proof.
Qed.
(* Saved predicates. *)
-Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
-Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
+Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ ∙)).
+Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
- saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
+ saved_anything_own (F := A -d> ▶ ∙) γ (OfeMor Next ∘ Φ).
Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
- Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
+ Contractive (saved_pred_own γ : (A -d> iProp Σ) → iProp Σ).
Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
Qed.
@@ -130,5 +130,5 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
Proof.
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 "?".
+ by iDestruct (discrete_fun_equivI with "Heq") as "?".
Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index d6538bff82ef4ea3d461af873dc806a8f2dcc7c9..6ffb41ff725616ab7e44b9e07fae6ac257635f84 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
Module invG.
Class invG (Σ : gFunctors) : Set := WsatG {
- inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+ inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
enabled_inG :> inG Σ coPset_disjR;
disabled_inG :> inG Σ (gset_disjR positive);
invariant_name : gname;
@@ -18,12 +18,12 @@ Module invG.
}.
Definition invΣ : gFunctors :=
- #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+ #[GFunctor (authRF (gmapURF positive (agreeRF (laterOF idOF))));
GFunctor coPset_disjUR;
GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG {
- inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+ inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive);
}.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index df7df317133753818dcaf439eb01f4d8fd17d04e..9ba56ac869bec30087823a8331d0136003e9c32e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -80,23 +80,23 @@ Section cofe.
by trans (Q i x);[apply HP|apply HQ].
- intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
Qed.
- Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
+ Canonical Structure uPredO : ofeT := OfeT (uPred M) uPred_ofe_mixin.
- Program Definition uPred_compl : Compl uPredC := λ c,
+ Program Definition uPred_compl : Compl uPredO := λ c,
{| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'}x → c n' n' x |}.
Next Obligation.
move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
eapply cmra_includedN_le=>//; lia. done.
Qed.
- Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
+ Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
Next Obligation.
intros n c; split=>i x Hin Hv.
etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
Qed.
End cofe.
-Arguments uPredC : clear implicits.
+Arguments uPredO : clear implicits.
Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
@@ -150,23 +150,23 @@ Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
`{!CmraMorphism f} `{!CmraMorphism g}:
(∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
- uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
-Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
+Definition uPredO_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
+ uPredO M1 -n> uPredO M2 := OfeMor (uPred_map f : uPredO M1 → uPredO M2).
+Lemma uPredO_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
`{!CmraMorphism f, !CmraMorphism g} n :
- f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
+ f ≡{n}≡ g → uPredO_map f ≡{n}≡ uPredO_map g.
Proof.
by intros Hfg P; split=> n' y ??;
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.
-Program Definition uPredCF (F : urFunctor) : cFunctor := {|
- cFunctor_car A _ B _ := uPredC (urFunctor_car F B A);
- cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
+Program Definition uPredOF (F : urFunctor) : oFunctor := {|
+ oFunctor_car A _ B _ := uPredO (urFunctor_car F B A);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
- apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
+ apply uPredO_map_ne, urFunctor_ne; split; by apply HPQ.
Qed.
Next Obligation.
intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
@@ -177,10 +177,10 @@ Next Obligation.
apply uPred_map_ext=>y; apply urFunctor_compose.
Qed.
-Instance uPredCF_contractive F :
- urFunctorContractive F → cFunctorContractive (uPredCF F).
+Instance uPredOF_contractive F :
+ urFunctorContractive F → oFunctorContractive (uPredOF F).
Proof.
- intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
+ intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredO_map_ne, urFunctor_contractive.
destruct n; split; by apply HPQ.
Qed.
@@ -398,7 +398,7 @@ Proof.
- intros HPQ; split; split=> x i; apply HPQ.
- intros [??]. exact: entails_anti_sym.
Qed.
-Lemma entails_lim (cP cQ : chain (uPredC M)) :
+Lemma entails_lim (cP cQ : chain (uPredO M)) :
(∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
Proof.
intros Hlim; split=> n m ? HP.
@@ -693,10 +693,10 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
-Lemma fun_ext {A} {B : A → ofeT} (g1 g2 : ofe_fun B) :
+Lemma fun_ext {A} {B : A → ofeT} (g1 g2 : discrete_fun B) :
(∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
Proof. by unseal. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) :
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigO P) :
proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
Proof. by unseal. Qed.
@@ -797,7 +797,7 @@ Proof. unseal. by destruct mx. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. by unseal. Qed.
(** Consistency/soundness statement *)
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 8e6b4e1b8042a29edf1a383aaa6a2d1baee02794..a9883b41da68679ab94a6613af1cd622f9b52e89 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -84,21 +84,21 @@ Qed.
Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
-Lemma ofe_fun_equivI {A} {B : A → ofeT} (f g : ofe_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof.
apply (anti_symm _); auto using fun_ext.
apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
Qed.
-Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma ofe_morO_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof.
apply (anti_symm _).
- apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
- - rewrite -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
+ - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
set (h1 (f : A -n> B) :=
- exist (λ f : A -c> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
- set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A → B))) :=
- @CofeMor A B (`f) (proj2_sig f)).
+ exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
+ set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
+ @OfeMor A B (`f) (proj2_sig f)).
assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 738ced79e280d16c7f289bc2722a94f55092c740..3d3ea3b860ff401c580599f2f18074f3f8b8e6bc 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -125,7 +125,7 @@ Section bi_mixin.
sbi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a;
sbi_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
- sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
+ sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ;
@@ -168,8 +168,8 @@ Structure bi := Bi {
bi_exist bi_sep bi_wand bi_persistently;
}.
-Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
-Canonical Structure bi_ofeC.
+Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
+Canonical Structure bi_ofeO.
Instance: Params (@bi_entails) 1 := {}.
Instance: Params (@bi_emp) 1 := {}.
@@ -230,8 +230,8 @@ Instance: Params (@sbi_internal_eq) 1 := {}.
Arguments sbi_later {PROP} _%I : simpl never, rename.
Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
-Coercion sbi_ofeC (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
-Canonical Structure sbi_ofeC.
+Coercion sbi_ofeO (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
+Canonical Structure sbi_ofeO.
Coercion sbi_bi (PROP : sbi) : bi :=
{| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}.
Canonical Structure sbi_bi.
@@ -423,7 +423,7 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
-Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) :
+Lemma fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) :
(∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) :
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 7485c5280f886d4cb8ee8007a7266f2bc8dbffe1..1423040d92826018c0680a2ca337180a353e6299 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -44,7 +44,7 @@ Section least.
Lemma least_fixpoint_unfold_1 x :
bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
Proof.
- iIntros "HF". iApply ("HF" $! (CofeMor (F (bi_least_fixpoint F))) with "[#]").
+ iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2.
Qed.
@@ -58,7 +58,7 @@ Section least.
Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
□ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof.
- iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
+ iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (OfeMor Φ) with "[#]").
Qed.
Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
@@ -107,7 +107,7 @@ Section greatest.
Lemma greatest_fixpoint_unfold_2 x :
F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
Proof.
- iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))).
+ iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed.
@@ -120,5 +120,5 @@ Section greatest.
Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
□ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
- Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
+ Proof. iIntros "#HΦ" (x) "Hx". iExists (OfeMor Φ). auto. Qed.
End greatest.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6a75a8459c034adbd16185032db46e587c282036..9e9fe6a05908dac779199b51d81746b852a1383c 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -40,10 +40,10 @@ Section Ofe_Cofe_def.
{ monPred_in_dist i : P i ≡{n}≡ Q i }.
Instance monPred_dist : Dist monPred := monPred_dist'.
- Definition monPred_sig P : { f : I -c> PROP | Proper ((⊑) ==> (⊢)) f } :=
+ Definition monPred_sig P : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f } :=
exist _ (monPred_at P) (monPred_mono P).
- Definition sig_monPred (P' : { f : I -c> PROP | Proper ((⊑) ==> (⊢)) f })
+ Definition sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f })
: monPred :=
MonPred (proj1_sig P') (proj2_sig P').
@@ -60,18 +60,18 @@ Section Ofe_Cofe_def.
Definition monPred_ofe_mixin : OfeMixin monPred.
Proof. by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist). Qed.
- Canonical Structure monPredC := OfeT monPred monPred_ofe_mixin.
+ Canonical Structure monPredO := OfeT monPred monPred_ofe_mixin.
- Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredC.
+ Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredO.
Proof.
- unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_at _ _ _);
+ unshelve refine (iso_cofe_subtype (A:=I-d>PROP) _ MonPred monPred_at _ _ _);
[apply _|by apply monPred_sig_dist|done|].
intros c i j Hij. apply @limit_preserving;
[by apply bi.limit_preserving_entails; intros ??|]=>n. by rewrite Hij.
Qed.
End Ofe_Cofe_def.
-Lemma monPred_sig_monPred (P' : { f : I -c> PROP | Proper ((⊑) ==> (⊢)) f }) :
+Lemma monPred_sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f }) :
monPred_sig (sig_monPred P') ≡ P'.
Proof. by change (P' ≡ P'). Qed.
Lemma sig_monPred_sig P : sig_monPred (monPred_sig P) ≡ P.
@@ -107,7 +107,7 @@ End Ofe_Cofe.
Arguments monPred _ _ : clear implicits.
Arguments monPred_at {_ _} _%I _.
Local Existing Instance monPred_mono.
-Arguments monPredC _ _ : clear implicits.
+Arguments monPredO _ _ : clear implicits.
(** BI and SBI structures. *)
@@ -840,7 +840,7 @@ Proof.
apply bi.equiv_spec. split.
- apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
- by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
- -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
+ -bi.f_equiv -bi.sig_equivI !bi.discrete_fun_equivI.
Qed.
(** Objective *)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 0791353e7adb17ce1b9c602579143f26b158255b..c38fdfc5acd12ea63e3a430d0c5cbe4a8507e8f4 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -351,10 +351,10 @@ Instance state_inhabited : Inhabited state :=
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
-Canonical Structure stateC := leibnizC state.
-Canonical Structure locC := leibnizC loc.
-Canonical Structure valC := leibnizC val.
-Canonical Structure exprC := leibnizC expr.
+Canonical Structure stateO := leibnizO state.
+Canonical Structure locO := leibnizO loc.
+Canonical Structure valO := leibnizO val.
+Canonical Structure exprO := leibnizO expr.
(** Evaluation contexts *)
Inductive ectx_item :=
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index a213fec88bfa18f4926cb90472bb32f0af781c66..7e698d52bbe39eb5b94ee5c18be0986285120d36 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -19,8 +19,8 @@ Definition join : val :=
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
+Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 5b010185c020dba618f23713ae646fbfd00e15f7..695cd759a9feb025dffa2eb185dbafc5db2bf1d2 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -14,8 +14,8 @@ Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
+Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index a3c6010703a90dff6299f920de677d4802cc9f06..0fb6f0aa8047e5720e640c202f34b07a04393795 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -29,9 +29,9 @@ Definition release : val :=
(** The CMRAs we need. *)
Class tlockG Σ :=
- tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
+ tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
Definition tlockΣ : gFunctors :=
- #[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
+ #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. solve_inG. Qed.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index e6f6e0f33987ff0d21e8f7191e532a94b2ef4f54..a1a6b7c6d58f22106136b87e8888fa5479dd8079 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -37,9 +37,9 @@ Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _ _.
-Canonical Structure stateC Λ := leibnizC (state Λ).
-Canonical Structure valC Λ := leibnizC (val Λ).
-Canonical Structure exprC Λ := leibnizC (expr Λ).
+Canonical Structure stateO Λ := leibnizO (state Λ).
+Canonical Structure valO Λ := leibnizO (val Λ).
+Canonical Structure exprO Λ := leibnizO (expr Λ).
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index a99eaa683aceed22b09865490f8bd8c06ec2952e..40f4763f94dd1f05d7895876f7aeb87d4dd9b1f3 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -16,7 +16,7 @@ union.
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ;
- ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
+ ownP_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))));
ownP_name : gname;
}.
@@ -29,11 +29,11 @@ Global Opaque iris_invG.
Definition ownPΣ (Λ : language) : gFunctors :=
#[invΣ;
- GFunctor (authR (optionUR (exclR (stateC Λ))))].
+ GFunctor (authR (optionUR (exclR (stateO Λ))))].
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_invG :> invPreG Σ;
- ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))))
+ ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))))
}.
Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 3b964c1fe6e944f5b6d3e6692ca42aa7e55db2fc..9ab29cf73e84b91398d9090e775206a8a7d20f35 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -37,8 +37,8 @@ Qed.
(* Uncurry [twp_pre] and equip its type with an OFE structure *)
Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
- (prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ) →
- prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ :=
+ (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ) →
+ prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ :=
curry3 ∘ twp_pre s ∘ uncurry3.
Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
@@ -76,7 +76,7 @@ Lemma twp_ind s Ψ :
Proof.
iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
set (Ψ' := curry3 Ψ :
- prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ).
+ prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ).
assert (NonExpansive Ψ').
{ intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f26a223b9bbdaa1f912e9d4c3ca16015bb1b51de..134ce595b8ff85757ce4178af75f51eafbff083b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -23,8 +23,8 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
Global Opaque iris_invG.
Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
- (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
- coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
+ (wp : coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ) :
+ coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,