From 9fd1f58e6cfad9b0ba1eecc36f05645195155f57 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Dec 2015 15:35:02 +0100
Subject: [PATCH] More timeless stuff.

Also introduce a notion for valid to be timeless.
---
 iris/auth.v      | 12 +++++++++++-
 iris/cmra.v      | 25 +++++++++++++++++++++++--
 iris/cmra_maps.v | 40 +++++++++++++++++++++++++++++++++++++---
 iris/excl.v      |  9 +++++++++
 iris/logic.v     | 17 ++++++++++++-----
 5 files changed, 92 insertions(+), 11 deletions(-)

diff --git a/iris/auth.v b/iris/auth.v
index cc51e16ff..d29b6744a 100644
--- a/iris/auth.v
+++ b/iris/auth.v
@@ -25,7 +25,6 @@ Proof. by destruct 1. Qed.
 
 Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
   Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
-
 Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
 Proof.
   split.
@@ -40,6 +39,9 @@ Proof.
   * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
     apply (conv_compl (chain_map own c) n).
 Qed.
+Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) :
+  Timeless x → Timeless y → Timeless (Auth x y).
+Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed.
 
 (* CMRA *)
 Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
@@ -122,6 +124,14 @@ Proof.
   split; [apply (ra_empty_valid (A:=A))|].
   by intros x; constructor; simpl; rewrite (left_id _ _).
 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) :
+  ValidTimeless x → ValidTimeless (● x).
+Proof.
+  by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
+Qed.
 Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
 
diff --git a/iris/cmra.v b/iris/cmra.v
index 8f941eb75..73b49da8b 100644
--- a/iris/cmra.v
+++ b/iris/cmra.v
@@ -83,6 +83,11 @@ Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n,
 Infix "⇝" := cmra_update (at level 70).
 Instance: Params (@cmra_update) 3.
 
+(** Timeless elements *)
+Class ValidTimeless `{Valid A, ValidN A} (x : A) :=
+  valid_timeless : validN 1 x → valid x.
+Arguments valid_timeless {_ _ _} _ {_} _.
+
 (** Properties **)
 Section cmra.
 Context `{cmra : CMRA A}.
@@ -122,12 +127,23 @@ Proof.
 Qed.
 Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
 Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
+
+(* Timeless *)
+Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
+  Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
+Proof.
+  intros ?? [x' ?].
+  destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
+  by exists z'; rewrite Hy, (timeless x z) by done.
+Qed.
+Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y.
+Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
 Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
-  ✓{1} (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
+  ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
   destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
-  { by rewrite <-?Hz. }
+  { by rewrite <-?Hz; apply cmra_valid_validN. }
   by rewrite Hz', (timeless x1 y1), (timeless x2 y2).
 Qed.
 
@@ -223,6 +239,8 @@ Section discrete.
     intros [|n] x y1 y2 ??; [|by exists (y1,y2)].
     by exists (x,unit x); simpl; rewrite ra_unit_r.
   Qed.
+  Global Instance discrete_timeless (x : A) : ValidTimeless x.
+  Proof. by intros ?. Qed.
   Definition discreteRA : cmraT := CMRAT A.
   Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ⇝: P.
@@ -291,6 +309,9 @@ Proof.
   destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
   by exists ((z1.1,z2.1),(z1.2,z2.2)).
 Qed.
+Instance pair_timeless `{Valid A, ValidN A, Valid B, ValidN B} (x : A) (y : B) :
+  ValidTimeless x → ValidTimeless y → ValidTimeless (x,y).
+Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
 Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B).
 Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'}
   (f : A → A') (g : B → B') `{!CMRAMonotone f, !CMRAMonotone g} :
diff --git a/iris/cmra_maps.v b/iris/cmra_maps.v
index 808772146..d484a19aa 100644
--- a/iris/cmra_maps.v
+++ b/iris/cmra_maps.v
@@ -10,6 +10,17 @@ Instance option_unit `{Unit A} : Unit (option A) := fmap unit.
 Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus `{Minus A} : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
+Lemma option_included `{CMRA A} mx my :
+  mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
+Proof.
+  split.
+  * intros [mz Hmz]; destruct mx as [x|]; [right|by left].
+    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
+    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
+      setoid_subst; eauto using ra_included_l.
+  * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
+    by exists (Some z); constructor.
+Qed.
 Lemma option_includedN `{CMRA A} n mx my :
   mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
 Proof.
@@ -17,9 +28,8 @@ Proof.
   * intros [mz Hmz]; destruct n as [|n]; [by left|right].
     destruct mx as [x|]; [right|by left].
     destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
-    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto.
-    + by exists z.
-    + by cofe_subst.
+    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
+      cofe_subst; auto using cmra_included_l.
   * intros [->|[->|(x&y&->&->&z&Hz)]];
       try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
@@ -65,6 +75,11 @@ Proof.
   * by exists (None,Some x); inversion Hx'; repeat constructor.
   * exists (None,None); repeat constructor.
 Qed.
+Instance None_valid_timeless `{Valid A, ValidN A} : ValidTimeless (@None A).
+Proof. done. Qed.
+Instance Some_valid_timeless `{Valid A, ValidN A} x :
+  ValidTimeless x → ValidTimeless (Some x).
+Proof. by intros ? y; apply (valid_timeless x). Qed.
 Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
   `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B).
 Proof.
@@ -154,6 +169,25 @@ Section map.
       pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
       by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
   Qed.
+  Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
+    ValidTimeless (∅ : M A).
+  Proof. by intros ??; rewrite lookup_empty. Qed.
+  Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x:
+    ValidTimeless x → ValidTimeless m → m !! i = None →
+    ValidTimeless (<[i:=x]>m).
+  Proof.
+    intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality.
+    { specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). }
+    generalize j; clear dependent j; rapply (valid_timeless m).
+    intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
+    by specialize (Hm j); simplify_map_equality.
+  Qed.
+  Global Instance map_ra_singleton_timeless `{Valid A, ValidN A} (i : K) x :
+    ValidTimeless x → ValidTimeless ({[ i, x ]} : M A).
+  Proof.
+    intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
+    by rewrite lookup_empty.
+  Qed.
   Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
   Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
     `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B).
diff --git a/iris/excl.v b/iris/excl.v
index 05bb89ed0..53c63b150 100644
--- a/iris/excl.v
+++ b/iris/excl.v
@@ -61,6 +61,13 @@ Proof.
     feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
     destruct (c 1); simplify_equality'.
 Qed.
+Instance Excl_timeless `{Equiv A, Dist A} (x : excl A) :
+  Timeless x → Timeless (Excl x).
+Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
+Instance ExclUnit_timeless `{Equiv A, Dist A} : Timeless (@ExclUnit A).
+Proof. by inversion_clear 1; constructor. Qed.
+Instance ExclBot_timeless `{Equiv A, Dist A} : Timeless (@ExclBot A).
+Proof. by inversion_clear 1; constructor. Qed.
 
 (* CMRA *)
 Instance excl_valid {A} : Valid (excl A) := λ x,
@@ -112,6 +119,8 @@ Proof.
     | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
     end; destruct y1, y2; inversion_clear Hx; repeat constructor.
 Qed.
+Instance excl_valid_timeless {A} (x : excl A) : ValidTimeless x.
+Proof. by destruct x; intros ?. Qed.
 
 (* Updates *)
 Lemma excl_update {A} (x : A) y : ✓ y → Excl x ⇝ y.
diff --git a/iris/logic.v b/iris/logic.v
index 75db56336..fa24ea604 100644
--- a/iris/logic.v
+++ b/iris/logic.v
@@ -692,6 +692,14 @@ Lemma uPred_own_valid (a : M) : uPred_own a ⊆ (✓ a)%I.
 Proof.
   intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l.
 Qed.
+Lemma uPred_valid_intro (a : M) : ✓ a → True%I ⊆ (✓ a)%I.
+Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
+Lemma uPred_valid_elim_timess (a : M) :
+  ValidTimeless a → ¬ ✓ a → (✓ a)%I ⊆ False%I.
+Proof.
+  intros ? Hvalid x [|n] ??; [done|apply Hvalid].
+  apply (valid_timeless _), cmra_valid_le with (S n); auto with lia.
+Qed.
 
 (* Timeless *)
 Global Instance uPred_const_timeless (P : Prop) : TimelessP (@uPred_const M P).
@@ -733,11 +741,10 @@ Proof. intros ? x n ??; simpl; apply timelessP; auto using cmra_unit_valid. Qed.
 Global Instance uPred_eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M).
 Proof. by intros ? x n ??; apply equiv_dist, timeless. Qed.
-Global Instance uPred_own_timeless (a : M) :
-  Timeless a → TimelessP (uPred_own a).
+
+(** Timeless elements *)
+Global Instance uPred_own_timeless (a: M): Timeless a → TimelessP (uPred_own a).
 Proof.
-  intros ? x n ? [a' ?].
-  destruct (cmra_extend_op 1 x a a') as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
-  by exists b'; rewrite Hx, (timeless a b) by done.
+  by intros ? x n ??; apply cmra_included_includedN, cmra_timeless_included_l.
 Qed.
 End logic.
-- 
GitLab