From 6e10b9aa0e6cb727442e49b5bcf999c34184a78d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jul 2016 16:09:11 +0200
Subject: [PATCH] Generalize iTimeless tactic.

---
 proofmode/classes.v     |  3 +++
 proofmode/coq_tactics.v | 10 ++++++++
 proofmode/pviewshifts.v | 53 ++++++++++-------------------------------
 proofmode/tactics.v     |  9 +++++++
 4 files changed, 34 insertions(+), 41 deletions(-)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index a88e3daf7..c25740c0c 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -312,4 +312,7 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
 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.
+
+Class TimelessElim (Q : uPred M) :=
+  timeless_elim `{!TimelessP P} R : (R ⊢ Q) → ▷ P ★ (P -★ R) ⊢ Q.
 End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 1ac516bbd..3b3bb0f12 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -375,6 +375,16 @@ Proof.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
 
+Lemma tac_timeless Δ Δ' i p P Q :
+  TimelessElim Q →
+  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP 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. by apply timeless_elim.
+Qed.
+
 (** * Always *)
 Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof. intros. by apply: always_intro. Qed.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e919ea13e..8695abb15 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -30,6 +30,12 @@ Global Instance into_wand_pvs E1 E2 R P Q :
   IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
 Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
+Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
+Proof.
+  intros P ? R HR. rewrite (pvs_timeless E1 P) pvs_frame_r.
+  by rewrite wand_elim_r HR pvs_trans; last set_solver.
+Qed.
+
 Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
     (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
   is_fsa : P ⊣⊢ fsa E Φ;
@@ -48,6 +54,12 @@ Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
 Proof.
   intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
 Qed.
+Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
+  IsFSA Q E fsa fsaV Φ → TimelessElim Q.
+Proof.
+  intros ? P ? R. rewrite (is_fsa Q) -{2}fsa_pvs_fsa. intros <-.
+  by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
+Qed.
 
 Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → (Δ ⊢ Q) → Δ ⊢ |={E1,E2}=> Q.
 Proof. intros -> ->. apply pvs_intro. Qed.
@@ -74,26 +86,6 @@ Proof.
   intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eapply tac_pvs_elim; set_solver.
 Qed.
-
-Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
-  (Δ' ={E1,E2}=> Q) → Δ ={E1,E2}=> Q.
-Proof.
-  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
-  rewrite always_if_later (pvs_timeless E1 (â–¡?_ P)%I) pvs_frame_r.
-  by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
-Qed.
-
-Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
-  IsFSA Q E fsa fsaV Φ →
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
-  (Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
-Proof.
-  intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
-  eauto using tac_pvs_timeless.
-Qed.
 End pvs.
 
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
@@ -161,26 +153,5 @@ Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
   iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
-Tactic Notation "iTimeless" constr(H) :=
-  match goal with
-  | |- _ ⊢ |={_,_}=> _ =>
-     eapply tac_pvs_timeless with _ H _ _;
-       [env_cbv; reflexivity || fail "iTimeless:" H "not found"
-       |let P := match goal with |- TimelessP ?P => P end in
-        apply _ || fail "iTimeless: " P "not timeless"
-       |env_cbv; reflexivity|simpl]
-  | |- _ =>
-     eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
-       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
-        apply _ || fail "iTimeless: " P "not a pvs"
-       |env_cbv; reflexivity || fail "iTimeless:" H "not found"
-       |let P := match goal with |- TimelessP ?P => P end in
-        apply _ || fail "iTimeless: " P "not timeless"
-       |env_cbv; reflexivity|simpl]
-  end.
-
-Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
-  iTimeless H; iDestruct H as Hs.
-
 Hint Extern 2 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (|={_}=> _)%I => iPvsIntro end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 8e6a504da..3901386c4 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -501,6 +501,15 @@ Tactic Notation "iNext":=
     |let P := match goal with |- FromLater ?P _ => P end in
      apply _ || fail "iNext:" P "does not contain laters"|].
 
+Tactic Notation "iTimeless" constr(H) :=
+  eapply tac_timeless with _ H _ _;
+    [let Q := match goal with |- TimelessElim ?Q => Q end in
+     apply _ || fail "iTimeless: cannot eliminate later in goal" Q
+    |env_cbv; reflexivity || fail "iTimeless:" H "not found"
+    |let P := match goal with |- TimelessP ?P => P end in
+     apply _ || fail "iTimeless: " P "not timeless"
+    |env_cbv; reflexivity|].
+
 (** * Introduction tactic *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x
-- 
GitLab