Commit cc9470e0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

parent ccc5ddf9
......@@ -66,6 +66,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
* Move `algebra.base` module to `prelude.prelude`.
* Strengthen `cmra_op_discrete` to assume only `✓{0} (x1 ⋅ x2)` instead of `✓
(x1 ⋅ x2)`.
* Rename the types `ofeT``ofe`, `cmraT``cmra`, `ucmraT``ucmra`, and the
constructors `OfeT``Ofe`, and `CmraT``Cmra`, since the `T` suffix is not
needed. This change makes these names consistent with `bi` and `Ucmra`,
which also do not have a `T` suffix.
**Changes in `bi`:**
......@@ -215,6 +219,12 @@ s/\bgen_heap_ctx\b/gen_heap_interp/g
s/\bproph_map_ctx\b/proph_map_interp/g
# other gen_heap changes
s/\bmapsto_mapsto_ne\b/mapsto_frac_ne/g
# remove Ts in algebra
s/\bofeT\b/ofe/g
s/\bOfeT\b/Ofe/g
s/\bcmraT\b/cmra/g
s/\bCmraT\b/Cmra/g
s/\bcmraT\b/ucmra/g
EOF
```
......
......@@ -50,7 +50,7 @@ Proof.
Qed.
Section agree.
Context {A : ofeT}.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
......@@ -74,7 +74,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 agreeO := OfeT (agree A) agree_ofe_mixin.
Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
......@@ -147,7 +147,7 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin.
Canonical Structure agreeR : cmra := Cmra (agree A) agree_cmra_mixin.
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
......@@ -275,7 +275,7 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
Proof. by apply agree_eq. Qed.
Section agree_map.
Context {A B : ofeT} (f : A B) {Hf: NonExpansive f}.
Context {A B : ofe} (f : A B) {Hf: NonExpansive f}.
Local Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Type*.
......
......@@ -12,9 +12,9 @@ agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
(** * Definition of the view relation *)
(** The authoritative camera is obtained by instantiating the view camera. *)
Definition auth_view_rel_raw {A : ucmraT} (n : nat) (a b : A) : Prop :=
Definition auth_view_rel_raw {A : ucmra} (n : nat) (a b : A) : Prop :=
b {n} a {n} a.
Lemma auth_view_rel_raw_mono (A : ucmraT) n1 n2 (a1 a2 b1 b2 : A) :
Lemma auth_view_rel_raw_mono (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
auth_view_rel_raw n1 a1 b1
a1 {n2} a2
b2 {n2} b1
......@@ -25,26 +25,26 @@ Proof.
- trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
- rewrite -Ha12. by apply cmra_validN_le with n1.
Qed.
Lemma auth_view_rel_raw_valid (A : ucmraT) n (a b : A) :
Lemma auth_view_rel_raw_valid (A : ucmra) n (a b : A) :
auth_view_rel_raw n a b {n} b.
Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
Lemma auth_view_rel_raw_unit (A : ucmraT) n :
Lemma auth_view_rel_raw_unit (A : ucmra) n :
a : A, auth_view_rel_raw n a ε.
Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
Canonical Structure auth_view_rel {A : ucmraT} : view_rel A A :=
Canonical Structure auth_view_rel {A : ucmra} : view_rel A A :=
ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
(auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
Lemma auth_view_rel_unit {A : ucmraT} n (a : A) : auth_view_rel n a ε {n} a.
Lemma auth_view_rel_unit {A : ucmra} n (a : A) : auth_view_rel n a ε {n} a.
Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
Lemma auth_view_rel_exists {A : ucmraT} n (b : A) :
Lemma auth_view_rel_exists {A : ucmra} n (b : A) :
( a, auth_view_rel n a b) {n} b.
Proof.
split; [|intros; exists b; by split].
intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
Qed.
Global Instance auth_view_rel_discrete {A : ucmraT} :
Global Instance auth_view_rel_discrete {A : ucmra} :
CmraDiscrete A ViewRelDiscrete (auth_view_rel (A:=A)).
Proof.
intros ? n a b [??]; split.
......@@ -54,15 +54,15 @@ Qed.
(** * Definition and operations on the authoritative camera *)
(** The type [auth] is not defined as a [Definition], but as a [Notation].
This way, one can use [auth A] with [A : Type] instead of [A : ucmraT], and let
This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
canonical structure search determine the corresponding camera instance. *)
Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
Definition authO (A : ucmraT) : ofeT := viewO (A:=A) (B:=A) auth_view_rel.
Definition authR (A : ucmraT) : cmraT := viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR (A : ucmraT) : ucmraT := viewUR (A:=A) (B:=A) auth_view_rel.
Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
Definition auth_auth {A: ucmraT} : Qp A auth A := view_auth.
Definition auth_frag {A: ucmraT} : A auth A := view_frag.
Definition auth_auth {A: ucmra} : Qp A auth A := view_auth.
Definition auth_frag {A: ucmra} : A auth A := view_frag.
Typeclasses Opaque auth_auth auth_frag.
......@@ -78,7 +78,7 @@ Notation "● a" := (auth_auth 1 a) (at level 20).
general version in terms of [●] and [◯], and because such a lemma has never
been needed in practice. *)
Section auth.
Context {A : ucmraT}.
Context {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
......
This diff is collapsed.
......@@ -3,14 +3,14 @@ From iris.algebra Require Export big_op cmra.
From iris.prelude Require Import options.
(** Option *)
Lemma big_opL_None {M : cmraT} {A} (f : nat A option M) l :
Lemma big_opL_None {M : cmra} {A} (f : nat A option M) l :
([^op list] kx l, f k x) = None k x, l !! k = Some x f k x = None.
Proof.
revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
- intros [??] [|k] y ?; naive_solver.
- intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
Qed.
Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K A option M) m :
Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K A option M) m :
([^op map] kx m, f k x) = None k x, m !! k = Some x f k x = None.
Proof.
induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
......@@ -20,13 +20,13 @@ Proof.
- apply (Hm i). by simplify_map_eq.
- intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.
Lemma big_opS_None {M : cmraT} `{Countable A} (f : A option M) X :
Lemma big_opS_None {M : cmra} `{Countable A} (f : A option M) X :
([^op set] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
Qed.
Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A option M) X :
Lemma big_opMS_None {M : cmra} `{Countable A} (f : A option M) X :
([^op mset] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X IH] using gmultiset_ind.
......
......@@ -44,7 +44,7 @@ Section coPset.
Lemma coPset_ucmra_mixin : UcmraMixin coPset.
Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
......@@ -117,5 +117,5 @@ Section coPset_disj.
Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
Canonical Structure coPset_disjUR := UcmraT coPset_disj coPset_disj_ucmra_mixin.
Canonical Structure coPset_disjUR := Ucmra coPset_disj coPset_disj_ucmra_mixin.
End coPset_disj.
......@@ -2,7 +2,7 @@ From iris.algebra Require Export ofe.
From iris.prelude Require Import options.
Record solution (F : oFunctor) := Solution {
solution_car :> ofeT;
solution_car :> ofe;
solution_cofe : Cofe solution_car;
solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}.
......@@ -10,11 +10,11 @@ Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
Context `{Fcofe : (T : ofeT) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
Context `{Fcofe : (T : ofe) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
Notation map := (oFunctor_map F).
Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
Fixpoint A' (k : nat) : { C : ofe & Cofe C } :=
match k with
| 0 => existT (P:=Cofe) unitO _
| S k => existT (P:=Cofe) (@oFunctor_apply F (projT1 (A' k)) (projT2 (A' k))) _
......@@ -64,7 +64,7 @@ Proof.
- intros k X Y HXY n; apply dist_S.
by rewrite -(g_tower X) (HXY (S n)) g_tower.
Qed.
Definition T : ofeT := OfeT tower tower_ofe_mixin.
Definition T : ofe := Ofe tower tower_ofe_mixin.
Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
{| chain_car i := c i k |}.
......
......@@ -27,7 +27,7 @@ Global Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
match x with Cinr b => Some b | _ => None end.
Section ofe.
Context {A B : ofeT}.
Context {A B : ofe}.
Implicit Types a : A.
Implicit Types b : B.
......@@ -73,7 +73,7 @@ Proof.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
Qed.
Canonical Structure csumO : ofeT := OfeT (csum A B) csum_ofe_mixin.
Canonical Structure csumO : ofe := Ofe (csum A B) csum_ofe_mixin.
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 |}.
......@@ -128,10 +128,10 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
(g : B B') (g' : B' B'') (x : csum A B) :
csum_map (f' f) (g' g) x = csum_map f' g' (csum_map f g x).
Proof. by destruct x. Qed.
Lemma csum_map_ext {A A' B B' : ofeT} (f f' : A A') (g g' : B B') x :
Lemma csum_map_ext {A A' B B' : ofe} (f f' : A A') (g g' : B B') x :
( x, f x f' x) ( x, g x g' x) csum_map f g x csum_map f' g' x.
Proof. by destruct x; constructor. Qed.
Global Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
Global Instance csum_map_cmra_ne {A A' B B' : ofe} 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.
......@@ -143,7 +143,7 @@ Global Instance csumO_map_ne A A' B B' :
Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
Section cmra.
Context {A B : cmraT}.
Context {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
......@@ -257,7 +257,7 @@ Proof.
exists (Cinr z1), (Cinr z2). by repeat constructor.
+ by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
Qed.
Canonical Structure csumR := CmraT (csum A B) csum_cmra_mixin.
Canonical Structure csumR := Cmra (csum A B) csum_cmra_mixin.
Global Instance csum_cmra_discrete :
CmraDiscrete A CmraDiscrete B CmraDiscrete csumR.
......@@ -369,7 +369,7 @@ End cmra.
Global Arguments csumR : clear implicits.
(* Functor *)
Global Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A A') (g : B B') :
Global Instance csum_map_cmra_morphism {A A' B B' : cmra} (f : A A') (g : B B') :
CmraMorphism f CmraMorphism g CmraMorphism (csum_map f g).
Proof.
split; try apply _.
......
......@@ -118,7 +118,7 @@ Proof.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
split; [|intros; trans y]; tauto.
Qed.
Canonical Structure validityO : ofeT := discreteO (validity A).
Canonical Structure validityO : ofe := discreteO (validity A).
Local Instance dra_valid_proper' : Proper (() ==> iff) (valid : A Prop).
Proof. by split; apply: dra_valid_proper. Qed.
......@@ -177,7 +177,7 @@ Proof.
intros. rewrite Hy //. tauto.
- by intros [x px ?] [y py ?] (?&?&?).
Qed.
Canonical Structure validityR : cmraT :=
Canonical Structure validityR : cmra :=
discreteR (validity A) validity_ra_mixin.
Global Instance validity_disrete_cmra : CmraDiscrete validityR.
......
......@@ -21,7 +21,7 @@ Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
Section excl.
Context {A : ofeT}.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
......@@ -50,7 +50,7 @@ Proof.
- by intros [a|] [b|]; split; inversion_clear 1; constructor.
- by intros n [a|] [b|]; split; inversion_clear 1; constructor.
Qed.
Canonical Structure exclO : ofeT := OfeT (excl A) excl_ofe_mixin.
Canonical Structure exclO : ofe := Ofe (excl A) excl_ofe_mixin.
Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
Proof.
......@@ -89,7 +89,7 @@ Proof.
- by intros n [?|] [?|].
- intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
Qed.
Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.
Global Instance excl_cmra_discrete : OfeDiscrete A CmraDiscrete exclR.
Proof. split; first apply _. by intros []. Qed.
......@@ -125,13 +125,13 @@ Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A B) (g : B C) (x : excl A) :
excl_map (g f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : ofeT} (f g : A B) x :
Lemma excl_map_ext {A B : ofe} (f g : A B) x :
( x, f x g x) excl_map f x excl_map g x.
Proof. by destruct x; constructor. Qed.
Global Instance excl_map_ne {A B : ofeT} n :
Global Instance excl_map_ne {A B : ofe} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Global Instance excl_map_cmra_morphism {A B : ofeT} (f : A B) :
Global Instance excl_map_cmra_morphism {A B : ofe} (f : A B) :
NonExpansive f CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
......
......@@ -3,17 +3,17 @@ From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From iris.prelude Require Import options.
Definition discrete_fun_insert `{EqDecision A} {B : A ofeT}
Definition discrete_fun_insert `{EqDecision A} {B : A ofe}
(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.
Global Instance: Params (@discrete_fun_insert) 5 := {}.
Definition discrete_fun_singleton `{EqDecision A} {B : A ucmraT}
Definition discrete_fun_singleton `{EqDecision A} {B : A ucmra}
(x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
Global Instance: Params (@discrete_fun_singleton) 5 := {}.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A ofeT}.
Context `{Heqdec : EqDecision A} {B : A ofe}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
......@@ -52,7 +52,7 @@ Section ofe.
End ofe.
Section cmra.
Context `{EqDecision A} {B : A ucmraT}.
Context `{EqDecision A} {B : A ucmra}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
......
......@@ -4,7 +4,7 @@ From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
Section ofe.
Context `{Countable K} {A : ofeT}.
Context `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
......@@ -22,7 +22,7 @@ Proof.
+ by intros m1 m2 m3 ?? k; trans (m2 !! k).
- by intros n m1 m2 ? k; apply dist_S.
Qed.
Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
Canonical Structure gmapO : ofe := Ofe (gmap K A) gmap_ofe_mixin.
Program Definition gmap_chain (c : chain gmapO)
(k : K) : chain (optionO A) := {| chain_car n := c n !! k |}.
......@@ -100,22 +100,22 @@ End ofe.
Global Arguments gmapO _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A option B option C)
Lemma merge_ne `{Countable K} {A B C : ofe} (f g : option A option B option C)
`{!DiagNone f, !DiagNone g} n :
((dist n) ==> (dist n) ==> (dist n))%signature f g
((dist n) ==> (dist n) ==> (dist n))%signature (merge (M:=gmap K) f) (merge g).
Proof. by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge //; apply Hf. Qed.
Global Instance union_with_proper `{Countable K} {A : ofeT} n :
Global Instance union_with_proper `{Countable K} {A : ofe} n :
Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
(dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Global Instance map_fmap_proper `{Countable K} {A B : ofeT} (f : A B) n :
Global Instance map_fmap_proper `{Countable K} {A B : ofe} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
Global Instance map_zip_with_proper `{Countable K} {A B C : ofeT} (f : A B C) n :
Global Instance map_zip_with_proper `{Countable K} {A B C : ofe} (f : A B C) n :
Proper (dist n ==> dist n ==> dist n) f
Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
......@@ -123,7 +123,7 @@ Proof.
destruct 1; destruct 1; repeat f_equiv; constructor || done.
Qed.
Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofeT} (f g : K A M) m1 m2 n :
Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofe} (f g : K A M) m1 m2 n :
m1 {n} m2
( k y1 y2,
m1 !! k = Some y1 m2 !! k = Some y2 y1 {n} y2 f k y1 {n} g k y2)
......@@ -138,7 +138,7 @@ Qed.
(* CMRA *)
Section cmra.
Context `{Countable K} {A : cmraT}.
Context `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Local Instance gmap_unit : Unit (gmap K A) := ( : gmap K A).
......@@ -216,7 +216,7 @@ Proof.
+ revert Hz1i. case: (y1!!i)=>[?|] //.
+ revert Hz2i. case: (y2!!i)=>[?|] //.
Qed.
Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin.
Canonical Structure gmapR := Cmra (gmap K A) gmap_cmra_mixin.
Global Instance gmap_cmra_discrete : CmraDiscrete A CmraDiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
......@@ -228,7 +228,7 @@ Proof.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.
End cmra.
......@@ -236,7 +236,7 @@ Global Arguments gmapR _ {_ _} _.
Global Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
Context `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
......@@ -594,7 +594,7 @@ Proof.
[done|by rewrite lookup_singleton].
Qed.
Lemma gmap_fmap_mono {B : cmraT} (f : A B) m1 m2 :
Lemma gmap_fmap_mono {B : cmra} (f : A B) m1 m2 :
Proper (() ==> ()) f
( x y, x y f x f y) m1 m2 fmap f m1 fmap f m2.
Proof.
......@@ -620,7 +620,7 @@ Qed.
End properties.
Section unital_properties.
Context `{Countable K} {A : ucmraT}.
Context `{Countable K} {A : ucmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
......@@ -643,10 +643,10 @@ Qed.
End unital_properties.
(** Functor *)
Global Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A B) n :
Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A B)
Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmra} (f : A B)
`{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A gmap K B).
Proof.
split; try apply _.
......
......@@ -51,7 +51,7 @@ Section gmultiset.
split; [done | | done]. intros X.
by rewrite gmultiset_op_disj_union left_id_L.
Qed.
Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
Canonical Structure gmultisetUR := Ucmra (gmultiset K) gmultiset_ucmra_mixin.
Global Instance gmultiset_cancelable X : Cancelable X.
Proof.
......
......@@ -38,7 +38,7 @@ Section gset.
Lemma gset_ucmra_mixin : UcmraMixin (gset K).
Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
......@@ -132,7 +132,7 @@ Section gset_disj.
Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
Canonical Structure gset_disjUR := Ucmra (gset_disj K) gset_disj_ucmra_mixin.
Local Arguments op _ _ _ _ : simpl never.
......
......@@ -6,14 +6,14 @@ From iris.prelude Require Import options.
This is effectively a single "ghost variable" with two views, the frament [◯E a]
and the authority [●E a]. *)
Definition excl_authR (A : ofeT) : cmraT :=
Definition excl_authR (A : ofe) : cmra :=
authR (optionUR (exclR A)).
Definition excl_authUR (A : ofeT) : ucmraT :=
Definition excl_authUR (A : ofe) : ucmra :=
authUR (optionUR (exclR A)).
Definition excl_auth_auth {A : ofeT} (a : A) : excl_authR A :=
Definition excl_auth_auth {A : ofe} (a : A) : excl_authR A :=
(Some (Excl a)).
Definition excl_auth_frag {A : ofeT} (a : A) : excl_authR A :=
Definition excl_auth_frag {A : ofe} (a : A) : excl_authR A :=
(Some (Excl a)).
Typeclasses Opaque excl_auth_auth excl_auth_frag.
......@@ -25,7 +25,7 @@ Notation "●E a" := (excl_auth_auth a) (at level 10).
Notation "◯E a" := (excl_auth_frag a) (at level 10).
Section excl_auth.
Context {A :