From cc9470e02a1e7b197633e479ca742dc86ff051ae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2021 12:04:33 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20`ofeT`=E2=86=92`ofe`,=20`cmraT`?=
=?UTF-8?q?=E2=86=92`cmra`,=20and=20`ucmraT`=E2=86=92`ucmra`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
CHANGELOG.md | 10 ++
iris/algebra/agree.v | 8 +-
iris/algebra/auth.v | 30 ++--
iris/algebra/cmra.v | 132 +++++++--------
iris/algebra/cmra_big_op.v | 8 +-
iris/algebra/coPset.v | 4 +-
iris/algebra/cofe_solver.v | 8 +-
iris/algebra/csum.v | 14 +-
iris/algebra/dra.v | 4 +-
iris/algebra/excl.v | 12 +-
iris/algebra/functions.v | 8 +-
iris/algebra/gmap.v | 30 ++--
iris/algebra/gmultiset.v | 2 +-
iris/algebra/gset.v | 4 +-
iris/algebra/lib/excl_auth.v | 10 +-
iris/algebra/lib/frac_agree.v | 6 +-
iris/algebra/lib/frac_auth.v | 10 +-
iris/algebra/lib/gmap_view.v | 14 +-
iris/algebra/lib/gset_bij.v | 6 +-
iris/algebra/lib/ufrac_auth.v | 10 +-
iris/algebra/list.v | 32 ++--
iris/algebra/local_updates.v | 20 +--
iris/algebra/monoid.v | 6 +-
iris/algebra/namespace_map.v | 14 +-
iris/algebra/numbers.v | 12 +-
iris/algebra/ofe.v | 160 +++++++++----------
iris/algebra/proofmode_classes.v | 18 +--
iris/algebra/updates.v | 14 +-
iris/algebra/vector.v | 14 +-
iris/algebra/view.v | 18 +--
iris/base_logic/algebra.v | 30 ++--
iris/base_logic/bi.v | 26 +--
iris/base_logic/bupd_alt.v | 4 +-
iris/base_logic/derived.v | 16 +-
iris/base_logic/lib/auth.v | 4 +-
iris/base_logic/lib/gen_inv_heap.v | 2 +-
iris/base_logic/lib/iprop.v | 8 +-
iris/base_logic/lib/own.v | 6 +-
iris/base_logic/proofmode.v | 4 +-
iris/base_logic/upred.v | 64 ++++----
iris/bi/big_op.v | 4 +-
iris/bi/derived_laws.v | 6 +-
iris/bi/embedding.v | 4 +-
iris/bi/interface.v | 4 +-
iris/bi/internal_eq.v | 80 +++++-----
iris/bi/lib/fixpoint.v | 20 +--
iris/bi/lib/relations.v | 12 +-
iris/bi/monpred.v | 8 +-
iris/bi/plainly.v | 6 +-
iris/proofmode/class_instances_embedding.v | 2 +-
iris/proofmode/class_instances_internal_eq.v | 20 +--
iris/proofmode/classes.v | 2 +-
iris/proofmode/coq_tactics.v | 4 +-
iris/proofmode/frame_instances.v | 2 +-
iris/proofmode/monpred.v | 4 +-
iris/si_logic/bi.v | 2 +-
iris/si_logic/siprop.v | 22 +--
tests/algebra.v | 4 +-
tests/ipm_paper.ref | 8 +-
tests/ipm_paper.v | 8 +-
tests/proofmode.v | 6 +-
tests/proofmode_ascii.v | 2 +-
tests/proofmode_iris.v | 2 +-
63 files changed, 522 insertions(+), 512 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4f286c5b2..acc6f0398 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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
```
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 6c938682a..089456dee 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -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*.
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 52306f467..702b0b33b 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -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.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index d4cb19cce..5ba38dff3 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -66,7 +66,7 @@ Section mixin.
End mixin.
(** Bundled version *)
-Structure cmraT := CmraT' {
+Structure cmra := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
@@ -77,11 +77,11 @@ Structure cmraT := CmraT' {
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
-Global Arguments CmraT' _ {_ _ _ _ _ _} _ _.
-(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
+Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.
+(* Given [m : CmraMixin A], the notation [Cmra A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
-Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m) (only parsing).
+Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Arguments cmra_car : simpl never.
Global Arguments cmra_equiv : simpl never.
@@ -92,21 +92,21 @@ Global Arguments cmra_valid : simpl never.
Global Arguments cmra_validN : simpl never.
Global Arguments cmra_ofe_mixin : simpl never.
Global Arguments cmra_mixin : simpl never.
-Add Printing Constructor cmraT.
+Add Printing Constructor cmra.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
-Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
+Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
-Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
+Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
(** Lifting properties from the mixin *)
Section cmra_mixin.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types x y : A.
Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
@@ -138,38 +138,38 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
-Definition opM {A : cmraT} (x : A) (my : option A) :=
+Definition opM {A : cmra} (x : A) (my : option A) :=
match my with Some y => x â‹… y | None => x end.
Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
-Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
+Class CoreId {A : cmra} (x : A) := core_id : pcore x ≡ Some x.
Global Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
Global Instance: Params (@CoreId) 1 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
-Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
+Class Exclusive {A : cmra} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
Global Arguments exclusive0_l {_} _ {_} _ _.
Global Hint Mode Exclusive + ! : typeclass_instances.
Global Instance: Params (@Exclusive) 1 := {}.
(** * Cancelable elements. *)
-Class Cancelable {A : cmraT} (x : A) :=
+Class Cancelable {A : cmra} (x : A) :=
cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
Global Arguments cancelableN {_} _ {_} _ _ _ _.
Global Hint Mode Cancelable + ! : typeclass_instances.
Global Instance: Params (@Cancelable) 1 := {}.
(** * Identity-free elements. *)
-Class IdFree {A : cmraT} (x : A) :=
+Class IdFree {A : cmra} (x : A) :=
id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
Global Arguments id_free0_r {_} _ {_} _ _.
Global Hint Mode IdFree + ! : typeclass_instances.
Global Instance: Params (@IdFree) 1 := {}.
(** * CMRAs whose core is total *)
-Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
+Class CmraTotal (A : cmra) := cmra_total (x : A) : is_Some (pcore x).
Global Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
@@ -188,7 +188,7 @@ Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
}.
-Structure ucmraT := UcmraT' {
+Structure ucmra := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
@@ -201,9 +201,9 @@ Structure ucmraT := UcmraT' {
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
-Global Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
-Notation UcmraT A m :=
- (UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
+Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
+Notation Ucmra A m :=
+ (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Arguments ucmra_car : simpl never.
Global Arguments ucmra_equiv : simpl never.
Global Arguments ucmra_dist : simpl never.
@@ -214,17 +214,17 @@ Global Arguments ucmra_validN : simpl never.
Global Arguments ucmra_ofe_mixin : simpl never.
Global Arguments ucmra_cmra_mixin : simpl never.
Global Arguments ucmra_mixin : simpl never.
-Add Printing Constructor ucmraT.
+Add Printing Constructor ucmra.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
-Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
+Coercion ucmra_ofeO (A : ucmra) : ofe := Ofe 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).
+Coercion ucmra_cmraR (A : ucmra) : cmra :=
+ Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
Section ucmra_mixin.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types x y : A.
Lemma ucmra_unit_valid : ✓ (ε : A).
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
@@ -235,14 +235,14 @@ Section ucmra_mixin.
End ucmra_mixin.
(** * Discrete CMRAs *)
-Class CmraDiscrete (A : cmraT) := {
+Class CmraDiscrete (A : cmra) := {
cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
}.
Global Hint Mode CmraDiscrete ! : typeclass_instances.
(** * Morphisms *)
-Class CmraMorphism {A B : cmraT} (f : A → B) := {
+Class CmraMorphism {A B : cmra} (f : A → B) := {
cmra_morphism_ne :> NonExpansive f;
cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
@@ -254,7 +254,7 @@ Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
(** * Properties **)
Section cmra.
-Context {A : cmraT}.
+Context {A : cmra}.
Implicit Types x y z : A.
Implicit Types xs ys zs : list A.
@@ -626,7 +626,7 @@ End cmra.
(** * Properties about CMRAs with a unit element **)
Section ucmra.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types x y z : A.
Lemma ucmra_unit_validN n : ✓{n} (ε:A).
@@ -658,7 +658,7 @@ Global Hint Immediate cmra_unit_cmra_total : core.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
Local Set Default Proof Using "Type*".
- Context {A : cmraT} `{!LeibnizEquiv A}.
+ Context {A : cmra} `{!LeibnizEquiv A}.
Implicit Types x y : A.
Global Instance cmra_assoc_L : Assoc (=) (@op A _).
@@ -705,7 +705,7 @@ End cmra_leibniz.
Section ucmra_leibniz.
Local Set Default Proof Using "Type*".
- Context {A : ucmraT} `{!LeibnizEquiv A}.
+ Context {A : ucmra} `{!LeibnizEquiv A}.
Implicit Types x y z : A.
Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
@@ -746,7 +746,7 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
-Global Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
+Global Instance cmra_morphism_id {A : cmra} : CmraMorphism (@id A).
Proof.
split => /=.
- apply _.
@@ -754,9 +754,9 @@ Proof.
- intros. by rewrite option_fmap_id.
- done.
Qed.
-Global Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
+Global Instance cmra_morphism_proper {A B : cmra} (f : A → B) `{!CmraMorphism f} :
Proper ((≡) ==> (≡)) f := ne_proper _.
-Global Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+Global Instance cmra_morphism_compose {A B C : cmra} (f : A → B) (g : B → C) :
CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
Proof.
split.
@@ -768,7 +768,7 @@ Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
- Context {A B : cmraT} (f : A → B) `{!CmraMorphism f}.
+ Context {A B : cmra} (f : A → B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
@@ -781,7 +781,7 @@ End cmra_morphism.
(** COFE → CMRA Functors *)
Record rFunctor := RFunctor {
- rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
+ rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmra;
rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -806,7 +806,7 @@ Class rFunctorContractive (F : rFunctor) :=
rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
+Definition rFunctor_apply (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
rFunctor_car F A A.
Program Definition rFunctor_to_oFunctor (F: rFunctor) : oFunctor := {|
@@ -862,17 +862,17 @@ Proof.
f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.
-Program Definition constRF (B : cmraT) : rFunctor :=
+Program Definition constRF (B : cmra) : rFunctor :=
{| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
-Coercion constRF : cmraT >-> rFunctor.
+Coercion constRF : cmra >-> rFunctor.
Global Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
(** COFE → UCMRA Functors *)
Record urFunctor := URFunctor {
- urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
+ urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmra;
urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -897,7 +897,7 @@ Class urFunctorContractive (F : urFunctor) :=
urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
+Definition urFunctor_apply (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
urFunctor_car F A A.
Program Definition urFunctor_to_rFunctor (F: urFunctor) : rFunctor := {|
@@ -953,24 +953,24 @@ Proof.
f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.
-Program Definition constURF (B : ucmraT) : urFunctor :=
+Program Definition constURF (B : ucmra) : urFunctor :=
{| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
-Coercion constURF : ucmraT >-> urFunctor.
+Coercion constURF : ucmra >-> urFunctor.
Global Instance constURF_contractive B : urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.
(** * Transporting a CMRA equality *)
-Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
+Definition cmra_transport {A B : cmra} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
-Lemma cmra_transport_trans {A B C : cmraT} (H1 : A = B) (H2 : B = C) x :
+Lemma cmra_transport_trans {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
Proof. by destruct H2. Qed.
Section cmra_transport.
- Context {A B : cmraT} (H : A = B).
+ Context {A B : cmra} (H : A = B).
Notation T := (cmra_transport H).
Global Instance cmra_transport_ne : NonExpansive T.
Proof. by intros ???; destruct H. Qed.
@@ -1023,7 +1023,7 @@ Section discrete.
Qed.
Local Instance discrete_cmra_discrete :
- CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
+ CmraDiscrete (Cmra' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Proof. split; first apply _. done. Qed.
End discrete.
@@ -1031,7 +1031,7 @@ End discrete.
[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
Notation discreteR A ra_mix :=
- (CmraT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
+ (Cmra A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Section ra_total.
@@ -1068,12 +1068,12 @@ Section unit.
Local Instance unit_op : Op () := λ x y, ().
Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
- Canonical Structure unitR : cmraT := CmraT unit unit_cmra_mixin.
+ Canonical Structure unitR : cmra := Cmra unit unit_cmra_mixin.
Local Instance unit_unit : Unit () := ().
Lemma unit_ucmra_mixin : UcmraMixin ().
Proof. done. Qed.
- Canonical Structure unitUR : ucmraT := UcmraT unit unit_ucmra_mixin.
+ Canonical Structure unitUR : ucmra := Ucmra unit unit_ucmra_mixin.
Global Instance unit_cmra_discrete : CmraDiscrete unitR.
Proof. done. Qed.
@@ -1091,7 +1091,7 @@ Section empty.
Local Instance Empty_set_op : Op Empty_set := λ x y, x.
Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
- Canonical Structure Empty_setR : cmraT := CmraT Empty_set Empty_set_cmra_mixin.
+ Canonical Structure Empty_setR : cmra := Cmra Empty_set Empty_set_cmra_mixin.
Global Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
Proof. done. Qed.
@@ -1103,7 +1103,7 @@ End empty.
(** ** Product *)
Section prod.
- Context {A B : cmraT}.
+ Context {A B : cmra}.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_/.
@@ -1166,7 +1166,7 @@ Section prod.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
- Canonical Structure prodR := CmraT (prod A B) prod_cmra_mixin.
+ Canonical Structure prodR := Cmra (prod A B) prod_cmra_mixin.
Lemma pair_op (a a' : A) (b b' : B) : (a â‹… a', b â‹… b') = (a, b) â‹… (a', b').
Proof. done. Qed.
@@ -1228,7 +1228,7 @@ Global Hint Extern 4 (CoreId _) =>
Global Arguments prodR : clear implicits.
Section prod_unit.
- Context {A B : ucmraT}.
+ Context {A B : ucmra}.
Local Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
Lemma prod_ucmra_mixin : UcmraMixin (A * B).
@@ -1238,7 +1238,7 @@ Section prod_unit.
- by split; rewrite /=left_id.
- rewrite prod_pcore_Some'; split; apply (core_id _).
Qed.
- Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
+ Canonical Structure prodUR := Ucmra (prod A B) prod_ucmra_mixin.
Lemma pair_split (a : A) (b : B) : (a, b) ≡ (a, ε) ⋅ (ε, b).
Proof. by rewrite -pair_op left_id right_id. Qed.
@@ -1264,7 +1264,7 @@ End prod_unit.
Global Arguments prodUR : clear implicits.
-Global Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+Global Instance prod_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B → B') :
CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
split; first apply _.
@@ -1327,7 +1327,7 @@ Qed.
(** ** CMRA for the option type *)
Section option.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types a b : A.
Implicit Types ma mb : option A.
Local Arguments core _ _ !_ /.
@@ -1425,7 +1425,7 @@ Section option.
+ by exists None, (Some a); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
- Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
+ Canonical Structure optionR := Cmra (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
@@ -1433,7 +1433,7 @@ Section option.
Local Instance option_unit : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split; [done| |done]. by intros []. Qed.
- Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
+ Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
(** Misc *)
Lemma op_None ma mb : ma ⋅ mb = None ↔ ma = None ∧ mb = None.
@@ -1518,7 +1518,7 @@ Global Arguments optionR : clear implicits.
Global Arguments optionUR : clear implicits.
Section option_prod.
- Context {A B : cmraT}.
+ Context {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
@@ -1543,7 +1543,7 @@ Section option_prod.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
-Lemma option_fmap_mono {A B : cmraT} (f : A → B) ma mb :
+Lemma option_fmap_mono {A B : cmra} (f : A → B) ma mb :
Proper ((≡) ==> (≡)) f →
(∀ a b, a ≼ b → f a ≼ f b) →
ma ≼ mb → f <$> ma ≼ f <$> mb.
@@ -1551,7 +1551,7 @@ Proof.
intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
-Global Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
+Global Instance option_fmap_cmra_morphism {A B : cmra} (f: A → B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
@@ -1594,7 +1594,7 @@ Proof. apply optionURF_contractive. Qed.
(* Dependently-typed functions over a discrete domain *)
Section discrete_fun_cmra.
- Context `{B : A → ucmraT}.
+ Context `{B : A → ucmra}.
Implicit Types f g : discrete_fun B.
Local Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
@@ -1640,7 +1640,7 @@ Section discrete_fun_cmra.
split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
by destruct (FUN x) as (?&?&?&?&?).
Qed.
- Canonical Structure discrete_funR := CmraT (discrete_fun B) discrete_fun_cmra_mixin.
+ Canonical Structure discrete_funR := Cmra (discrete_fun B) discrete_fun_cmra_mixin.
Local Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
@@ -1652,7 +1652,7 @@ Section discrete_fun_cmra.
- by intros f x; rewrite discrete_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
- Canonical Structure discrete_funUR := UcmraT (discrete_fun B) discrete_fun_ucmra_mixin.
+ Canonical Structure discrete_funUR := Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
Global Instance discrete_fun_unit_discrete :
(∀ i, Discrete (ε : B i)) → Discrete (ε : discrete_fun B).
@@ -1662,7 +1662,7 @@ End discrete_fun_cmra.
Global Arguments discrete_funR {_} _.
Global Arguments discrete_funUR {_} _.
-Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
+Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
(∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
Proof.
split; first apply _.
@@ -1695,7 +1695,7 @@ Qed.
(** * Constructing a camera [B] through a bijection with [A] that
is mostly an isomorphism but restricts validity. *)
-Lemma iso_cmra_mixin_restrict {A : cmraT} {B : Type}
+Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type}
`{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
@@ -1753,7 +1753,7 @@ Proof.
Qed.
(** * Constructing a camera through an isomorphism *)
-Lemma iso_cmra_mixin {A : cmraT} {B : Type}
+Lemma iso_cmra_mixin {A : cmra} {B : Type}
`{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
diff --git a/iris/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
index 73e7d22f3..9f105e214 100644
--- a/iris/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -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] k↦x ∈ 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] k↦x ∈ 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.
diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v
index 8763d0d30..0cd54e269 100644
--- a/iris/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -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.
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 4a2c745cd..69fea2571 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -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 |}.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 95fe7172d..72d750cb6 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -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 _.
diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index af0baf70e..c3e7706af 100644
--- a/iris/algebra/dra.v
+++ b/iris/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 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.
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 655c6315d..959fcf1ae 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -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 :=
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 9ff96afff..529e24031 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -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.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index f41d0cbe7..45f1fe156 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -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 _.
diff --git a/iris/algebra/gmultiset.v b/iris/algebra/gmultiset.v
index 02c3aa9f1..4f04081a1 100644
--- a/iris/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -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.
diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 6ad3aecba..4f6ea4efe 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -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.
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index 97fc0395d..b1cda8d1d 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -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 : ofeT}.
+ Context {A : ofe}.
Implicit Types a b : A.
Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth A).
diff --git a/iris/algebra/lib/frac_agree.v b/iris/algebra/lib/frac_agree.v
index 6812ca9a6..8355f3aec 100644
--- a/iris/algebra/lib/frac_agree.v
+++ b/iris/algebra/lib/frac_agree.v
@@ -2,13 +2,13 @@ From iris.algebra Require Export frac agree updates local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.prelude Require Import options.
-Definition frac_agreeR (A : ofeT) : cmraT := prodR fracR (agreeR A).
+Definition frac_agreeR (A : ofe) : cmra := prodR fracR (agreeR A).
-Definition to_frac_agree {A : ofeT} (q : frac) (a : A) : frac_agreeR A :=
+Definition to_frac_agree {A : ofe} (q : frac) (a : A) : frac_agreeR A :=
(q, to_agree a).
Section lemmas.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types (q : frac) (a : A).
Global Instance to_frac_agree_ne q : NonExpansive (@to_frac_agree A q).
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 6a6da0da1..b3558b166 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -9,14 +9,14 @@ From iris.prelude Require Import options.
split the authoritative part into fractions.
*)
-Definition frac_authR (A : cmraT) : cmraT :=
+Definition frac_authR (A : cmra) : cmra :=
authR (optionUR (prodR fracR A)).
-Definition frac_authUR (A : cmraT) : ucmraT :=
+Definition frac_authUR (A : cmra) : ucmra :=
authUR (optionUR (prodR fracR A)).
-Definition frac_auth_auth {A : cmraT} (x : A) : frac_authR A :=
+Definition frac_auth_auth {A : cmra} (x : A) : frac_authR A :=
â— (Some (1%Qp,x)).
-Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
+Definition frac_auth_frag {A : cmra} (q : frac) (x : A) : frac_authR A :=
â—¯ (Some (q,x)).
Typeclasses Opaque frac_auth_auth frac_auth_frag.
@@ -29,7 +29,7 @@ Notation "â—¯F{ q } a" := (frac_auth_frag q a) (at level 10, format "â—¯F{ q }
Notation "â—¯F a" := (frac_auth_frag 1 a) (at level 10).
Section frac_auth.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types a b : A.
Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth A).
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 12e9b7252..a2b8591e4 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -20,12 +20,12 @@ NOTE: The API surface for [gmap_view] is experimental and subject to change. We
plan to add notations for authoritative elements and fragments, and hope to
support arbitrary maps as fragments. *)
-Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
gmapUR K (prodR dfracR (agreeR V)).
(** View relation. *)
Section rel.
- Context (K : Type) `{Countable K} (V : ofeT).
+ Context (K : Type) `{Countable K} (V : ofe).
Implicit Types (m : gmap K V) (k : K) (v : V) (n : nat).
Implicit Types (f : gmap K (dfrac * agree V)).
@@ -127,15 +127,15 @@ Local Existing Instance gmap_view_rel_discrete.
(** [gmap_view] is a notation to give canonical structure search the chance
to infer the right instances (see [auth]). *)
Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
-Definition gmap_viewO (K : Type) `{Countable K} (V : ofeT) : ofeT :=
+Definition gmap_viewO (K : Type) `{Countable K} (V : ofe) : ofe :=
viewO (gmap_view_rel K V).
-Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
+Definition gmap_viewR (K : Type) `{Countable K} (V : ofe) : cmra :=
viewR (gmap_view_rel K V).
-Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+Definition gmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
viewUR (gmap_view_rel K V).
Section definitions.
- Context {K : Type} `{Countable K} {V : ofeT}.
+ Context {K : Type} `{Countable K} {V : ofe}.
Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
â—V{q} m.
@@ -144,7 +144,7 @@ Section definitions.
End definitions.
Section lemmas.
- Context {K : Type} `{Countable K} {V : ofeT}.
+ Context {K : Type} `{Countable K} {V : ofe}.
Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
Global Instance : Params (@gmap_view_auth) 5 := {}.
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index d3773e7d4..2c6d41765 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -98,11 +98,11 @@ End gset_bij_view_rel.
Definition gset_bij A B `{Countable A, Countable B} :=
view (gset_bij_view_rel_raw (A:=A) (B:=B)).
-Definition gset_bijO A B `{Countable A, Countable B} : ofeT :=
+Definition gset_bijO A B `{Countable A, Countable B} : ofe :=
viewO (gset_bij_view_rel (A:=A) (B:=B)).
-Definition gset_bijR A B `{Countable A, Countable B} : cmraT :=
+Definition gset_bijR A B `{Countable A, Countable B} : cmra :=
viewR (gset_bij_view_rel (A:=A) (B:=B)).
-Definition gset_bijUR A B `{Countable A, Countable B} : ucmraT :=
+Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
viewUR (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bij_auth `{Countable A, Countable B}
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index bbfd9d132..8d20e85f5 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -20,9 +20,9 @@ From iris.algebra Require Export auth frac updates local_updates.
From iris.algebra Require Import ufrac proofmode_classes.
From iris.prelude Require Import options.
-Definition ufrac_authR (A : cmraT) : cmraT :=
+Definition ufrac_authR (A : cmra) : cmra :=
authR (optionUR (prodR ufracR A)).
-Definition ufrac_authUR (A : cmraT) : ucmraT :=
+Definition ufrac_authUR (A : cmra) : ucmra :=
authUR (optionUR (prodR ufracR A)).
(** Note in the signature of [ufrac_auth_auth] and [ufrac_auth_frag] we use
@@ -32,9 +32,9 @@ instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
such that the [✓] of the default [fracR] camera is used, and not the [✓] of
the [ufracR] camera. *)
-Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
+Definition ufrac_auth_auth {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
â— (Some (q : ufracR,x)).
-Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
+Definition ufrac_auth_frag {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
â—¯ (Some (q : ufracR,x)).
Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
@@ -46,7 +46,7 @@ Notation "â—U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "â—U{ q }
Notation "â—¯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "â—¯U{ q } a").
Section ufrac_auth.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types a b : A.
Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth A q).
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 1fac28aea..a200489ae 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import updates local_updates big_op.
From iris.prelude Require Import options.
Section ofe.
-Context {A : ofeT}.
+Context {A : ofe}.
Implicit Types l : list A.
Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
@@ -57,7 +57,7 @@ Proof.
- apply _.
- rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
Qed.
-Canonical Structure listO := OfeT (list A) list_ofe_mixin.
+Canonical Structure listO := Ofe (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
@@ -98,32 +98,32 @@ End ofe.
Global Arguments listO : clear implicits.
(** Non-expansiveness of higher-order list functions and big-ops *)
-Global Instance list_fmap_ne {A B : ofeT} (f : A → B) n :
+Global Instance list_fmap_ne {A B : ofe} (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.
-Global Instance list_omap_ne {A B : ofeT} (f : A → option B) n :
+Global Instance list_omap_ne {A B : ofe} (f : A → option B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (omap (M:=list) f).
Proof.
intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
destruct (Hf _ _ Hx); [f_equiv|]; auto.
Qed.
-Global Instance imap_ne {A B : ofeT} (f : nat → A → B) n :
+Global Instance imap_ne {A B : ofe} (f : nat → A → B) n :
(∀ i, Proper (dist n ==> dist n) (f i)) → Proper (dist n ==> dist n) (imap f).
Proof.
intros Hf l1 l2 Hl. revert f Hf.
induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
Qed.
-Global Instance list_bind_ne {A B : ofeT} (f : A → list A) n :
+Global Instance list_bind_ne {A B : ofe} (f : A → list A) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (mbind f).
Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
-Global Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
+Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (M:=list) (A:=A)).
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
-Global Instance zip_with_ne {A B C : ofeT} (f : A → B → C) n :
+Global Instance zip_with_ne {A B C : ofe} (f : A → B → C) n :
Proper (dist n ==> dist n ==> dist n) f →
Proper (dist n ==> dist n ==> dist n) (zip_with f).
Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
-Lemma big_opL_ne_2 `{Monoid M o} {A : ofeT} (f g : nat → A → M) l1 l2 n :
+Lemma big_opL_ne_2 `{Monoid M o} {A : ofe} (f g : nat → A → M) l1 l2 n :
l1 ≡{n}≡ l2 →
(∀ k y1 y2,
l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
@@ -136,7 +136,7 @@ Proof.
Qed.
(** Functor *)
-Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
+Lemma list_fmap_ext_ne {A} {B : ofe} (f g : A → B) (l : list A) n :
(∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
@@ -168,7 +168,7 @@ Qed.
(* CMRA. Only works if [A] has a unit! *)
Section cmra.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types l : list A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
@@ -265,7 +265,7 @@ Section cmra.
[by inversion_clear Heq; inversion_clear Hl..|].
exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Qed.
- Canonical Structure listR := CmraT (list A) list_cmra_mixin.
+ Canonical Structure listR := Cmra (list A) list_cmra_mixin.
Global Instance list_unit : Unit (list A) := [].
Definition list_ucmra_mixin : UcmraMixin (list A).
@@ -275,7 +275,7 @@ Section cmra.
- by intros l.
- by constructor.
Qed.
- Canonical Structure listUR := UcmraT (list A) list_ucmra_mixin.
+ Canonical Structure listUR := Ucmra (list A) list_ucmra_mixin.
Global Instance list_cmra_discrete : CmraDiscrete A → CmraDiscrete listR.
Proof.
@@ -299,11 +299,11 @@ End cmra.
Global Arguments listR : clear implicits.
Global Arguments listUR : clear implicits.
-Global Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
+Global Instance list_singletonM {A : ucmra} : SingletonM nat A (list A) := λ n x,
replicate n ε ++ [x].
Section properties.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types l : list A.
Implicit Types x y z : A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
@@ -515,7 +515,7 @@ Section properties.
End properties.
(** Functor *)
-Global Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A → B)
+Global Instance list_fmap_cmra_morphism {A B : ucmra} (f : A → B)
`{!CmraMorphism f} : CmraMorphism (fmap f : list A → list B).
Proof.
split; try apply _.
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index d8819bf5a..ed932d645 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -2,13 +2,13 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Import options.
(** * Local updates *)
-Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
+Definition local_update {A : cmra} (x y : A * A) := ∀ n mz,
✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
Global Instance: Params (@local_update) 1 := {}.
Infix "~l~>" := local_update (at level 70).
Section updates.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types x y : A.
Global Instance local_update_proper :
@@ -110,7 +110,7 @@ Section updates.
End updates.
Section updates_unital.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types x y : A.
Lemma local_update_unital x y x' y' :
@@ -138,7 +138,7 @@ Section updates_unital.
End updates_unital.
(** * Product *)
-Lemma prod_local_update {A B : cmraT} (x y x' y' : A * B) :
+Lemma prod_local_update {A B : cmra} (x y x' y' : A * B) :
(x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
(x,y) ~l~> (x',y').
Proof.
@@ -148,21 +148,21 @@ Proof.
by destruct mz.
Qed.
-Lemma prod_local_update' {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
+Lemma prod_local_update' {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
(x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') →
((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
Proof. intros. by apply prod_local_update. Qed.
-Lemma prod_local_update_1 {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 : B) :
+Lemma prod_local_update_1 {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 : B) :
(x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
Proof. intros. by apply prod_local_update. Qed.
-Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) :
+Lemma prod_local_update_2 {A B : cmra} (x1 y1 : A) (x2 y2 x2' y2' : B) :
(x2,y2) ~l~> (x2',y2') → ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')).
Proof. intros. by apply prod_local_update. Qed.
(** * Option *)
(* TODO: Investigate whether we can use these in proving the very similar local
updates on finmaps. *)
-Lemma option_local_update {A : cmraT} (x y x' y' : A) :
+Lemma option_local_update {A : cmra} (x y x' y' : A) :
(x, y) ~l~> (x',y') →
(Some x, Some y) ~l~> (Some x', Some y').
Proof.
@@ -172,7 +172,7 @@ Proof.
split; first done. destruct mz as [?|]; constructor; auto.
Qed.
-Lemma alloc_option_local_update {A : cmraT} (x : A) y :
+Lemma alloc_option_local_update {A : cmra} (x : A) y :
✓ x →
(None, y) ~l~> (Some x, Some x).
Proof.
@@ -181,7 +181,7 @@ Proof.
destruct z as [z|]; last done. destruct y; inversion Heq.
Qed.
-Lemma delete_option_local_update {A : cmraT} (x : option A) (y : A) :
+Lemma delete_option_local_update {A : cmra} (x : option A) (y : A) :
Exclusive y → (x, Some y) ~l~> (None, None).
Proof.
move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
diff --git a/iris/algebra/monoid.v b/iris/algebra/monoid.v
index f8a563322..95a23c034 100644
--- a/iris/algebra/monoid.v
+++ b/iris/algebra/monoid.v
@@ -17,7 +17,7 @@ we do not have a canonical structure for setoids, we do not go that way.
Note that we do not declare any of the projections as type class instances. That
is because we only need them in the [big_op] file, and nowhere else. Hence, we
declare these instances locally there to avoid them being used elsewhere. *)
-Class Monoid {M : ofeT} (o : M → M → M) := {
+Class Monoid {M : ofe} (o : M → M → M) := {
monoid_unit : M;
monoid_ne : NonExpansive2 o;
monoid_assoc : Assoc (≡) o;
@@ -33,7 +33,7 @@ Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
commuting with each other. We also consider a [WeakMonoidHomomorphism] which
does not necessarily commute with unit; an example is the [own] connective: we
only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
-Class WeakMonoidHomomorphism {M1 M2 : ofeT}
+Class WeakMonoidHomomorphism {M1 M2 : ofe}
(o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_rel_po : PreOrder R;
@@ -43,7 +43,7 @@ Class WeakMonoidHomomorphism {M1 M2 : ofeT}
monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
}.
-Class MonoidHomomorphism {M1 M2 : ofeT}
+Class MonoidHomomorphism {M1 M2 : ofe}
(o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 R f;
diff --git a/iris/algebra/namespace_map.v b/iris/algebra/namespace_map.v
index 862a60668..eb2ee07d9 100644
--- a/iris/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -28,15 +28,15 @@ Global Instance: Params (@namespace_map_data_proj) 1 := {}.
Global Instance: Params (@namespace_map_token_proj) 1 := {}.
(** TODO: [positives_flatten] violates the namespace abstraction. *)
-Definition namespace_map_data {A : cmraT} (N : namespace) (a : A) : namespace_map A :=
+Definition namespace_map_data {A : cmra} (N : namespace) (a : A) : namespace_map A :=
NamespaceMap {[ positives_flatten N := a ]} ε.
-Definition namespace_map_token {A : cmraT} (E : coPset) : namespace_map A :=
+Definition namespace_map_token {A : cmra} (E : coPset) : namespace_map A :=
NamespaceMap ∅ (CoPset E).
Global Instance: Params (@namespace_map_data) 2 := {}.
(* Ofe *)
Section ofe.
-Context {A : ofeT}.
+Context {A : ofe}.
Implicit Types x y : namespace_map A.
Local Instance namespace_map_equiv : Equiv (namespace_map A) := λ x y,
@@ -62,7 +62,7 @@ Proof.
(λ x, (namespace_map_data_proj x, namespace_map_token_proj x))).
Qed.
Canonical Structure namespace_mapO :=
- OfeT (namespace_map A) namespace_map_ofe_mixin.
+ Ofe (namespace_map A) namespace_map_ofe_mixin.
Global Instance NamespaceMap_discrete a b :
Discrete a → Discrete b → Discrete (NamespaceMap a b).
@@ -76,7 +76,7 @@ Global Arguments namespace_mapO : clear implicits.
(* Camera *)
Section cmra.
-Context {A : cmraT}.
+Context {A : cmra}.
Implicit Types a b : A.
Implicit Types x y : namespace_map A.
@@ -183,7 +183,7 @@ Proof.
by exists (NamespaceMap m1 E1), (NamespaceMap m2 E2).
Qed.
Canonical Structure namespace_mapR :=
- CmraT (namespace_map A) namespace_map_cmra_mixin.
+ Cmra (namespace_map A) namespace_map_cmra_mixin.
Global Instance namespace_map_cmra_discrete :
CmraDiscrete A → CmraDiscrete namespace_mapR.
@@ -202,7 +202,7 @@ Proof.
- do 2 constructor; [apply (core_id_core _)|done].
Qed.
Canonical Structure namespace_mapUR :=
- UcmraT (namespace_map A) namespace_map_ucmra_mixin.
+ Ucmra (namespace_map A) namespace_map_ucmra_mixin.
Global Instance namespace_map_data_core_id N a :
CoreId a → CoreId (namespace_map_data N a).
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 8fb3dd44b..14b02b9df 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -18,7 +18,7 @@ Section nat.
- intros x y. apply Nat.add_comm.
- by exists 0.
Qed.
- Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
+ Canonical Structure natR : cmra := discreteR nat nat_ra_mixin.
Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
@@ -26,7 +26,7 @@ Section nat.
Local Instance nat_unit : Unit nat := 0.
Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
- Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
+ Canonical Structure natUR : ucmra := Ucmra nat nat_ucmra_mixin.
Global Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
@@ -71,14 +71,14 @@ Section max_nat.
- intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
- intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
Qed.
- Canonical Structure max_natR : cmraT := discreteR max_nat max_nat_ra_mixin.
+ Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
Global Instance max_nat_cmra_discrete : CmraDiscrete max_natR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma max_nat_ucmra_mixin : UcmraMixin max_nat.
Proof. split; try apply _ || done. intros [x]. done. Qed.
- Canonical Structure max_natUR : ucmraT := UcmraT max_nat max_nat_ucmra_mixin.
+ Canonical Structure max_natUR : ucmra := Ucmra max_nat max_nat_ucmra_mixin.
Global Instance max_nat_core_id (x : max_nat) : CoreId x.
Proof. by constructor. Qed.
@@ -126,7 +126,7 @@ Section min_nat.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
Qed.
- Canonical Structure min_natR : cmraT := discreteR min_nat min_nat_ra_mixin.
+ Canonical Structure min_natR : cmra := discreteR min_nat min_nat_ra_mixin.
Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
Proof. apply discrete_cmra_discrete. Qed.
@@ -173,7 +173,7 @@ Section positive.
- intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm.
Qed.
- Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
+ Canonical Structure positiveR : cmra := discreteR positive pos_ra_mixin.
Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 9d0de0012..9219e4c43 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -44,14 +44,14 @@ Record OfeMixin A `{Equiv A, Dist A} := {
}.
(** Bundled version *)
-Structure ofeT := OfeT {
+Structure ofe := Ofe {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
-Global Arguments OfeT _ {_ _} _.
-Add Printing Constructor ofeT.
+Global Arguments Ofe _ {_ _} _.
+Add Printing Constructor ofe.
Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
Global Arguments ofe_car : simpl never.
@@ -62,7 +62,7 @@ Global Arguments ofe_mixin : simpl never.
(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
mixin out of it. This makes sure we do not use two different OFE instances in
-different places (see for example the constructors [CmraT] and [UcmraT] in the
+different places (see for example the constructors [Cmra] and [Ucmra] in the
file [cmra.v].)
In order to infer the OFE instance, we use the definition [ofe_mixin_of'] which
@@ -80,13 +80,13 @@ The notation [ofe_mixin_of A] that we define on top of [ofe_mixin_of' A id]
hides the [id] and normalizes the mixin to head normal form. The latter is to
ensure that we do not end up with redundant canonical projections to the mixin,
i.e. them all being of the shape [ofe_mixin_of' A id]. *)
-Definition ofe_mixin_of' A {Ac : ofeT} (f : Ac → A) : OfeMixin Ac := ofe_mixin Ac.
+Definition ofe_mixin_of' A {Ac : ofe} (f : Ac → A) : OfeMixin Ac := ofe_mixin Ac.
Notation ofe_mixin_of A :=
ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
(** Lifting properties from the mixin *)
Section ofe_mixin.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types x y : A.
Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
@@ -99,28 +99,28 @@ End ofe_mixin.
Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
(** Discrete OFEs and discrete OFE elements *)
-Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
+Class Discrete {A : ofe} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
Global Arguments discrete {_} _ {_} _ _.
Global Hint Mode Discrete + ! : typeclass_instances.
Global Instance: Params (@Discrete) 1 := {}.
-Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
+Class OfeDiscrete (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
(** OFEs with a completion *)
-Record chain (A : ofeT) := {
+Record chain (A : ofe) := {
chain_car :> nat → A;
chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
}.
Global Arguments chain_car {_} _ _.
Global Arguments chain_cauchy {_} _ _ _ _.
-Program Definition chain_map {A B : ofeT} (f : A → B)
+Program Definition chain_map {A B : ofe} (f : A → B)
`{!NonExpansive f} (c : chain A) : chain B :=
{| chain_car n := f (c n) |}.
Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Notation Compl A := (chain A%type → A).
-Class Cofe (A : ofeT) := {
+Class Cofe (A : ofe) := {
compl : Compl A;
conv_compl n c : compl c ≡{n}≡ c n;
}.
@@ -131,17 +131,17 @@ Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
compl (chain_map f c) ≡ f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
-Program Definition chain_const {A : ofeT} (a : A) : chain A :=
+Program Definition chain_const {A : ofe} (a : A) : chain A :=
{| chain_car n := a |}.
Next Obligation. by intros A a n i _. Qed.
-Lemma compl_chain_const {A : ofeT} `{!Cofe A} (a : A) :
+Lemma compl_chain_const {A : ofe} `{!Cofe A} (a : A) :
compl (chain_const a) ≡ a.
Proof. apply equiv_dist=>n. by rewrite conv_compl. Qed.
(** General properties *)
Section ofe.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types x y : A.
Global Instance ofe_equivalence : Equivalence ((≡) : relation A).
Proof.
@@ -173,10 +173,10 @@ Section ofe.
type class search during setoid rewriting.
Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
[Proper] built using these lemmas. *)
- Lemma ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
+ Lemma ne_proper {B : ofe} (f : A → B) `{!NonExpansive f} :
Proper ((≡) ==> (≡)) f.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
- Lemma ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
+ Lemma ne_proper_2 {B C : ofe} (f : A → B → C) `{!NonExpansive2 f} :
Proper ((≡) ==> (≡) ==> (≡)) f.
Proof.
unfold Proper, respectful; setoid_rewrite equiv_dist.
@@ -202,31 +202,31 @@ Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x ≡{n}≡ y end.
Global Arguments dist_later _ _ !_ _ _ /.
-Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
+Global Instance dist_later_equivalence (A : ofe) n : Equivalence (@dist_later A _ n).
Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
-Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
+Lemma dist_dist_later {A : ofe} n (x y : A) : dist n x y → dist_later n x y.
Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
-Lemma dist_later_dist {A : ofeT} n (x y : A) : dist_later (S n) x y → dist n x y.
+Lemma dist_later_dist {A : ofe} n (x y : A) : dist_later (S n) x y → dist n x y.
Proof. done. Qed.
(* We don't actually need this lemma (as our tactics deal with this through
other means), but technically speaking, this is the reason why
pre-composing a non-expansive function to a contractive function
preserves contractivity. *)
-Lemma ne_dist_later {A B : ofeT} (f : A → B) :
+Lemma ne_dist_later {A B : ofe} (f : A → B) :
NonExpansive f → ∀ n, Proper (dist_later n ==> dist_later n) f.
Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.
Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
-Global Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
+Global Instance const_contractive {A B : ofe} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
Section contractive.
Local Set Default Proof Using "Type*".
- Context {A B : ofeT} (f : A → B) `{!Contractive f}.
+ Context {A B : ofe} (f : A → B) `{!Contractive f}.
Implicit Types x y : A.
Lemma contractive_0 x y : f x ≡{0}≡ f y.
@@ -308,7 +308,7 @@ Section limit_preserving.
End limit_preserving.
(** Fixpoint *)
-Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
+Program Definition fixpoint_chain {A : ofe} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
intros A ? f ? n.
@@ -525,7 +525,7 @@ Section fixpointAB_ne.
End fixpointAB_ne.
(** Non-expansive function space *)
-Record ofe_mor (A B : ofeT) : Type := OfeMor {
+Record ofe_mor (A B : ofe) : Type := OfeMor {
ofe_mor_car :> A → B;
ofe_mor_ne : NonExpansive ofe_mor_car
}.
@@ -538,7 +538,7 @@ Notation "'λne' x .. y , t" :=
(at level 200, x binder, y binder, right associativity).
Section ofe_mor.
- Context {A B : ofeT}.
+ Context {A B : ofe}.
Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, ofe_mor_ne. Qed.
Local Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
@@ -554,7 +554,7 @@ 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_morO := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
+ Canonical Structure ofe_morO := Ofe (ofe_mor A B) ofe_mor_ofe_mixin.
Program Definition ofe_mor_chain (c : chain ofe_morO)
(x : A) : chain B := {| chain_car n := c n x |}.
@@ -584,13 +584,13 @@ End ofe_mor.
Global Arguments ofe_morO : clear implicits.
Notation "A -n> B" :=
(ofe_morO A B) (at level 99, B at level 200, right associativity).
-Global Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
+Global Instance ofe_mor_inhabited {A B : ofe} `{Inhabited B} :
Inhabited (A -n> B) := populate (λne _, inhabitant).
(** Identity and composition and constant function *)
Definition cid {A} : A -n> A := OfeMor id.
Global Instance: Params (@cid) 1 := {}.
-Definition cconst {A B : ofeT} (x : B) : A -n> B := OfeMor (const x).
+Definition cconst {A B : ofe} (x : B) : A -n> B := OfeMor (const x).
Global Instance: Params (@cconst) 2 := {}.
Definition ccompose {A B C}
@@ -622,7 +622,7 @@ Section unit.
Local Instance unit_dist : Dist unit := λ _ _ _, True.
Definition unit_ofe_mixin : OfeMixin unit.
Proof. by repeat split; try exists 0. Qed.
- Canonical Structure unitO : ofeT := OfeT unit unit_ofe_mixin.
+ Canonical Structure unitO : ofe := Ofe unit unit_ofe_mixin.
Global Program Instance unit_cofe : Cofe unitO := { compl x := () }.
Next Obligation. by repeat split; try exists 0. Qed.
@@ -636,7 +636,7 @@ Section empty.
Local Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
Proof. by repeat split; try exists 0. Qed.
- Canonical Structure Empty_setO : ofeT := OfeT Empty_set Empty_set_ofe_mixin.
+ Canonical Structure Empty_setO : ofe := Ofe Empty_set Empty_set_ofe_mixin.
Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
Next Obligation. by repeat split; try exists 0. Qed.
@@ -647,7 +647,7 @@ End empty.
(** * Product type *)
Section product.
- Context {A B : ofeT}.
+ Context {A B : ofe}.
Local Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
Global Instance pair_ne :
@@ -662,7 +662,7 @@ Section product.
- apply _.
- by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Qed.
- Canonical Structure prodO : ofeT := OfeT (A * B) prod_ofe_mixin.
+ Canonical Structure prodO : ofe := Ofe (A * B) prod_ofe_mixin.
Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
{ compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
@@ -683,7 +683,7 @@ End product.
Global Arguments prodO : clear implicits.
Typeclasses Opaque prod_dist.
-Global Instance prod_map_ne {A A' B B' : ofeT} n :
+Global Instance prod_map_ne {A A' B B' : ofe} 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.
@@ -695,7 +695,7 @@ Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** * COFE → OFE Functors *)
Record oFunctor := OFunctor {
- oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
+ oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofe;
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_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -720,7 +720,7 @@ Global Hint Mode oFunctorContractive ! : typeclass_instances.
(** Not a coercion due to the [Cofe] type class argument, and to avoid
ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
-Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
+Definition oFunctor_apply (F: oFunctor) (A: ofe) `{!Cofe A} : ofe :=
oFunctor_car F A A.
Program Definition oFunctor_oFunctor_compose (F1 F2 : oFunctor)
@@ -758,10 +758,10 @@ Proof.
f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.
-Program Definition constOF (B : ofeT) : oFunctor :=
+Program Definition constOF (B : ofe) : oFunctor :=
{| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
-Coercion constOF : ofeT >-> oFunctor.
+Coercion constOF : ofe >-> oFunctor.
Global Instance constOF_contractive B : oFunctorContractive (constOF B).
Proof. rewrite /oFunctorContractive; apply _. Qed.
@@ -823,7 +823,7 @@ Qed.
(** * Sum type *)
Section sum.
- Context {A B : ofeT}.
+ Context {A B : ofe}.
Local Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
Global Instance inl_ne : NonExpansive (@inl A B) := _.
@@ -840,7 +840,7 @@ Section sum.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
- Canonical Structure sumO : ofeT := OfeT (A + B) sum_ofe_mixin.
+ Canonical Structure sumO : ofe := Ofe (A + B) sum_ofe_mixin.
Program Definition inl_chain (c : chain sumO) (a : A) : chain A :=
{| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
@@ -875,7 +875,7 @@ End sum.
Global Arguments sumO : clear implicits.
Typeclasses Opaque sum_dist.
-Global Instance sum_map_ne {A A' B B' : ofeT} n :
+Global Instance sum_map_ne {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@sum_map A A' B B').
Proof.
@@ -923,10 +923,10 @@ Section discrete_ofe.
- done.
Qed.
- Global Instance discrete_ofe_discrete : OfeDiscrete (OfeT A discrete_ofe_mixin).
+ Global Instance discrete_ofe_discrete : OfeDiscrete (Ofe A discrete_ofe_mixin).
Proof. by intros x y. Qed.
- Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
+ Global Program Instance discrete_cofe : Cofe (Ofe A discrete_ofe_mixin) :=
{ compl c := c 0 }.
Next Obligation.
intros n c. rewrite /compl /=;
@@ -934,11 +934,11 @@ Section discrete_ofe.
Qed.
End discrete_ofe.
-Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
+Notation discreteO A := (Ofe A (discrete_ofe_mixin _)).
(** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
find another one, like [ofe_equivalence], in the case of aliases. See also
https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
-Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL eq_equivalence)).
+Notation leibnizO A := (Ofe A (@discrete_ofe_mixin _ equivL eq_equivalence)).
(** 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
@@ -971,7 +971,7 @@ End prop.
(** * Option type *)
Section option.
- Context {A : ofeT}.
+ Context {A : ofe}.
Local Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
@@ -986,7 +986,7 @@ Section option.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
- Canonical Structure optionO := OfeT (option A) option_ofe_mixin.
+ Canonical Structure optionO := Ofe (option A) option_ofe_mixin.
Program Definition option_chain (c : chain optionO) (x : A) : chain A :=
{| chain_car n := default x (c n) |}.
@@ -1037,17 +1037,17 @@ End option.
Typeclasses Opaque option_dist.
Global Arguments optionO : clear implicits.
-Global Instance option_fmap_ne {A B : ofeT} n:
+Global Instance option_fmap_ne {A B : ofe} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
-Global Instance option_mbind_ne {A B : ofeT} n:
+Global Instance option_mbind_ne {A B : ofe} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind option _ A B).
Proof. destruct 2; simpl; auto. Qed.
-Global Instance option_mjoin_ne {A : ofeT} n:
+Global Instance option_mjoin_ne {A : ofe} n:
Proper (dist n ==> dist n) (@mjoin option _ A).
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
-Lemma fmap_Some_dist {A B : ofeT} (f : A → B) (mx : option A) (y : B) n :
+Lemma fmap_Some_dist {A B : ofe} (f : A → B) (mx : option A) (y : B) n :
f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
Proof.
split; [|by intros (x&->&->)].
@@ -1094,7 +1094,7 @@ Global Arguments later_car {_} _.
Global Instance: Params (@Next) 1 := {}.
Section later.
- Context {A : ofeT}.
+ Context {A : ofe}.
Local Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
Local Instance later_dist : Dist (later A) := λ n x y,
dist_later n (later_car x) (later_car y).
@@ -1111,7 +1111,7 @@ 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 laterO : ofeT := OfeT (later A) later_ofe_mixin.
+ Canonical Structure laterO : ofe := Ofe (later A) later_ofe_mixin.
Program Definition later_chain (c : chain laterO) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
@@ -1135,7 +1135,7 @@ Section later.
(** [f] is contractive iff it can factor into [Next] and a non-expansive
function. *)
- Lemma contractive_alt {B : ofeT} (f : A → B) :
+ Lemma contractive_alt {B : ofe} (f : A → B) :
Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
Proof.
split.
@@ -1148,11 +1148,11 @@ Global Arguments laterO : clear implicits.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
Next (f (later_car x)).
-Global Instance later_map_ne {A B : ofeT} (f : A → B) n :
+Global Instance later_map_ne {A B : ofe} (f : A → B) n :
Proper (dist (pred n) ==> dist (pred n)) f →
Proper (dist n ==> dist n) (later_map f) | 0.
Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
-Global Instance later_map_proper {A B : ofeT} (f : A → B) :
+Global Instance later_map_proper {A B : ofe} (f : A → B) :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡)) (later_map f).
Proof. solve_proper. Qed.
@@ -1161,12 +1161,12 @@ Proof. by destruct x. Qed.
Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
later_map (g ∘ f) x = later_map g (later_map f x).
Proof. by destruct x. Qed.
-Lemma later_map_ext {A B : ofeT} (f g : A → B) x :
+Lemma later_map_ext {A B : ofe} (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 laterO_map {A B} (f : A -n> B) : laterO A -n> laterO B :=
OfeMor (later_map f).
-Global Instance laterO_map_contractive (A B : ofeT) : Contractive (@laterO_map A B).
+Global Instance laterO_map_contractive (A B : ofe) : Contractive (@laterO_map A B).
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
Program Definition laterOF (F : oFunctor) : oFunctor := {|
@@ -1207,10 +1207,10 @@ We make [discrete_fun] a definition so that we can register it as a canonical
structure. We do not bundle the [Proper] proof to keep [discrete_fun] easier to
use. It turns out all the desired OFE and functorial properties do not rely on
this [Proper] instance. *)
-Definition discrete_fun {A} (B : A → ofeT) := ∀ x : A, B x.
+Definition discrete_fun {A} (B : A → ofe) := ∀ x : A, B x.
Section discrete_fun.
- Context {A : Type} {B : A → ofeT}.
+ Context {A : Type} {B : A → ofe}.
Implicit Types f g : discrete_fun B.
Local Instance discrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.
@@ -1226,7 +1226,7 @@ Section discrete_fun.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
- Canonical Structure discrete_funO := OfeT (discrete_fun B) discrete_fun_ofe_mixin.
+ Canonical Structure discrete_funO := Ofe (discrete_fun B) discrete_fun_ofe_mixin.
Program Definition discrete_fun_chain `(c : chain discrete_funO)
(x : A) : chain (B x) := {| chain_car n := c n x |}.
@@ -1253,29 +1253,29 @@ Global Arguments discrete_funO {_} _.
Notation "A -d> B" :=
(@discrete_funO A (λ _, B)) (at level 99, B at level 200, right associativity).
-Definition discrete_fun_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
+Definition discrete_fun_map {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x)
(g : discrete_fun B1) : discrete_fun B2 := λ x, f _ (g x).
-Lemma discrete_fun_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
+Lemma discrete_fun_map_ext {A} {B1 B2 : A → ofe} (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 discrete_fun_map_id {A} {B : A → ofeT} (g : discrete_fun B) :
+Lemma discrete_fun_map_id {A} {B : A → ofe} (g : discrete_fun B) :
discrete_fun_map (λ _, id) g = g.
Proof. done. Qed.
-Lemma discrete_fun_map_compose {A} {B1 B2 B3 : A → ofeT}
+Lemma discrete_fun_map_compose {A} {B1 B2 B3 : A → ofe}
(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.
-Global Instance discrete_fun_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
+Global Instance discrete_fun_map_ne {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x) n :
(∀ x, Proper (dist n ==> dist n) (f x)) →
Proper (dist n ==> dist n) (discrete_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /discrete_fun_map (Hy x). Qed.
-Definition discrete_funO_map {A} {B1 B2 : A → ofeT} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
+Definition discrete_funO_map {A} {B1 B2 : A → ofe} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
discrete_funO B1 -n> discrete_funO B2 := OfeMor (discrete_fun_map f).
-Global Instance discrete_funO_map_ne {A} {B1 B2 : A → ofeT} :
+Global Instance discrete_funO_map_ne {A} {B1 B2 : A → ofe} :
NonExpansive (@discrete_funO_map A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
@@ -1307,7 +1307,7 @@ Proof.
Qed.
(** * Constructing isomorphic OFEs *)
-Lemma iso_ofe_mixin {A : ofeT} {B : Type} `{!Equiv B, !Dist B} (g : B → A)
+Lemma iso_ofe_mixin {A : ofe} {B : Type} `{!Equiv B, !Dist B} (g : B → A)
(g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
Proof.
@@ -1321,7 +1321,7 @@ Proof.
Qed.
Section iso_cofe_subtype.
- Context {A B : ofeT} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
+ Context {A B : ofe} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
@@ -1336,7 +1336,7 @@ Section iso_cofe_subtype.
Qed.
End iso_cofe_subtype.
-Lemma iso_cofe_subtype' {A B : ofeT} `{Cofe A}
+Lemma iso_cofe_subtype' {A B : ofe} `{Cofe A}
(P : A → Prop) (f : ∀ x, P x → B) (g : B → A)
(Pg : ∀ y, P (g y))
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
@@ -1344,14 +1344,14 @@ Lemma iso_cofe_subtype' {A B : ofeT} `{Cofe A}
(Hlimit : LimitPreserving P) : Cofe B.
Proof. apply: (iso_cofe_subtype P f g)=> // c. apply Hlimit=> ?; apply Pg. Qed.
-Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A)
+Definition iso_cofe {A B : ofe} `{Cofe A} (f : A → B) (g : B → A)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
(gf : ∀ x, g (f x) ≡ x) : Cofe B.
Proof. by apply (iso_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.
(** * Sigma type *)
Section sigma.
- Context {A : ofeT} {P : A → Prop}.
+ Context {A : ofe} {P : A → Prop}.
Implicit Types x : sig P.
(* TODO: Find a better place for this Equiv instance. It also
@@ -1370,7 +1370,7 @@ 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 sigO : ofeT := OfeT (sig P) sig_ofe_mixin.
+ Canonical Structure sigO : ofe := Ofe (sig P) sig_ofe_mixin.
Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
@@ -1389,7 +1389,7 @@ equality, while the second component might be any OFE. *)
Section sigT.
Import EqNotations.
- Context {A : Type} {P : A → ofeT}.
+ Context {A : Type} {P : A → ofe}.
Implicit Types x : sigT P.
(**
@@ -1439,7 +1439,7 @@ Section sigT.
exists eq_refl. exact: dist_S.
Qed.
- Canonical Structure sigTO : ofeT := OfeT (sigT P) sigT_ofe_mixin.
+ Canonical Structure sigTO : ofe := Ofe (sigT P) sigT_ofe_mixin.
Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
x1 ≡ x2 ↔
@@ -1546,7 +1546,7 @@ Global Arguments sigTO {_} _.
Section sigTOF.
Context {A : Type}.
- Program Definition sigT_map {P1 P2 : A → ofeT} :
+ Program Definition sigT_map {P1 P2 : A → ofe} :
discrete_funO (λ a, P1 a -n> P2 a) -n>
sigTO P1 -n> sigTO P2 :=
λne f xpx, existT _ (f _ (projT2 xpx)).
@@ -1584,7 +1584,7 @@ Notation "{ x & P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
Notation "{ x : A & P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
(** * Isomorphisms between OFEs *)
-Record ofe_iso (A B : ofeT) := OfeIso {
+Record ofe_iso (A B : ofe) := OfeIso {
ofe_iso_1 : A -n> B;
ofe_iso_2 : B -n> A;
ofe_iso_12 y : ofe_iso_1 (ofe_iso_2 y) ≡ y;
@@ -1597,7 +1597,7 @@ Global Arguments ofe_iso_12 {_ _} _ _.
Global Arguments ofe_iso_21 {_ _} _ _.
Section ofe_iso.
- Context {A B : ofeT}.
+ Context {A B : ofe}.
Local Instance ofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
ofe_iso_1 I1 ≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡ ofe_iso_2 I2.
@@ -1612,7 +1612,7 @@ Section ofe_iso.
Lemma ofe_iso_ofe_mixin : OfeMixin (ofe_iso A B).
Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
- Canonical Structure ofe_isoO : ofeT := OfeT (ofe_iso A B) ofe_iso_ofe_mixin.
+ Canonical Structure ofe_isoO : ofe := Ofe (ofe_iso A B) ofe_iso_ofe_mixin.
Global Instance ofe_iso_cofe `{!Cofe A, !Cofe B} : Cofe ofe_isoO.
Proof.
@@ -1631,7 +1631,7 @@ Global Arguments ofe_isoO : clear implicits.
Program Definition iso_ofe_refl {A} : ofe_iso A A := OfeIso cid cid _ _.
Solve Obligations with done.
-Definition iso_ofe_sym {A B : ofeT} (I : ofe_iso A B) : ofe_iso B A :=
+Definition iso_ofe_sym {A B : ofe} (I : ofe_iso A B) : ofe_iso B A :=
OfeIso (ofe_iso_2 I) (ofe_iso_1 I) (ofe_iso_21 I) (ofe_iso_12 I).
Global Instance iso_ofe_sym_ne {A B} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 0f1ab34e7..41571ba25 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -15,36 +15,36 @@ From iris.prelude Require Import options.
[own γ (q1 + q2)] where [q1] and [q2] are fractions, we actually get
[own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
*)
-Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
+Class IsOp {A : cmra} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
Global Arguments is_op {_} _ _ _ {_}.
Global Hint Mode IsOp + - - - : typeclass_instances.
-Global Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
+Global Instance is_op_op {A : cmra} (a b : A) : IsOp (a â‹… b) a b | 100.
Proof. by rewrite /IsOp. Qed.
-Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
+Class IsOp' {A : cmra} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
Global Hint Mode IsOp' + ! - - : typeclass_instances.
Global Hint Mode IsOp' + - ! ! : typeclass_instances.
-Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
+Class IsOp'LR {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
-Global Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
+Global Instance is_op_lr_op {A : cmra} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
(* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
-Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+Global Instance is_op_pair {A B : cmra} (a b1 b2 : A) (a' b1' b2' : B) :
IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
-Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
+Global Instance is_op_pair_core_id_l {A B : cmra} (a : A) (a' b1' b2' : B) :
CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
+Global Instance is_op_pair_core_id_r {A B : cmra} (a b1 b2 : A) (a' : B) :
CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
+Global Instance is_op_Some {A : cmra} (a : A) b1 b2 :
IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 951451c34..75250e3e5 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -6,18 +6,18 @@ From iris.prelude Require Import options.
make the following hold:
x ~~> P → Some c ~~> Some P
*)
-Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
+Definition cmra_updateP {A : cmra} (x : A) (P : A → Prop) := ∀ n mz,
✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
Global Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).
-Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
+Definition cmra_update {A : cmra} (x y : A) := ∀ n mz,
✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
Infix "~~>" := cmra_update (at level 70).
Global Instance: Params (@cmra_update) 1 := {}.
Section updates.
-Context {A : cmraT}.
+Context {A : cmra}.
Implicit Types x y : A.
Global Instance cmra_updateP_proper :
@@ -129,7 +129,7 @@ End updates.
(** * Transport *)
Section cmra_transport.
- Context {A B : cmraT} (H : A = B).
+ Context {A B : cmra} (H : A = B).
Notation T := (cmra_transport H).
Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
@@ -141,7 +141,7 @@ End cmra_transport.
(** * Isomorphism *)
Section iso_cmra.
- Context {A B : cmraT} (f : A → B) (g : B → A).
+ Context {A B : cmra} (f : A → B) (g : B → A).
Lemma iso_cmra_updateP (P : B → Prop) (Q : A → Prop) y
(gf : ∀ x, g (f x) ≡ x)
@@ -171,7 +171,7 @@ End iso_cmra.
(** * Product *)
Section prod.
- Context {A B : cmraT}.
+ Context {A B : cmra}.
Implicit Types x : A * B.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
@@ -194,7 +194,7 @@ End prod.
(** * Option *)
Section option.
- Context {A : cmraT}.
+ Context {A : cmra}.
Implicit Types x y : A.
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index 471583989..d0811da9c 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -4,14 +4,14 @@ From iris.algebra Require Import list.
From iris.prelude Require Import options.
Section ofe.
- Context {A : ofeT}.
+ Context {A : ofe}.
Local Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
Local Instance vec_dist m : Dist (vec A m) := dist (A:=list A).
Definition vec_ofe_mixin m : OfeMixin (vec A m).
Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
- Canonical Structure vecO m : ofeT := OfeT (vec A m) (vec_ofe_mixin m).
+ Canonical Structure vecO m : ofe := Ofe (vec A m) (vec_ofe_mixin m).
Global Instance list_cofe `{Cofe A} m : Cofe (vecO m).
Proof.
@@ -39,7 +39,7 @@ Global Arguments vecO : clear implicits.
Typeclasses Opaque vec_dist.
Section proper.
- Context {A : ofeT}.
+ Context {A : ofe}.
Global Instance vcons_ne n :
Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A).
@@ -68,22 +68,22 @@ Section proper.
End proper.
(** Functor *)
-Definition vec_map {A B : ofeT} m (f : A → B) : vecO A m → vecO B m :=
+Definition vec_map {A B : ofe} 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 :
+Lemma vec_map_ext_ne {A B : ofe} 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.
Proof.
intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
by rewrite -!vec_to_list_map in Hf.
Qed.
-Global Instance vec_map_ne {A B : ofeT} m f n :
+Global Instance vec_map_ne {A B : ofe} m f n :
Proper (dist n ==> dist n) f →
Proper (dist n ==> dist n) (@vec_map A B m f).
Proof.
intros ? v v' H. eapply list_fmap_ne in H; last done.
by rewrite -!vec_to_list_map in H.
Qed.
-Definition vecO_map {A B : ofeT} m (f : A -n> B) : vecO A m -n> vecO B m :=
+Definition vecO_map {A B : ofe} m (f : A -n> B) : vecO A m -n> vecO B m :=
OfeMor (vec_map m f).
Global Instance vecO_map_ne {A A'} m :
NonExpansive (@vecO_map A A' m).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 2b9b1224c..976034e1e 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -40,7 +40,7 @@ not use type classes for this purpose because cameras themselves are represented
using canonical structures. It has proven fragile for a canonical structure
instance to take a type class as a parameter (in this case, [viewR] would need
to take a class with the view relation laws). *)
-Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
+Structure view_rel (A : ofe) (B : ucmra) := ViewRel {
view_rel_holds :> nat → A → B → Prop;
view_rel_mono n1 n2 a1 a2 b1 b2 :
view_rel_holds n1 a1 b1 →
@@ -101,7 +101,7 @@ Notation "â—¯V a" := (view_frag a) (at level 20).
general version in terms of [â—V] and [â—¯V], and because such a lemma has never
been needed in practice. *)
Section ofe.
- Context {A B : ofeT} (rel : nat → A → B → Prop).
+ Context {A B : ofe} (rel : nat → A → B → Prop).
Implicit Types a : A.
Implicit Types ag : option (frac * agree A).
Implicit Types b : B.
@@ -130,7 +130,7 @@ Section ofe.
Definition view_ofe_mixin : OfeMixin (view rel).
Proof. by apply (iso_ofe_mixin (λ x, (view_auth_proj x, view_frag_proj x))). Qed.
- Canonical Structure viewO := OfeT (view rel) view_ofe_mixin.
+ Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
Global Instance View_discrete ag b :
Discrete ag → Discrete b → Discrete (View ag b).
@@ -235,7 +235,7 @@ Section cmra.
+ intros [a ?]. exists a.
apply view_rel_mono with n a (b1 â‹… b2); eauto using cmra_includedN_l.
Qed.
- Canonical Structure viewR := CmraT (view rel) view_cmra_mixin.
+ Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Global Instance view_auth_discrete q a :
Discrete a → Discrete (ε : B) → Discrete (â—V{q} a : view rel).
@@ -261,7 +261,7 @@ Section cmra.
- by intros x; constructor; rewrite /= left_id.
- do 2 constructor; [done| apply (core_id_core _)].
Qed.
- Canonical Structure viewUR := UcmraT (view rel) view_ucmra_mixin.
+ Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
(** Operation *)
Lemma view_auth_frac_op p1 p2 a : â—V{p1 + p2} a ≡ â—V{p1} a â‹… â—V{p2} a.
@@ -546,7 +546,7 @@ Lemma view_map_compose {A A' A'' B B' B''}
view_map (f2 ∘ f1) (g2 ∘ g1) x
=@{view rel''} view_map f2 g2 (view_map (rel':=rel') f1 g1 x).
Proof. destruct x as [[[]|] ]; by rewrite // /view_map /= agree_map_compose. Qed.
-Lemma view_map_ext {A A' B B' : ofeT}
+Lemma view_map_ext {A A' B B' : ofe}
{rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
(f1 f2 : A → A') (g1 g2 : B → B')
`{!NonExpansive f1, !NonExpansive g1} (x : view rel) :
@@ -556,7 +556,7 @@ Proof.
intros. constructor; simpl; [|by auto].
apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
-Global Instance view_map_ne {A A' B B' : ofeT}
+Global Instance view_map_ne {A A' B B' : ofe}
{rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
(f : A → A') (g : B → B') `{Hf : !NonExpansive f, Hg : !NonExpansive g} :
NonExpansive (view_map (rel':=rel') (rel:=rel) f g).
@@ -566,11 +566,11 @@ Proof.
apply prod_map_ne; [done| |done]. by apply agree_map_ne.
Qed.
-Definition viewO_map {A A' B B' : ofeT}
+Definition viewO_map {A A' B B' : ofe}
{rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
(f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel' :=
OfeMor (view_map f g).
-Lemma viewO_map_ne {A A' B B' : ofeT}
+Lemma viewO_map_ne {A A' B B' : ofe}
{rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop} :
NonExpansive2 (viewO_map (rel:=rel) (rel':=rel')).
Proof.
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 35a40a4ee..ca1adceeb 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -6,18 +6,18 @@ From iris.prelude Require Import options.
(** Internalized properties of our CMRA constructions. *)
Section upred.
-Context {M : ucmraT}.
+Context {M : ucmra}.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by uPred.unseal. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
+Lemma option_validI {A : cmra} (mx : option A) :
✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
Proof. uPred.unseal. by destruct mx. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) :
+Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. by uPred.unseal. Qed.
@@ -25,7 +25,7 @@ Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1âŒ%Qp.
Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
Section gmap_ofe.
- Context `{Countable K} {A : ofeT}.
+ Context `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
@@ -34,7 +34,7 @@ Section gmap_ofe.
End gmap_ofe.
Section gmap_cmra.
- Context `{Countable K} {A : cmraT}.
+ Context `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
@@ -51,7 +51,7 @@ Section gmap_cmra.
End gmap_cmra.
Section list_ofe.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types l : list A.
Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
@@ -59,7 +59,7 @@ Section list_ofe.
End list_ofe.
Section list_cmra.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types l : list A.
Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
@@ -67,7 +67,7 @@ Section list_cmra.
End list_cmra.
Section excl.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
@@ -88,7 +88,7 @@ Section excl.
End excl.
Section agree.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
@@ -106,7 +106,7 @@ Section agree.
End agree.
Section csum_ofe.
- Context {A B : ofeT}.
+ Context {A B : ofe}.
Implicit Types a : A.
Implicit Types b : B.
@@ -124,7 +124,7 @@ Section csum_ofe.
End csum_ofe.
Section csum_cmra.
- Context {A B : cmraT}.
+ Context {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
@@ -203,7 +203,7 @@ Section view.
End view.
Section auth.
- Context {A : ucmraT}.
+ Context {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
@@ -235,7 +235,7 @@ Section auth.
End auth.
Section excl_auth.
- Context {A : ofeT}.
+ Context {A : ofe}.
Implicit Types a b : A.
Lemma excl_auth_agreeI a b : ✓ (â—E a â‹… â—¯E b) ⊢ (a ≡ b).
@@ -247,7 +247,7 @@ Section excl_auth.
End excl_auth.
Section gmap_view.
- Context {K : Type} `{Countable K} {V : ofeT}.
+ Context {K : Type} `{Countable K} {V : ofe}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_validI m k dq v :
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 7cf03eccb..672eaa716 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -10,7 +10,7 @@ Definition uPred_emp {M} : uPred M := uPred_pure True.
Local Existing Instance entails_po.
-Lemma uPred_bi_mixin (M : ucmraT) :
+Lemma uPred_bi_mixin (M : ucmra) :
BiMixin
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
@@ -66,7 +66,7 @@ Proof.
- exact: persistently_and_sep_l_1.
Qed.
-Lemma uPred_bi_later_mixin (M : ucmraT) :
+Lemma uPred_bi_later_mixin (M : ucmra) :
BiLaterMixin
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
@@ -84,7 +84,7 @@ Proof.
- exact: later_false_em.
Qed.
-Canonical Structure uPredI (M : ucmraT) : bi :=
+Canonical Structure uPredI (M : ucmra) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M);
bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M |}.
@@ -170,7 +170,7 @@ Proof. exact: @plainly_exist_1. Qed.
Module uPred.
Section restate.
-Context {M : ucmraT}.
+Context {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -180,7 +180,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
+Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A)
:= uPred_primitive.cmra_valid_ne.
(** Re-exporting primitive lemmas that are not in any interface *)
@@ -201,28 +201,28 @@ Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofeT} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
Proof. exact: uPred_primitive.internal_eq_entails. Qed.
Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■✓ a.
Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. exact: uPred_primitive.discrete_valid. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmraT} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
Proof. exact: uPred_primitive.valid_entails. Qed.
@@ -230,7 +230,7 @@ Proof. exact: uPred_primitive.valid_entails. Qed.
Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ âŒ) → φ.
Proof. apply pure_soundness. Qed.
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index efb542d4c..898511d53 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -60,7 +60,7 @@ Section bupd_alt.
(** We get the usual rule for frame preserving updates if we have an [own]
connective satisfying the following rule w.r.t. interaction with plainly. *)
- Context {M : ucmraT} (own : M → PROP).
+ Context {M : ucmra} (own : M → PROP).
Context (own_updateP_plainly : ∀ x Φ R,
x ~~>: Φ →
own x ∗ (∀ y, ⌜Φ y⌠-∗ own y -∗ ■R) ⊢ ■R).
@@ -95,7 +95,7 @@ Proof.
Qed.
(** The law about the interaction between [uPred_ownM] and plainly holds. *)
-Lemma ownM_updateP {M : ucmraT} x (Φ : M → Prop) (R : uPred M) :
+Lemma ownM_updateP {M : ucmra} x (Φ : M → Prop) (R : uPred M) :
x ~~>: Φ →
uPred_ownM x ∗ (∀ y, ⌜Φ y⌠-∗ uPred_ownM y -∗ ■R) ⊢ ■R.
Proof.
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index ad9a4c01e..b81a3b475 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -9,7 +9,7 @@ Import bi.bi base_logic.bi.uPred.
Module uPred.
Section derived.
-Context {M : ucmraT}.
+Context {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -20,11 +20,11 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(** Propers *)
Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_proper {A : cmraT} :
+Global Instance cmra_valid_proper {A : cmra} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
(** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
@@ -38,9 +38,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■✓ a ⊣⊢ ✓ a.
+Lemma plainly_cmra_valid {A : cmra} (a : A) : ■✓ a ⊣⊢ ✓ a.
Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma intuitionistically_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Proof.
rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
first by rewrite persistently_elim.
@@ -53,7 +53,7 @@ Proof.
Qed.
(** Timeless instances *)
-Global Instance valid_timeless {A : cmraT} `{!CmraDiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
Timeless (✓ a : uPred M)%I.
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
@@ -66,12 +66,12 @@ Proof.
Qed.
(** Plainness *)
-Global Instance cmra_valid_plain {A : cmraT} (a : A) :
+Global Instance cmra_valid_plain {A : cmra} (a : A) :
Plain (✓ a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
(** Persistence *)
-Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
+Global Instance cmra_valid_persistent {A : cmra} (a : A) :
Persistent (✓ a : uPred M)%I.
Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
diff --git a/iris/base_logic/lib/auth.v b/iris/base_logic/lib/auth.v
index 0df2a9fcf..5a3e4a0bd 100644
--- a/iris/base_logic/lib/auth.v
+++ b/iris/base_logic/lib/auth.v
@@ -6,11 +6,11 @@ From iris.prelude Require Import options.
Import uPred.
(* The CMRA we need. *)
-Class authG Σ (A : ucmraT) := AuthG {
+Class authG Σ (A : ucmra) := AuthG {
auth_inG :> inG Σ (authR A);
auth_cmra_discrete :> CmraDiscrete A;
}.
-Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
+Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
Global Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 9ebda575a..87f3719df 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -22,7 +22,7 @@ keep all the other proofs that do not need it conservative. *)
Definition inv_heapN: namespace := nroot .@ "inv_heap".
Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
-Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR
+Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
(optionR $ exclR $ leibnizO V)
(agreeR (V -d> PropO)).
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 7c31a9c77..bccdb42bf 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -116,10 +116,10 @@ Qed.
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
- Parameter iPrePropO : gFunctors → ofeT.
+ Parameter iPrePropO : gFunctors → ofe.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
- Definition iResUR (Σ : gFunctors) : ucmraT :=
+ Definition iResUR (Σ : gFunctors) : ucmra :=
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
@@ -138,10 +138,10 @@ Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Σ : gFunctors) :
solution (uPredOF (iResF Σ)) := solver.result _.
- Definition iPrePropO (Σ : gFunctors) : ofeT := iProp_result Σ.
+ Definition iPrePropO (Σ : gFunctors) : ofe := iProp_result Σ.
Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
- Definition iResUR (Σ : gFunctors) : ucmraT :=
+ Definition iResUR (Σ : gFunctors) : ucmra :=
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index de2d2e1f0..9497fb0b3 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -9,7 +9,7 @@ Import uPred.
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
-Class inG (Σ : gFunctors) (A : cmraT) := InG {
+Class inG (Σ : gFunctors) (A : cmra) := InG {
inG_id : gid Σ;
inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
inG_prf : A = inG_apply (iPropO Σ) _;
@@ -298,7 +298,7 @@ Global Arguments own_update {_ _} [_] _ _ _ _.
Global Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Global Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
-Lemma own_unit A `{i : !inG Σ (A:ucmraT)} γ : ⊢ |==> own γ (ε:A).
+Lemma own_unit A `{i : !inG Σ (A:ucmra)} γ : ⊢ |==> own γ (ε:A).
Proof.
rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, discrete_fun_singleton_update_empty.
@@ -312,7 +312,7 @@ Qed.
(** Big op class instances *)
Section big_op_instances.
- Context `{!inG Σ (A:ucmraT)}.
+ Context `{!inG Σ (A:ucmra)}.
Global Instance own_cmra_sep_homomorphism γ :
WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index dfebe0742..6ababee40 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -7,14 +7,14 @@ Import base_logic.bi.uPred.
(* Setup of the proof mode *)
Section class_instances.
-Context {M : ucmraT}.
+Context {M : ucmra}.
Implicit Types P Q R : uPred M.
Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) (✓ a) (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
-Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
+Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
@FromPure (uPredI M) false (✓ a) (✓ a).
Proof.
rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 9c4ca484c..237149e76 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -104,7 +104,7 @@ This completes the proof.
*)
-Record uPred (M : ucmraT) : Type := UPred {
+Record uPred (M : ucmra) : Type := UPred {
uPred_holds :> nat → M → Prop;
uPred_mono n1 n2 x1 x2 :
@@ -116,7 +116,7 @@ Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 3 := {}.
Section cofe.
- Context {M : ucmraT}.
+ Context {M : ucmra}.
Inductive uPred_equiv' (P Q : uPred M) : Prop :=
{ uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
@@ -137,7 +137,7 @@ 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 uPredO : ofeT := OfeT (uPred M) uPred_ofe_mixin.
+ Canonical Structure uPredO : ofe := Ofe (uPred M) uPred_ofe_mixin.
Program Definition uPred_compl : Compl uPredO := λ c,
{| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
@@ -170,7 +170,7 @@ Proof.
Qed.
(* Equivalence to the definition of uPred in the appendix. *)
-Lemma uPred_alt {M : ucmraT} (P: nat → M → Prop) :
+Lemma uPred_alt {M : ucmra} (P: nat → M → Prop) :
(∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → P n2 x2) ↔
( (∀ x n1 n2, n2 ≤ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ≤ n → P m x1 ↔ P m x2) (* Non-expansive *)
@@ -187,30 +187,30 @@ Proof.
Qed.
(** functor *)
-Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
+Program Definition uPred_map {M1 M2 : ucmra} (f : M2 -n> M1)
`{!CmraMorphism f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
-Global Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
+Global Instance uPred_map_ne {M1 M2 : ucmra} (f : M2 -n> M1)
`{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
intros x1 x2 Hx; split=> n' y ??.
split; apply Hx; auto using cmra_morphism_validN.
Qed.
-Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
+Lemma uPred_map_id {M : ucmra} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+Lemma uPred_map_compose {M1 M2 M3 : ucmra} (f : M1 -n> M2) (g : M2 -n> M3)
`{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
-Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
+Lemma uPred_map_ext {M1 M2 : ucmra} (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 uPredO_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
+Definition uPredO_map {M1 M2 : ucmra} (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)
+Lemma uPredO_map_ne {M1 M2 : ucmra} (f g : M2 -n> M1)
`{!CmraMorphism f, !CmraMorphism g} n :
f ≡{n}≡ g → uPredO_map f ≡{n}≡ uPredO_map g.
Proof.
@@ -304,7 +304,7 @@ Definition uPred_exist := uPred_exist_aux.(unseal).
Global Arguments uPred_exist {M A}.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
-Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
+Program Definition uPred_internal_eq_def {M} {A : ofe} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using dist_le.
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
@@ -371,7 +371,7 @@ Global Arguments uPred_later {M}.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
-Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
+Program Definition uPred_ownM_def {M : ucmra} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn.
@@ -383,7 +383,7 @@ Global Arguments uPred_ownM {M}.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
-Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
+Program Definition uPred_cmra_valid_def {M} {A : cmra} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
@@ -424,7 +424,7 @@ Ltac unseal :=
rewrite !unseal_eqs /=.
Section primitive.
-Context {M : ucmraT}.
+Context {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -514,7 +514,7 @@ Proof.
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
-Lemma internal_eq_ne (A : ofeT) :
+Lemma internal_eq_ne (A : ofe) :
NonExpansive2 (@uPred_internal_eq M A).
Proof.
intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
@@ -559,7 +559,7 @@ Proof.
unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
-Lemma cmra_valid_ne {A : cmraT} :
+Lemma cmra_valid_ne {A : cmra} :
NonExpansive (@uPred_cmra_valid M A).
Proof.
intros n a b Ha; unseal; split=> n' x ? /=.
@@ -760,25 +760,25 @@ Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
Proof. by unseal. Qed.
(** Internal equality *)
-Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a).
+Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
+Lemma internal_eq_rewrite {A : ofe} 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 : discrete_fun B) :
+Lemma fun_ext {A} {B : A → ofe} (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 : sigO P) :
+Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
Proof. by unseal. Qed.
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
Proof. by unseal. Qed.
-Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
+Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
Proof.
unseal=> ?. split=> n x ?. by apply (discrete_iff n).
Qed.
@@ -787,7 +787,7 @@ Qed.
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofeT} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
@@ -862,23 +862,23 @@ Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
-Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■✓ a.
Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmraT} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
@@ -888,7 +888,7 @@ instance of [siProp] soundness in the future. *)
Lemma pure_soundness φ : (True ⊢ ⌜ φ âŒ) → φ.
Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
Proof.
unseal=> -[H]. apply equiv_dist=> n.
by apply (H n ε); eauto using ucmra_unit_validN.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 7663101f0..6edadcd30 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -644,7 +644,7 @@ Section sep_list2.
Proof. rewrite big_sepL2_alt. apply _. Qed.
End sep_list2.
-Lemma big_sepL2_ne_2 {A B : ofeT}
+Lemma big_sepL2_ne_2 {A B : ofe}
(Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
(∀ k y1 y1' y2 y2',
@@ -1499,7 +1499,7 @@ Section map2.
Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
End map2.
-Lemma big_sepM2_ne_2 `{Countable K} (A B : ofeT)
+Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
(Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
(∀ k y1 y1' y2 y2',
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 8dc90eaff..19e0dedc0 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1588,20 +1588,20 @@ Global Instance bi_persistently_sep_entails_homomorphism :
Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
(* Limits *)
-Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_entails {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x).
Proof.
intros HΦ HΨ c Hc. apply entails_eq_True, equiv_dist=>n.
rewrite conv_compl. apply equiv_dist, entails_eq_True. done.
Qed.
-Lemma limit_preserving_equiv {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_equiv {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
Proof.
intros HΦ HΨ. eapply limit_preserving_ext.
{ intros x. symmetry; apply equiv_spec. }
apply limit_preserving_and; by apply limit_preserving_entails.
Qed.
-Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP) :
+Global Instance limit_preserving_Persistent {A:ofe} `{Cofe A} (Φ : A → PROP) :
NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
End derived.
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index fa2c800a7..530a2d0e3 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -63,7 +63,7 @@ Global Hint Mode BiEmbedLater - ! - : typeclass_instances.
Class BiEmbedInternalEq (PROP1 PROP2 : bi)
`{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
- embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
+ embed_internal_eq_1 (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
Global Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
Global Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
@@ -291,7 +291,7 @@ Section embed.
Section internal_eq.
Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
- Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+ Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
Proof.
apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 3638fa926..ce04316c2 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -176,14 +176,14 @@ Structure bi := Bi {
bi_persistently : bi_car → bi_car;
bi_later : bi_car → bi_car;
bi_ofe_mixin : OfeMixin bi_car;
- bi_cofe : Cofe (OfeT bi_car bi_ofe_mixin);
+ bi_cofe : Cofe (Ofe bi_car bi_ofe_mixin);
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently;
bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
-Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
+Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
Global Instance bi_cofe' (PROP : bi) : Cofe PROP.
Proof. apply bi_cofe. Qed.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index da7d84cfd..65dec0d28 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -7,7 +7,7 @@ Internal equality is not part of the [bi] canonical structure as [internal_eq]
can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
Class InternalEq (PROP : bi) :=
- internal_eq : ∀ {A : ofeT}, A → A → PROP.
+ internal_eq : ∀ {A : ofe}, A → A → PROP.
Global Arguments internal_eq {_ _ _} _ _ : simpl never.
Global Hint Mode InternalEq ! : typeclass_instances.
Global Instance: Params (@internal_eq) 3 := {}.
@@ -20,19 +20,19 @@ Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
Record BiInternalEqMixin (PROP : bi) `(InternalEq PROP) := {
- bi_internal_eq_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A);
- bi_internal_eq_mixin_internal_eq_refl {A : ofeT} (P : PROP) (a : A) : P ⊢ a ≡ a;
- bi_internal_eq_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ bi_internal_eq_mixin_internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A);
+ bi_internal_eq_mixin_internal_eq_refl {A : ofe} (P : PROP) (a : A) : P ⊢ a ≡ a;
+ bi_internal_eq_mixin_internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
- bi_internal_eq_mixin_fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ bi_internal_eq_mixin_fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
(∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
- bi_internal_eq_mixin_sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ bi_internal_eq_mixin_sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
`x ≡ `y ⊢@{PROP} x ≡ y;
- bi_internal_eq_mixin_discrete_eq_1 {A : ofeT} (a b : A) :
+ bi_internal_eq_mixin_discrete_eq_1 {A : ofe} (a b : A) :
Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ;
- bi_internal_eq_mixin_later_equivI_1 {A : ofeT} (x y : A) :
+ bi_internal_eq_mixin_later_equivI_1 {A : ofe} (x y : A) :
Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
- bi_internal_eq_mixin_later_equivI_2 {A : ofeT} (x y : A) :
+ bi_internal_eq_mixin_later_equivI_2 {A : ofe} (x y : A) :
▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
}.
@@ -47,28 +47,28 @@ Section internal_eq_laws.
Context `{BiInternalEq PROP}.
Implicit Types P Q : PROP.
- Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A).
+ Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
- Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
+ Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
- Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
- Lemma fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
(∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
- Lemma sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
`x ≡ `y ⊢@{PROP} x ≡ y.
Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
- Lemma discrete_eq_1 {A : ofeT} (a b : A) :
+ Lemma discrete_eq_1 {A : ofe} (a b : A) :
Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ.
Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
- Lemma later_equivI_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
+ Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
- Lemma later_equivI_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
+ Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
End internal_eq_laws.
@@ -81,7 +81,7 @@ Implicit Types P : PROP.
Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
-Global Instance internal_eq_proper (A : ofeT) :
+Global Instance internal_eq_proper (A : ofe) :
Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
(* Equality *)
@@ -90,31 +90,31 @@ Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
Local Hint Resolve internal_eq_refl : core.
Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
-Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
Proof. intros ->. auto. Qed.
-Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P
+Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
{HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
apply impl_elim_l'. by apply internal_eq_rewrite.
Qed.
-Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
+Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
-Lemma f_equivI {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
+Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
x ≡ y ⊢ f x ≡ f y.
Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-Lemma f_equivI_contractive {A B : ofeT} (f : A → B) `{Hf : !Contractive f} x y :
+Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
▷ (x ≡ y) ⊢ f x ≡ f y.
Proof.
rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
by apply f_equivI.
Qed.
-Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
Proof.
apply (anti_symm _).
- apply and_intro; apply f_equivI; apply _.
@@ -122,7 +122,7 @@ Proof.
apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
Qed.
-Lemma sum_equivI {A B : ofeT} (x y : A + B) :
+Lemma sum_equivI {A B : ofe} (x y : A + B) :
x ≡ y ⊣⊢
match x, y with
| inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
@@ -136,7 +136,7 @@ Proof.
destruct x; auto.
- destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
Qed.
-Lemma option_equivI {A : ofeT} (x y : option A) :
+Lemma option_equivI {A : ofe} (x y : option A) :
x ≡ y ⊣⊢ match x, y with
| Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
end.
@@ -150,7 +150,7 @@ Proof.
- destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
Qed.
-Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
Proof.
apply (anti_symm _).
- apply sig_equivI_1.
@@ -160,7 +160,7 @@ Qed.
Section sigT_equivI.
Import EqNotations.
-Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
+Lemma sigT_equivI {A : Type} {P : A → ofe} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
Proof.
@@ -176,13 +176,13 @@ Proof.
Qed.
End sigT_equivI.
-Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof.
apply (anti_symm _); auto using fun_extI.
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_morO_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma ofe_morO_equivI {A B : ofe} (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.
@@ -196,20 +196,20 @@ Proof.
by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
Qed.
-Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
+Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
+Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
Proof.
intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
Qed.
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
+Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
Proof.
apply (anti_symm _), absorbingly_intro.
apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
apply wand_intro_l, internal_eq_refl.
Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
Proof.
apply (anti_symm (⊢)).
{ by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
@@ -217,33 +217,33 @@ Proof.
rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
Qed.
-Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
+Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
Absorbing (PROP:=PROP) (x ≡ y).
Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
+Global Instance internal_eq_persistent {A : ofe} (a b : A) :
Persistent (PROP:=PROP) (a ≡ b).
Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
(* Equality under a later. *)
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
+Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
{HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
Proof.
rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
Qed.
-Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
+Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
{HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
by apply internal_eq_rewrite'.
Qed.
-Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
Proof. apply (f_equivI_contractive _). Qed.
-Global Instance eq_timeless {A : ofeT} (a b : A) :
+Global Instance eq_timeless {A : ofe} (a b : A) :
Discrete a → Timeless (PROP:=PROP) (a ≡ b).
Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
End internal_eq_derived.
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 64a5fc7d7..52d8fb0ee 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -5,34 +5,34 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
-Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
+Class BiMonoPred {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
Global Arguments bi_mono_pred {_ _ _ _} _ _.
Local Existing Instance bi_mono_pred_ne.
-Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
+Definition bi_least_fixpoint {PROP : bi} {A : ofe}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
Global Arguments bi_least_fixpoint : simpl never.
-Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
+Definition bi_greatest_fixpoint {PROP : bi} {A : ofe}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
Global Arguments bi_greatest_fixpoint : simpl never.
-Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n :
+Global Instance least_fixpoint_ne {PROP : bi} {A : ofe} n :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_least_fixpoint.
Proof. solve_proper. Qed.
-Global Instance least_fixpoint_proper {PROP : bi} {A : ofeT} :
+Global Instance least_fixpoint_proper {PROP : bi} {A : ofe} :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
(≡) ==> (≡)) bi_least_fixpoint.
Proof. solve_proper. Qed.
Section least.
- Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+ Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
Proof using Type*.
@@ -74,7 +74,7 @@ Section least.
Qed.
End least.
-Lemma greatest_fixpoint_ne_outer {PROP : bi} {A : ofeT}
+Lemma greatest_fixpoint_ne_outer {PROP : bi} {A : ofe}
(F1 : (A → PROP) → (A → PROP)) (F2 : (A → PROP) → (A → PROP)):
(∀ Φ x n, F1 Φ x ≡{n}≡ F2 Φ x) → ∀ x1 x2 n,
x1 ≡{n}≡ x2 → bi_greatest_fixpoint F1 x1 ≡{n}≡ bi_greatest_fixpoint F2 x2.
@@ -83,17 +83,17 @@ Proof.
do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF.
Qed.
-Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n :
+Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
-Global Instance greatest_fixpoint_proper {PROP : bi} {A : ofeT} :
+Global Instance greatest_fixpoint_proper {PROP : bi} {A : ofe} :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
(≡) ==> (≡)) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
Section greatest.
- Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+ Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Lemma greatest_fixpoint_unfold_1 x :
bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index acab442ba..04a640392 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -8,12 +8,12 @@ From iris.prelude Require Import options.
Set Default Proof Using "Type*".
Definition bi_rtc_pre `{!BiInternalEq PROP}
- {A : ofeT} (R : A → A → PROP)
+ {A : ofe} (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
(<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
- {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+ {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
BiMonoPred (bi_rtc_pre R x).
Proof.
constructor; [|solve_proper].
@@ -25,26 +25,26 @@ Proof.
Qed.
Definition bi_rtc `{!BiInternalEq PROP}
- {A : ofeT} (R : A → A → PROP) (x1 x2 : A) : PROP :=
+ {A : ofe} (R : A → A → PROP) (x1 x2 : A) : PROP :=
bi_least_fixpoint (bi_rtc_pre R x2) x1.
Global Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.
-Global Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP) :
+Global Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP) :
NonExpansive2 (bi_rtc R).
Proof.
intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
solve_proper.
Qed.
-Global Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP)
+Global Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
Section bi_rtc.
Context `{!BiInternalEq PROP}.
- Context {A : ofeT}.
+ Context {A : ofe}.
Context (R : A → A → PROP) `{NonExpansive2 R}.
Lemma bi_rtc_unfold (x1 x2 : A) :
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 68189d8fd..f09bf301b 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -62,7 +62,7 @@ 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 monPredO := OfeT monPred monPred_ofe_mixin.
+ Canonical Structure monPredO := Ofe monPred monPred_ofe_mixin.
Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredO.
Proof.
@@ -826,7 +826,7 @@ Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
Proof. rewrite /bi_except_0. apply _. Qed.
(** Internal equality *)
-Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
+Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofe) (a b : A) : monPred :=
MonPred (λ _, a ≡ b)%I _.
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
Proof. by eexists. Qed.
@@ -862,7 +862,7 @@ Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
@internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
Proof. rewrite monPred_internal_eq_eq. by unseal. Qed.
-Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} i (a b : A) :
+Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} i (a b : A) :
@monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
@@ -875,7 +875,7 @@ Proof.
-f_equivI -sig_equivI !discrete_fun_equivI.
Qed.
-Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
+Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofe} (x y : A) :
@Objective I PROP (x ≡ y).
Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 5549afda8..2a016fb62 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -381,7 +381,7 @@ Proof.
- apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
Qed.
-Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
+Global Instance limit_preserving_Plain {A:ofe} `{Cofe A} (Φ : A → PROP) :
NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
@@ -558,7 +558,7 @@ Qed.
Section internal_eq.
Context `{!BiInternalEq PROP}.
- Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
+ Lemma plainly_internal_eq {A:ofe} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
Proof.
apply (anti_symm (⊢)).
{ by rewrite plainly_elim. }
@@ -566,7 +566,7 @@ Section internal_eq.
rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
Qed.
- Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+ Global Instance internal_eq_plain {A : ofe} (a b : A) :
Plain (PROP:=PROP) (a ≡ b).
Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
End internal_eq.
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index e355153ea..2cbcaf760 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -152,7 +152,7 @@ Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
Global Instance into_internal_eq_embed
`{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
- {A : ofeT} (x y : A) (P : PROP) :
+ {A : ofe} (x y : A) (P : PROP) :
IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index a8cf210e7..879b65fe3 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -8,20 +8,20 @@ Section class_instances_internal_eq.
Context `{!BiInternalEq PROP}.
Implicit Types P Q R : PROP.
-Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+Global Instance from_pure_internal_eq {A : ofe} (a b : A) :
@FromPure PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
-Global Instance into_pure_eq {A : ofeT} (a b : A) :
+Global Instance into_pure_eq {A : ofe} (a b : A) :
Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
-Global Instance from_modal_Next {A : ofeT} (x y : A) :
+Global Instance from_modal_Next {A : ofe} (x y : A) :
FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
(▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
-Global Instance into_laterN_Next {A : ofeT} only_head n n' (x y : A) :
+Global Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
NatCancel n 1 n' 0 →
IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
@@ -29,22 +29,22 @@ Proof.
move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
Qed.
-Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+Global Instance into_internal_eq_internal_eq {A : ofe} (x y : A) :
@IntoInternalEq PROP _ A (x ≡ y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_affinely {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_intuitionistically {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (□ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_absorbingly {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (■P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
End class_instances_internal_eq.
\ No newline at end of file
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index dd4c2a2c6..f4e726483 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -79,7 +79,7 @@ Proof. by exists φ. Qed.
Global Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
-Class IntoInternalEq `{BiInternalEq PROP} {A : ofeT} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{BiInternalEq PROP} {A : ofe} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
Global Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
Global Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index ef474074a..81d01599e 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -799,7 +799,7 @@ Qed.
(** * Rewriting *)
Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy) →
- ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
+ ∀ {A : ofe} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
(Q ⊣⊢ Φ (if d is Left then y else x)) →
NonExpansive Φ →
@@ -814,7 +814,7 @@ Qed.
Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
envs_lookup i Δ = Some (p, Pxy) →
envs_lookup j Δ = Some (q, P) →
- ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
+ ∀ {A : ofe} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
(P ⊣⊢ Φ (if d is Left then y else x)) →
NonExpansive Φ →
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 291e326b7..9b7fba1f7 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -304,7 +304,7 @@ Qed.
Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
!BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
- p P Q (Q' : PROP') {A : ofeT} (a b : A) :
+ p P Q (Q' : PROP') {A : ofe} (a b : A) :
Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 580854139..4170bc9fd 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -476,7 +476,7 @@ Global Instance is_except_0_monPred_at i P :
IsExcept0 P → IsExcept0 (P i).
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
-Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} (x y : A) i :
+Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} (x y : A) i :
MakeMonPredAt i (x ≡ y) (x ≡ y).
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
Global Instance make_monPred_at_except_0 i P ð“ :
@@ -493,7 +493,7 @@ Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ :
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
- {A : ofeT} (x y : A) P i :
+ {A : ofe} (x y : A) P i :
IntoInternalEq P x y → IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index cc94b000c..47a2e322f 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -180,7 +180,7 @@ Section restate.
Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ âŒ) → φ.
Proof. apply pure_soundness. Qed.
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 5fc399342..4725abbcc 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -36,7 +36,7 @@ Section cofe.
by trans (Q i);[apply HP|apply HQ].
- intros n P Q HPQ; split=> i ?; apply HPQ; auto.
Qed.
- Canonical Structure siPropO : ofeT := OfeT siProp siProp_ofe_mixin.
+ Canonical Structure siPropO : ofe := Ofe siProp siProp_ofe_mixin.
Program Definition siProp_compl : Compl siPropO := λ c,
{| siProp_holds n := c n n |}.
@@ -101,7 +101,7 @@ Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
Definition siProp_exist {A} := unseal siProp_exist_aux A.
Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
-Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
+Program Definition siProp_internal_eq_def {A : ofe} (a1 a2 : A) : siProp :=
{| siProp_holds n := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using dist_le.
Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
@@ -195,7 +195,7 @@ Proof.
unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
apply HPQ; lia.
Qed.
-Lemma internal_eq_ne (A : ofeT) : NonExpansive2 (@siProp_internal_eq A).
+Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
Proof.
intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
- by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
@@ -252,19 +252,19 @@ Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ
Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
(** Equality *)
-Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a).
+Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
Proof. unseal; by split=> n ? /=. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → siProp) :
+Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof.
intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
Qed.
-Lemma fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
+Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
Proof. by unseal. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
+Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
Proof. by unseal. Qed.
-Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
+Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
@@ -274,9 +274,9 @@ Proof.
Qed.
(** Later *)
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
Proof. by unseal. Qed.
Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
@@ -299,7 +299,7 @@ Qed.
Lemma pure_soundness φ : (True ⊢ ⌜ φ âŒ) → φ.
Proof. unseal=> -[H]. by apply (H 0). Qed.
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
diff --git a/tests/algebra.v b/tests/algebra.v
index 169f1b573..fa9931e01 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -50,7 +50,7 @@ Section test_prod.
End test_prod.
(** Make sure the [auth]/[gmap_view] notation does not mix up its arguments. *)
-Definition auth_check {A : ucmraT} :
+Definition auth_check {A : ucmra} :
auth A = authO A := eq_refl.
-Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
+Definition gmap_view_check {K : Type} `{Countable K} {V : ofe} :
gmap_view K V = gmap_viewO K V := eq_refl.
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index aa78bae6c..74a366e9c 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -2,7 +2,7 @@
: string
1 goal
- M : ucmraT
+ M : ucmra
A : Type
P, R : iProp
Ψ : A → iProp
@@ -16,7 +16,7 @@
2 goals
- M : ucmraT
+ M : ucmra
A : Type
P, R : iProp
Ψ : A → iProp
@@ -35,7 +35,7 @@ P
1 goal
- M : ucmraT
+ M : ucmra
A : Type
P, R : iProp
Ψ : A → iProp
@@ -50,7 +50,7 @@ P
: string
1 goal
- M : ucmraT
+ M : ucmra
A : Type
P, R : iProp
Ψ : A → iProp
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index d1de99fbb..6c7517d51 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
(** The proofs from Section 3.1 *)
Section demo.
- Context {M : ucmraT}.
+ Context {M : ucmra}.
Notation iProp := (uPred M).
(* The version in Coq *)
@@ -132,7 +132,7 @@ Section M.
Local Arguments op _ _ !_ !_/.
Local Arguments core _ _ !_/.
- Canonical Structure M_O : ofeT := leibnizO M.
+ Canonical Structure M_O : ofe := leibnizO M.
Local Instance M_valid : Valid M := λ x, x ≠Bot.
Local Instance M_op : Op M := λ x y,
@@ -157,7 +157,7 @@ Section M.
repeat (simpl; case_decide); f_equal/=; lia.
- intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
Qed.
- Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
+ Canonical Structure M_R : cmra := discreteR M M_ra_mixin.
Global Instance M_discrete : CmraDiscrete M_R.
Proof. apply discrete_cmra_discrete. Qed.
@@ -167,7 +167,7 @@ Section M.
split; try (done || apply _).
intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
Qed.
- Canonical Structure M_UR : ucmraT := UcmraT M M_ucmra_mixin.
+ Canonical Structure M_UR : ucmra := Ucmra M M_ucmra_mixin.
Global Instance frag_core_id n : CoreId (Frag n).
Proof. by constructor. Qed.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 400147740..589b9fc19 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -68,7 +68,7 @@ Check "test_iStopProof".
Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
-Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofeT} (x y : A) P :
+Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofe} (x y : A) P :
□ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
Proof.
iIntros "#H1 H2".
@@ -478,7 +478,7 @@ Proof.
unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done.
Qed.
-Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofeT} (φ : Prop) (y z : A) :
+Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :
φ → <affine> ⌜y ≡ z⌠-∗ (⌜ φ ⌠∧ ⌜ φ ⌠∧ y ≡ z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
@@ -577,7 +577,7 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
(∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.
-Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofeT} (f : A -n> A) x y :
+Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofe} (f : A -n> A) x y :
Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
Proof. iIntros "H". iNext. by iRewrite "H". Qed.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index 74451f504..aa2e63c33 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -7,7 +7,7 @@ From iris.bi Require Import ascii.
Set Default Proof Using "Type".
Section base_logic_tests.
- Context {M : ucmraT}.
+ Context {M : ucmra}.
Implicit Types P Q R : uPred M.
Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 96b2f643a..700ffde50 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -4,7 +4,7 @@ From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
Section base_logic_tests.
- Context {M : ucmraT}.
+ Context {M : ucmra}.
Implicit Types P Q R : uPred M.
(* Test scopes for bupd *)
--
GitLab