From f5f9e7ff04e5b623288c0d339fc381edd453273e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2016 09:15:09 +0100
Subject: [PATCH] Timelessness of ownership.

---
 iris/ownership.v | 7 +++++++
 iris/parameter.v | 4 +++-
 iris/resources.v | 2 ++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/iris/ownership.v b/iris/ownership.v
index 65813e25c..d439589c7 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -9,9 +9,12 @@ Instance: Params (@inv) 2.
 Instance: Params (@ownP) 1.
 Instance: Params (@ownG) 1.
 
+Typeclasses Opaque inv ownG ownP.
+
 Section ownership.
 Context {Σ : iParam}.
 Implicit Types r : res' Σ.
+Implicit Types σ : istate Σ.
 Implicit Types P : iProp Σ.
 Implicit Types m : icmra' Σ.
 
@@ -38,6 +41,8 @@ Proof.
   rewrite /ownP -uPred.own_op Res_op.
   by apply uPred.own_invalid; intros (_&?&_).
 Qed.
+Global Instance ownP_timeless σ : TimelessP (ownP σ).
+Proof. rewrite /ownP; apply _. Qed.
 
 (* ghost state *)
 Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
@@ -51,6 +56,8 @@ Proof.
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
+Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
+Proof. rewrite /ownG; apply _. Qed.
 
 (* inversion lemmas *)
 Lemma inv_spec r n i P :
diff --git a/iris/parameter.v b/iris/parameter.v
index 671bdbab7..c3973232f 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -8,6 +8,7 @@ Record iParam := IParam {
   ilanguage : Language iexpr ival istate;
   icmra_empty A : Empty (icmra A);
   icmra_empty_spec A : RAIdentity (icmra A);
+  icmra_empty_timeless A : Timeless (∅ : icmra A);
   icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
   icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
   icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x ≡ x;
@@ -16,7 +17,8 @@ Record iParam := IParam {
   icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
 }.
 Existing Instances ilanguage.
-Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono.
+Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
+Existing Instances icmra_map_ne icmra_map_mono.
 
 Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
   (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
diff --git a/iris/resources.v b/iris/resources.v
index 725d36f32..73996b11c 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -161,6 +161,8 @@ Lemma lookup_wld_op_r n r1 r2 i P :
 Proof.
   rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
 Qed.
+Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
+Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
 End res.
 Arguments resRA : clear implicits.
 
-- 
GitLab