From c012a2f311bdb3fca089b9f7322f4cd7e5de9e34 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 23:26:20 +0200
Subject: [PATCH] Generalize iTimeless to deal with now_True hypotheses.

---
 proofmode/class_instances.v | 12 +++++++++++-
 proofmode/classes.v         |  3 +++
 proofmode/coq_tactics.v     | 10 +++++-----
 proofmode/tactics.v         |  4 ++--
 4 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 7c3f504f2..988f33754 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -327,11 +327,21 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 
-(* IsTrueNow *)
+(* IntoNowTrue *)
+Global Instance into_now_True_now_True P : IntoNowTrue (â—‡ P) P.
+Proof. done. Qed.
+Global Instance into_now_True_timeless P : TimelessP P → IntoNowTrue (▷ P) P.
+Proof. done. Qed.
+
+(* IsNowTrue *)
 Global Instance is_now_True_now_True P : IsNowTrue (â—‡ P).
 Proof. by rewrite /IsNowTrue now_True_idemp. Qed.
 Global Instance is_now_True_later P : IsNowTrue (â–· P).
 Proof. by rewrite /IsNowTrue now_True_later. Qed.
+Global Instance is_now_True_rvs P : IsNowTrue P → IsNowTrue (|=r=> P).
+Proof.
+  rewrite /IsNowTrue=> HP. by rewrite -{2}HP -now_True_rvs -(now_True_intro P).
+Qed.
 
 (* FromViewShift *)
 Global Instance from_vs_rvs P : FromVs (|=r=> P) P.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 037de8467..730e5ee77 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -55,6 +55,9 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
   into_exist : P ⊢ ∃ x, Φ x.
 Global Arguments into_exist {_} _ _ {_}.
 
+Class IntoNowTrue (P Q : uPred M) := into_now_True : P ⊢ ◇ Q.
+Global Arguments into_now_True : clear implicits.
+
 Class IsNowTrue (Q : uPred M) := is_now_True : ◇ Q ⊢ Q.
 Global Arguments is_now_True : clear implicits.
 
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 1c0d4f3ac..83dd251a3 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -375,15 +375,15 @@ Proof.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
 
-Lemma tac_timeless Δ Δ' i p P Q :
+Lemma tac_timeless Δ Δ' i p P P' Q :
   IsNowTrue Q →
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
+  envs_lookup i Δ = Some (p, P) → IntoNowTrue P P' →
+  envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
-  rewrite always_if_later right_id HQ -{2}(is_now_True Q).
-  by rewrite (timelessP (â–¡?p P)) now_True_frame_r wand_elim_r.
+  rewrite right_id HQ -{2}(is_now_True Q).
+  by rewrite (into_now_True P) -now_True_always_if now_True_frame_r wand_elim_r.
 Qed.
 
 (** * Always *)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index dcf66b391..85791ec21 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -496,11 +496,11 @@ Tactic Notation "iNext":=
      apply _ || fail "iNext:" P "does not contain laters"|].
 
 Tactic Notation "iTimeless" constr(H) :=
-  eapply tac_timeless with _ H _ _;
+  eapply tac_timeless with _ H _ _ _;
     [let Q := match goal with |- IsNowTrue ?Q => Q end in
      apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
     |env_cbv; reflexivity || fail "iTimeless:" H "not found"
-    |let P := match goal with |- TimelessP ?P => P end in
+    |let P := match goal with |- IntoNowTrue ?P _ => P end in
      apply _ || fail "iTimeless:" P "not timeless"
     |env_cbv; reflexivity|].
 
-- 
GitLab