From 7975f8726b1aefbfef80a18aa9ad32690903a773 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 20 Aug 2016 21:30:01 +0200
Subject: [PATCH] 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.
---
 algebra/auth.v  | 1 -
 algebra/cmra.v  | 6 +-----
 algebra/gmap.v  | 3 +--
 algebra/iprod.v | 8 ++++++--
 algebra/list.v  | 1 -
 5 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index 26dbe5652..7d04ae801 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -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 :=
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 642a4dc62..8d6f666a8 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -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.
 
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 55a18a326..8d2fe2b1a 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -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 :=
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 782b9df96..181e5d80d 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -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.
diff --git a/algebra/list.v b/algebra/list.v
index 38fc3a495..373ea5057 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -210,7 +210,6 @@ Section cmra.
     split.
     - constructor.
     - by intros l.
-    - by inversion_clear 1.
     - by constructor.
   Qed.
   Canonical Structure listUR :=
-- 
GitLab