Commit 785b2175 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename RAEmpty -> RAIdentity.

parent 07f5e2fe
......@@ -119,7 +119,7 @@ Proof.
as (z2&?&?&?); auto using own_validN.
by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
Qed.
Instance auth_ra_empty `{CMRA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
Instance auth_ra_empty `{CMRA A, Empty A, !RAIdentity A} : RAIdentity (auth A).
Proof.
split; [apply (ra_empty_valid (A:=A))|].
by intros x; constructor; simpl; rewrite (left_id _ _).
......@@ -127,7 +127,7 @@ Qed.
Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
ValidTimeless x ValidTimeless ( x).
Proof. by intros ??; apply (valid_timeless x). Qed.
Instance auth_valid_timeless `{CMRA A, Empty A, !RAEmpty A} (x : A) :
Instance auth_valid_timeless `{CMRA A, Empty A, !RAIdentity A} (x : A) :
ValidTimeless x ValidTimeless ( x).
Proof.
by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
......
......@@ -300,7 +300,7 @@ Proof.
* intros x y n; rewrite prod_includedN; intros [??].
by split; apply cmra_op_minus.
Qed.
Instance prod_ra_empty `{RAEmpty A, RAEmpty B} : RAEmpty (A * B).
Instance prod_ra_empty `{RAIdentity A, RAIdentity B} : RAIdentity (A * B).
Proof.
repeat split; simpl; repeat apply ra_empty_valid; repeat apply (left_id _ _).
Qed.
......
......@@ -108,7 +108,7 @@ Proof.
* by intros n [?| |] [?| |].
* by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Qed.
Instance excl_empty_ra `{Cofe A} : RAEmpty (excl A).
Instance excl_empty_ra `{Cofe A} : RAIdentity (excl A).
Proof. split. done. by intros []. Qed.
Instance excl_extend `{Cofe A} : CMRAExtend (excl A).
Proof.
......
......@@ -131,7 +131,7 @@ Proof.
* intros x y n; rewrite map_includedN_spec; intros ? i.
by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
Qed.
Global Instance map_ra_empty `{RA A} : RAEmpty (M A).
Global Instance map_ra_empty `{RA A} : RAIdentity (M A).
Proof.
split.
* by intros ?; rewrite lookup_empty.
......
......@@ -354,7 +354,7 @@ Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
Proof.
intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
Lemma eq_equiv `{Empty M, !RAEmpty M} {A : cofeT} (a b : A) :
Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
True%I (a b : uPred M)%I a b.
Proof.
intros Hab; apply equiv_dist; intros n; apply Hab with .
......@@ -673,7 +673,7 @@ Proof.
rewrite <-(ra_unit_idempotent a), Hx.
apply cmra_unit_preserving, cmra_included_l.
Qed.
Lemma own_empty `{Empty M, !RAEmpty M} : True%I uPred_own .
Lemma own_empty `{Empty M, !RAIdentity M} : True%I uPred_own .
Proof. intros x [|n] ??; [done|]. by exists x; rewrite (left_id _ _). Qed.
Lemma own_valid (a : M) : uPred_own a ( a)%I.
Proof.
......
......@@ -38,7 +38,7 @@ Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
ra_valid_op_l x y : (x y) x;
ra_op_minus x y : x y x y x y
}.
Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
Class RAIdentity A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
ra_empty_valid : ;
ra_empty_l :> LeftId () ()
}.
......@@ -115,7 +115,7 @@ Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
(** ** RAs with empty element *)
Context `{Empty A, !RAEmpty A}.
Context `{Empty A, !RAIdentity A}.
Global Instance ra_empty_r : RightId () ().
Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment