From 9c600c8b1ab7f6176d8bc52ee10b6f943ba1afb7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 00:05:11 +0200
Subject: [PATCH] =?UTF-8?q?Define=20uPred=5Fnow=5FTrue=20P=20:=3D=20?=
 =?UTF-8?q?=E2=96=B7=20False=20=E2=88=A8=20P.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Prove some properties about it, and define timeless in terms of it,
and factor this notion out of raw view shifts.
---
 algebra/upred.v             | 108 ++++++++++++++++++++++--------------
 proofmode/class_instances.v |  15 +++++
 2 files changed, 82 insertions(+), 41 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 643e5df77..fe2debbb7 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -266,7 +266,7 @@ Definition uPred_valid_eq :
 
 Program Definition uPred_rvs_def {M} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
-      0 < k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
+      k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
 Next Obligation.
   intros M Q n x1 x2 HQ [x3 Hx] k yf Hk.
   rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
@@ -335,7 +335,12 @@ Notation "â–·^ n P" := (uPred_laterN n P)
   (at level 20, n at level 9, right associativity,
    format "â–·^ n  P") : uPred_scope.
 
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
+Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P.
+Notation "â—‡ P" := (uPred_now_True P)
+  (at level 20, right associativity) : uPred_scope.
+Instance: Params (@uPred_now_True) 1.
+
+Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
 
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
@@ -1118,6 +1123,47 @@ Qed.
 Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
 
+(* True now *)
+Global Instance now_True_ne n : Proper (dist n ==> dist n) (@uPred_now_True M).
+Proof. solve_proper. Qed.
+Global Instance now_True_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_now_True M).
+Proof. solve_proper. Qed.
+Global Instance now_True_mono' : Proper ((⊢) ==> (⊢)) (@uPred_now_True M).
+Proof. solve_proper. Qed.
+Global Instance now_True_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_now_True M).
+Proof. solve_proper. Qed.
+
+Lemma now_True_intro P : P ⊢ ◇ P.
+Proof. rewrite /uPred_now_True; auto. Qed.
+Lemma now_True_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
+Proof. by intros ->. Qed.
+Lemma now_True_idemp P : ◇ ◇ P ⊢ ◇ P.
+Proof. rewrite /uPred_now_True; auto. Qed.
+Lemma now_True_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
+Proof. rewrite /uPred_now_True. apply (anti_symm _); auto. Qed.
+Lemma now_True_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
+Proof. by rewrite /uPred_now_True or_and_l. Qed.
+Lemma now_True_sep P Q : ◇ (P ★ Q) ⊣⊢ ◇ P ★ ◇ Q.
+Proof.
+  rewrite /uPred_now_True. apply (anti_symm _).
+  - apply or_elim; last by auto.
+    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
+  - rewrite sep_or_r sep_elim_l sep_or_l; auto.
+Qed.
+Lemma now_True_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
+Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
+Lemma now_True_exist {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
+Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
+Lemma now_True_later P : ◇ ▷ P ⊢ ▷ P.
+Proof. by rewrite /uPred_now_True -later_or False_or. Qed.
+Lemma now_True_always P : ◇ □ P ⊣⊢ □ ◇ P.
+Proof. by rewrite /uPred_now_True always_or always_later always_pure. Qed.
+Lemma now_True_frame_l P Q : P ★ ◇ Q ⊢ ◇ (P ★ Q).
+Proof. by rewrite {1}(now_True_intro P) now_True_sep. Qed.
+Lemma now_True_frame_r P Q : ◇ P ★ Q ⊢ ◇ (P ★ Q).
+Proof. by rewrite {1}(now_True_intro Q) now_True_sep. Qed.
+
 (* Own *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2.
@@ -1159,17 +1205,6 @@ Proof. by intros; rewrite ownM_valid valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 
-(* Equivalent definition of timeless in the model *)
-Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
-Proof.
-  split.
-  - intros HP n x ??; induction n as [|n]; auto.
-    move: HP; rewrite /TimelessP; unseal=> /uPred_in_entails /(_ (S n) x).
-    by destruct 1; auto using cmra_validN_S.
-  - move=> HP; rewrite /TimelessP; unseal; split=> -[|n] x /=; auto; left.
-    apply HP, uPred_closed with n; eauto using cmra_validN_le.
-Qed.
-
 (* Viewshifts *)
 Lemma rvs_intro P : P =r=> P.
 Proof.
@@ -1182,13 +1217,6 @@ Proof.
   destruct (HP k yf) as (x'&?&?); eauto.
   exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
 Qed.
-Lemma rvs_timeless P : TimelessP P → ▷ P =r=> P.
-Proof.
-  unseal. rewrite timelessP_spec=> HP.
-  split=> -[|n] x ? HP' k yf ??; first lia.
-  exists x; split; first done.
-  apply HP, uPred_closed with n; eauto using cmra_validN_le.
-Qed.
 Lemma rvs_trans P : (|=r=> |=r=> P) =r=> P.
 Proof. unseal; split; naive_solver. Qed.
 Lemma rvs_frame_r P R : (|=r=> P) ★ R =r=> P ★ R.
@@ -1203,17 +1231,12 @@ Qed.
 Lemma rvs_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x =r=> ∃ y, ■ Φ y ∧ uPred_ownM y.
 Proof.
-  unseal=> Hup; split=> -[|n] x2 ? [x3 Hx] [|k] yf ??; try lia.
-  destruct (Hup (S k) (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
+  unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
+  destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
   { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma rvs_later_pure φ : (|=r=> ▷ ■ φ) ⊢ ▷ ■ φ.
-Proof.
-  unseal; split=> -[|n] x ? Hvs; simpl in *; first done.
-  by destruct (Hvs (S n) (core x)) as (x'&?&?); [omega|by rewrite cmra_core_r|].
-Qed.
 
 (** * Derived rules *)
 Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).
@@ -1265,6 +1288,19 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. uPred.unseal. by destruct mx. Qed.
 
+(* Equivalent definition of timeless in the model *)
+Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
+Proof.
+  split.
+  - intros HP n x ??; induction n as [|n]; auto.
+    move: HP; rewrite /TimelessP /uPred_now_True /=.
+    unseal=> /uPred_in_entails /(_ (S n) x) /=.
+    by destruct 1; auto using cmra_validN_S.
+  - move=> HP; rewrite /TimelessP /uPred_now_True /=.
+    unseal; split=> -[|n] x /=; auto.
+    right. apply HP, uPred_closed with n; eauto using cmra_validN_le.
+Qed.
+
 (* Timeless instances *)
 Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof. by apply timelessP_spec; unseal => -[|n] x. Qed.
@@ -1274,23 +1310,16 @@ Proof.
   apply timelessP_spec; unseal=> n x /=. by rewrite -!cmra_discrete_valid_iff.
 Qed.
 Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
-Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
+Proof. intros; rewrite /TimelessP now_True_and later_and; auto. Qed.
 Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
-Proof.
-  intros; rewrite /TimelessP later_or (timelessP _) (timelessP Q); eauto 10.
-Qed.
+Proof. intros; rewrite /TimelessP now_True_or later_or; auto. Qed.
 Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
 Proof.
   rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto.
   apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
 Qed.
 Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
-Proof.
-  intros; rewrite /TimelessP later_sep (timelessP P) (timelessP Q).
-  apply wand_elim_l', or_elim; apply wand_intro_r; auto.
-  apply wand_elim_r', or_elim; apply wand_intro_r; auto.
-  rewrite ?(comm _ Q); auto.
-Qed.
+Proof. intros; rewrite /TimelessP now_True_sep later_sep; auto. Qed.
 Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
 Proof.
   rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto.
@@ -1307,10 +1336,7 @@ Proof.
     [|intros [a ?]; exists a; apply HΨ].
 Qed.
 Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
-Proof.
-  intros ?; rewrite /TimelessP.
-  by rewrite -always_pure -!always_later -always_or; apply always_mono.
-Qed.
+Proof. intros; rewrite /TimelessP now_True_always -always_later; auto. Qed.
 Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
 Proof. destruct p; apply _. Qed.
 Global Instance eq_timeless {A : cofeT} (a b : A) :
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 08b7d7bab..ddc588c5f 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -269,6 +269,21 @@ Proof.
   rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
 Qed.
 
+Class MakeNowTrue (P Q : uPred M) := make_now_True : ◇ P ⊣⊢ Q.
+Global Instance make_now_True_true : MakeNowTrue True True.
+Proof.
+  rewrite /MakeNowTrue /uPred_now_True. apply (anti_symm _); auto with I.
+Qed.
+Global Instance make_now_True_default P : MakeNowTrue P (â—‡ P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_now_true R P Q Q' :
+  Frame R P Q → MakeNowTrue Q Q' → Frame R (◇ P) Q'.
+Proof.
+  rewrite /Frame /MakeNowTrue=><- <-.
+  by rewrite now_True_sep -(now_True_intro R).
+Qed.
+
 Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
   (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-- 
GitLab