From e965b669432646c5cde0b0df3b2f80af5eecf0c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 May 2016 14:13:08 +0200
Subject: [PATCH] Merge iAssert and iPvsAssert.

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.
---
 heap_lang/lib/barrier/proof.v | 10 ++++-----
 proofmode/coq_tactics.v       | 33 ++++++++++++++++-------------
 proofmode/pviewshifts.v       | 36 +++++++-------------------------
 proofmode/spec_patterns.v     | 22 +++++++++++++-------
 proofmode/tactics.v           | 39 ++++++++++++++++++++---------------
 tests/proofmode.v             | 19 ++++++++++++++---
 6 files changed, 84 insertions(+), 75 deletions(-)

diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index a002baa5f..fdff15b7b 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -109,8 +109,8 @@ Proof.
     iSplit; [|done]. by iIntros "> ?". }
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }
-  iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ★ sts_ownS γ' low_states {[Send]})%I with "[-]" as "[Hr Hs]".
+  iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
+    ★ sts_ownS γ' low_states {[Send]})%I with "=>[-]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
     + iApply (sts_own_weaken with "Hγ'");
@@ -148,7 +148,7 @@ Proof.
     iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
     { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
     iIntros "Hγ".
-    iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
   - (* a High state: the comparison succeeds, and we perform a transition and
@@ -184,8 +184,8 @@ Proof.
   - iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
   - iIntros "Hγ".
-    iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
-      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "[-]" as "[Hγ1 Hγ2]".
+    iAssert (sts_ownS γ (i_states i1) {[Change i1]}
+      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]".
     { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
       + set_solver.
       + iApply (sts_own_weaken with "Hγ");
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 938eecce3..3e2a5691f 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -494,24 +494,28 @@ Proof.
     by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q :
+Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
+  to_assert : (R ★ (P -★ Q)) ⊢ Q.
+Global Arguments to_assert _ _ _ {_}.
+Lemma to_assert_fallthrough P Q : ToAssert P Q P.
+Proof. by rewrite /ToAssert wand_elim_r. Qed.
+
+Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  ToWand R P1 P2 →
+  ToWand R P1 P2 → ToAssert P1 Q P1' →
   ('(Δ1,Δ2) ← envs_split lr js Δ';
-    Δ2' ← envs_app (envs_persistent Δ1 && q) (Esnoc Enil j P2) Δ2;
+    Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  Δ1 ⊢ P1 → Δ2' ⊢ Q → Δ ⊢ Q.
+  Δ1 ⊢ P1' → Δ2' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HP1 <-.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
-  destruct (envs_persistent Δ1) eqn:?; simplify_eq/=.
-  - rewrite right_id (to_wand R) (persistentP Δ1) HP1.
-    by rewrite assoc (always_elim_if q) -always_if_sep wand_elim_l wand_elim_r.
-  - rewrite right_id (to_wand R).
-    by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
+  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
+  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
+  by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
 Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
@@ -559,14 +563,15 @@ Proof.
   intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
 Qed.
 
-Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
+Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
+  ToAssert P Q R →
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  Δ1 ⊢ P → Δ2' ⊢ Q → Δ ⊢ Q.
+  Δ1 ⊢ R → Δ2' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HP HQ. rewrite envs_split_sound //.
+  intros ??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
-  by rewrite right_id HP HQ wand_elim_r.
+  by rewrite right_id HP HQ.
 Qed.
 
 Lemma tac_assert_persistent Δ Δ' j P Q :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e9450cdae..bf2b58384 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -31,7 +31,7 @@ Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
 Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
     (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
-  fsa_split : fsa E Φ ⊢ P;
+  fsa_split : fsa E Φ ⊣⊢ P;
   fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
 }.
 Global Arguments fsa_split {_} _ _ _ _ _ {_}.
@@ -42,6 +42,13 @@ Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
   FrameShiftAssertion fsaV fsa → FSASplit (fsa E Φ) E fsa fsaV Φ.
 Proof. done. Qed.
 
+Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
+  FSASplit Q E fsa fsaV Φ → ToAssert P Q (|={E}=> P).
+Proof.
+  intros.
+  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
+Qed.
+
 Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → Δ ⊢ Q → Δ ⊢ |={E1,E2}=> Q.
 Proof. intros -> ->. apply pvs_intro. Qed.
 
@@ -87,17 +94,6 @@ Proof.
   intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
   eauto using tac_pvs_timeless.
 Qed.
-
-Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
-  FSASplit Q E fsa fsaV Φ →
-  envs_split lr js Δ = Some (Δ1,Δ2) →
-  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  Δ1 ⊢ (|={E}=> P) → Δ2' ⊢ fsa E Φ → Δ ⊢ Q.
-Proof.
-  intros ??? HP HQ. rewrite -(fsa_split Q) -fsa_pvs_fsa -HQ envs_split_sound //.
-  rewrite HP envs_app_sound //; simpl.
-  by rewrite right_id pvs_frame_r wand_elim_r.
-Qed.
 End pvs.
 
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
@@ -185,19 +181,3 @@ Tactic Notation "iTimeless" constr(H) :=
 
 Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
   iTimeless H; iDestruct H as Hs.
-
-Tactic Notation "iPvsAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
-  let H := iFresh in
-  let Hs := spec_pat.parse_one Hs in
-  lazymatch Hs with
-  | SGoal ?lr ?Hs =>
-     eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
-       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
-        apply _ || fail "iPvsAssert: " P "not a pvs"
-       |env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
-       |env_cbv; reflexivity|
-       |simpl; iDestruct H as pat]
-  | ?pat => fail "iPvsAssert: invalid pattern" pat
-  end.
-Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
-  iPvsAssert Q with "[]" as pat.
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index e3c065a65..c6919d5fa 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,7 +1,9 @@
 From iris.prelude Require Export strings.
 
+Inductive spec_goal_kind := GoalStd | GoalPvs.
+
 Inductive spec_pat :=
-  | SGoal : bool → list string → spec_pat
+  | SGoal : spec_goal_kind → bool → list string → spec_pat
   | SGoalPersistent : spec_pat
   | SGoalPure : spec_pat
   | SName : bool → string → spec_pat (* first arg = persistent *)
@@ -15,7 +17,8 @@ Inductive token :=
   | TBracketR : token
   | TPersistent : token
   | TPure : token
-  | TForall : token.
+  | TForall : token
+  | TPvs : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -29,13 +32,14 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
+  | String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
 Inductive state :=
   | StTop : state
-  | StAssert : bool → list string → state.
+  | StAssert : spec_goal_kind → bool → list string → state.
 
 Fixpoint parse_go (ts : list token) (s : state)
     (k : list spec_pat) : option (list spec_pat) :=
@@ -46,16 +50,18 @@ Fixpoint parse_go (ts : list token) (s : state)
      | TName s :: ts => parse_go ts StTop (SName false s :: k)
      | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
      | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
-     | TBracketL :: ts => parse_go ts (StAssert false []) k
+     | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
+     | TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
+     | TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
      | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
      | TForall :: ts => parse_go ts StTop (SForall :: k)
      | _ => None
      end
-  | StAssert neg ss =>
+  | StAssert kind neg ss =>
      match ts with
-     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert true ss) k
-     | TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k
-     | TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k)
+     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert kind true ss) k
+     | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
+     | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
      | _ => None
      end
   end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 195995bfc..17fc75871 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -186,10 +186,11 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |env_cbv; reflexivity
          |(*goal*)
          |go H1 pats]
-    | SGoal ?lr ?Hs :: ?pats =>
-       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
+    | SGoal ?k ?lr ?Hs :: ?pats =>
+       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
+         |match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
          |(*goal*)
          |go H1 pats]
@@ -225,24 +226,25 @@ Tactic Notation "iPoseProof" open_constr(t) :=
   let H := iFresh in iPoseProof t as H.
 
 (** * Apply *)
-Tactic Notation "iApplyCore" constr(H) := first
-  [iExact H
-  |eapply tac_apply with _ H _ _ _;
-     [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
-     |apply _ || fail 1 "iApply: cannot apply" H|]].
-
 Tactic Notation "iApply" open_constr(t) :=
+  let finish H := first
+    [iExact H
+    |eapply tac_apply with _ H _ _ _;
+       [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
+       |let P := match goal with |- ToWand ?P _ _ => P end in
+        apply _ || fail 1 "iApply: cannot apply" H ":" P
+       |lazy beta (* reduce betas created by instantiation *)]] in
   let Htmp := iFresh in
   lazymatch t with
   | ITrm ?H ?xs ?pat =>
      iPoseProofCore H as Htmp; last (
        iSpecializeArgs Htmp xs;
        try (iSpecializeArgs Htmp (hcons _ _));
-       iSpecializePat Htmp pat; last iApplyCore Htmp)
+       iSpecializePat Htmp pat; last finish Htmp)
   | _ =>
      iPoseProofCore t as Htmp; last (
        try (iSpecializeArgs Htmp (hcons _ _));
-       iApplyCore Htmp)
+       finish Htmp)
   end; try apply _.
 
 (** * Revert *)
@@ -703,18 +705,21 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
-  | [SGoal ?lr ?Hs] =>
-     eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
-       [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
-       |env_cbv; reflexivity|
-       |iDestructHyp H as pat]
-  | [SGoalPersistent]  =>
+  | [SGoalPersistent] =>
      eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
-       [apply _ || fail "iAssert:" Q "not persistent"
+       [env_cbv; reflexivity
+       |(*goal*)
+       |apply _ || fail "iAssert:" Q "not persistent"
+       |iDestructHyp H as pat]
+  | [SGoal ?k ?lr ?Hs] =>
+     eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
+       [match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
+       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
        |env_cbv; reflexivity|
        |iDestructHyp H as pat]
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
+
 Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
   iAssert Q with "[]" as pat.
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0dec14048..a74ee879e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : cmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
@@ -83,13 +83,26 @@ Qed.
 
 Section iris.
   Context {Λ : language} {Σ : iFunctor}.
+  Implicit Types E : coPset.
+  Implicit Types P Q : iProp Λ Σ.
 
-  Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
+  Lemma demo_7 E1 E2 E P :
     E1 ⊆ E2 → E ⊆ E1 →
     (|={E1,E}=> ▷ P) ⊢ (|={E2,E ∪ E2 ∖ E1}=> ▷ P).
   Proof.
     iIntros {? ?} "Hpvs".
-    iPvs "Hpvs"; first (split_and?; set_solver).
+    iPvs "Hpvs"; first set_solver.
     done.
   Qed.
+
+  Lemma demo_8 N E P Q R :
+    nclose N ⊆ E →
+    (True -★ P -★ inv N Q -★ True -★ R) ⊢ (P -★ ▷ Q -★ |={E}=> R).
+  Proof.
+    iIntros {?} "H HP HQ".
+    iApply ("H" with "[#] HP =>[HQ] =>").
+    - done.
+    - by iApply inv_alloc.
+    - by iPvsIntro.
+  Qed.
 End iris.
-- 
GitLab