Commit 7975f872 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove the requirement that the unit of a CMRA is timeless.

This requirement was useful in Iris 2.0: in order to ensure that ownership of
the physical state was timeless, we required the ghost CMRA to have a timeless
unit. To avoid having additional type class parameters, or having to extend the
algebraic hierarchy, we required the units of any CMRA to be timeless.

In Iris 3.0, this issue no longer applies: ownership of the physical state is
ghost ownership in the global CMRA, whose unit is always timeless.

Thanks to Jeehoon Kang for spotting this unnecessary requirement.
parent 558377ec
Pipeline #2614 passed with stage
in 8 minutes and 53 seconds
......@@ -156,7 +156,6 @@ Proof.
split; simpl.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure authUR :=
......
......@@ -153,7 +153,6 @@ Arguments core' _ _ _ /.
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_unit_valid : ;
mixin_ucmra_unit_left_id : LeftId () ();
mixin_ucmra_unit_timeless : Timeless ;
mixin_ucmra_pcore_unit : pcore Some
}.
......@@ -201,8 +200,6 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_left_id : LeftId () (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_timeless : Timeless ( : A).
Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
Lemma ucmra_pcore_unit : pcore (:A) Some .
Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
......@@ -922,7 +919,6 @@ Section prod_unit.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (timeless _).
- rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
Canonical Structure prodUR :=
......@@ -1063,7 +1059,7 @@ Section option.
Instance option_empty : Empty (option A) := None.
Lemma option_ucmra_mixin : UCMRAMixin optionR.
Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
Proof. split. done. by intros []. done. Qed.
Canonical Structure optionUR :=
UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
......
......@@ -62,7 +62,7 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
Instance gmap_empty_timeless : Timeless ( : gmap K A).
Global Instance gmap_empty_timeless : Timeless ( : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
......@@ -173,7 +173,6 @@ Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply gmap_empty_timeless.
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR :=
......
......@@ -135,12 +135,15 @@ Section iprod_cmra.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- intros f Hf x. by apply: timeless.
- constructor=> x. apply persistent_core, _.
Qed.
Canonical Structure iprodUR :=
UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
Global Instance iprod_empty_timeless :
( i, Timeless ( : B i)) Timeless ( : iprod B).
Proof. intros ? f Hf x. by apply: timeless. Qed.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : g1 g2 ( i, g1 i g2 i : uPred M).
Proof. by uPred.unseal. Qed.
......@@ -196,7 +199,8 @@ Section iprod_singleton.
Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
Global Instance iprod_singleton_timeless x (y : B x) :
Timeless y Timeless (iprod_singleton x y) := _.
( i, Timeless ( : B i)) Timeless y Timeless (iprod_singleton x y).
Proof. apply _. Qed.
Lemma iprod_singleton_validN n x (y : B x) : {n} iprod_singleton x y {n} y.
Proof.
......
......@@ -210,7 +210,6 @@ Section cmra.
split.
- constructor.
- by intros l.
- by inversion_clear 1.
- by constructor.
Qed.
Canonical Structure listUR :=
......
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