Make it possible to frame hypotheses using specialization patterns.

ProofMode.md

@@ -201,9 +201,12 @@ so called specification patterns to express this splitting:
 
 - `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
   spatial, it will be consumed.
-- `[H1 ... Hn]` : generate a goal with the spatial hypotheses `H1 ... Hn` and
-  all persistent hypotheses. The hypotheses `H1 ... Hn` will be consumed.
-- `[-H1 ... Hn]`  : negated form of the above pattern
+- `[H1 ... Hn]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
+  all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
+  consumed. Hypotheses may be prefixed with a `$`, which results in them being
+  framed in the generated goal.
+- `[-H1 ... Hn]`  : negated form of the above pattern. This pattern does not
+  accept hypotheses prefixed with a `$`.
 - `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a primitive view shift, in which case the view shift will be kept in the
   goal of the premise too.

program_logic/ownership.v

@@ -132,17 +132,17 @@ Qed.
 Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup I i P with "[-]") as (Q) "[% #HPQ]"; [by iFrame|].
-  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|?] HI]"; eauto.
+  iDestruct (invariant_lookup I i P with "[$Hw $Hi]") as (Q) "[% #HPQ]".
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
     iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
-  - iDestruct (ownE_singleton_twice with "[-]") as %[]. by iFrame.
+  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
 Qed.
 Lemma ownI_close i P : wsat ★ ownI i P ★ ▷ P ★ ownD {[i]} ⊢ wsat ★ ownE {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup with "[-]") as (Q) "[% #HPQ]"; first by iFrame.
+  iDestruct (invariant_lookup with "[$Hw $Hi]") as (Q) "[% #HPQ]".
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
   - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.

proofmode/spec_patterns.v

@@ -3,6 +3,7 @@ From iris.prelude Require Export strings.
 Record spec_goal := SpecGoal {
   spec_goal_vs : bool;
   spec_goal_negate : bool;
+  spec_goal_frame : list string;
   spec_goal_hyps : list string
 }.
 
@@ -22,7 +23,8 @@ Inductive token :=
   | TPersistent : token
   | TPure : token
   | TForall : token
-  | TVs : token.
+  | TVs : token
+  | TFrame : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -37,6 +39,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String "=" (String "=" (String ">" s)) => tokenize_go s (TVs :: cons_name kn k) ""
+  | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
@@ -51,9 +54,9 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   | TName s :: ts => parse_go ts (SName s :: k)
   | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
-  | TBracketL :: ts => parse_goal ts (SpecGoal false false []) k
-  | TVs :: TBracketL :: ts => parse_goal ts (SpecGoal true false []) k
-  | TVs :: ts => parse_go ts (SGoal (SpecGoal true true []) :: k)
+  | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
+  | TVs :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
+  | TVs :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
@@ -61,14 +64,19 @@ with parse_goal (ts : list token) (g : spec_goal)
     (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
-     guard (¬spec_goal_negate g ∧ spec_goal_hyps g = []);
-     parse_goal ts (SpecGoal (spec_goal_vs g) true (spec_goal_hyps g)) k
+     guard (¬spec_goal_negate g ∧ spec_goal_frame g = [] ∧ spec_goal_hyps g = []);
+     parse_goal ts (SpecGoal (spec_goal_vs g) true
+       (spec_goal_frame g) (spec_goal_hyps g)) k
   | TName s :: ts =>
      parse_goal ts (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
-                             (s :: spec_goal_hyps g)) k
+       (spec_goal_frame g) (s :: spec_goal_hyps g)) k
+  | TFrame :: TName s :: ts =>
+    guard (¬spec_goal_negate g);
+     parse_goal ts (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
+       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
   | TBracketR :: ts =>
      parse_go ts (SGoal (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
-                                  (reverse (spec_goal_hyps g))) :: k)
+       (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=

proofmode/tactics.v

@@ -124,6 +124,100 @@ Tactic Notation "iPureIntro" :=
     [let P := match goal with |- FromPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
+(** Framing *)
+Local Ltac iFrameFinish :=
+  lazy iota beta;
+  try match goal with
+  | |- _ ⊢ True => exact (uPred.pure_intro _ _ I)
+  end.
+
+Local Ltac iFramePure t :=
+  let φ := type of t in
+  eapply (tac_frame_pure _ _ _ _ t);
+    [apply _ || fail "iFrame: cannot frame" φ
+    |iFrameFinish].
+
+Local Ltac iFrameHyp H :=
+  eapply tac_frame with _ H _ _ _;
+    [env_cbv; reflexivity || fail "iFrame:" H "not found"
+    |let R := match goal with |- Frame ?R _ _ => R end in
+     apply _ || fail "iFrame: cannot frame" R
+    |iFrameFinish].
+
+Local Ltac iFrameAnyPure :=
+  repeat match goal with H : _ |- _ => iFramePure H end.
+
+Local Ltac iFrameAnyPersistent :=
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
+  match goal with
+  | |- of_envs ?Δ ⊢ _ =>
+     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
+  end.
+
+Local Ltac iFrameAnySpatial :=
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
+  match goal with
+  | |- of_envs ?Δ ⊢ _ =>
+     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
+  end.
+
+Tactic Notation "iFrame" := iFrameAnySpatial.
+
+Tactic Notation "iFrame" "(" constr(t1) ")" :=
+  iFramePure t1.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
+  iFramePure t1; iFrame ( t2 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
+  iFramePure t1; iFrame ( t2 t3 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).
+
+Tactic Notation "iFrame" constr(Hs) :=
+  let rec go Hs :=
+    match Hs with
+    | [] => idtac
+    | "%" :: ?Hs => iFrameAnyPure; go Hs
+    | "#" :: ?Hs => iFrameAnyPersistent; go Hs
+    | "★" :: ?Hs => iFrameAnySpatial; go Hs
+    | ?H :: ?Hs => iFrameHyp H; go Hs
+    end
+  in let Hs := words Hs in go Hs.
+Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
+  iFramePure t1; iFrame Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
+    constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
+
 (** * Specialize *)
 Record iTrm {X As} :=
   ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
@@ -180,8 +274,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |env_cbv; reflexivity
          |(*goal*)
          |go H1 pats]
-    | SGoal (SpecGoal ?vs ?lr ?Hs) :: ?pats =>
-       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
+    | SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs) :: ?pats =>
+       eapply tac_specialize_assert with _ _ _ H1 _ lr (Hs_frame ++ Hs) _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match vs with
@@ -189,7 +283,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           | true => apply _ || fail "iSpecialize: cannot generate view shifted goal"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
-         |(*goal*)
+         |iFrame Hs_frame (*goal*)
          |go H1 pats]
     end in let pats := spec_pat.parse pat in go H pats.
 
@@ -431,100 +525,6 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
      apply _ || fail "iCombine: cannot combine" P1 "and" P2
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
-(** Framing *)
-Local Ltac iFrameFinish :=
-  lazy iota beta;
-  try match goal with
-  | |- _ ⊢ True => exact (uPred.pure_intro _ _ I)
-  end.
-
-Local Ltac iFramePure t :=
-  let φ := type of t in
-  eapply (tac_frame_pure _ _ _ _ t);
-    [apply _ || fail "iFrame: cannot frame" φ
-    |iFrameFinish].
-
-Local Ltac iFrameHyp H :=
-  eapply tac_frame with _ H _ _ _;
-    [env_cbv; reflexivity || fail "iFrame:" H "not found"
-    |let R := match goal with |- Frame ?R _ _ => R end in
-     apply _ || fail "iFrame: cannot frame" R
-    |iFrameFinish].
-
-Local Ltac iFrameAnyPure :=
-  repeat match goal with H : _ |- _ => iFramePure H end.
-
-Local Ltac iFrameAnyPersistent :=
-  let rec go Hs :=
-    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
-  match goal with
-  | |- of_envs ?Δ ⊢ _ =>
-     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
-  end.
-
-Local Ltac iFrameAnySpatial :=
-  let rec go Hs :=
-    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
-  match goal with
-  | |- of_envs ?Δ ⊢ _ =>
-     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
-  end.
-
-Tactic Notation "iFrame" := iFrameAnySpatial.
-
-Tactic Notation "iFrame" "(" constr(t1) ")" :=
-  iFramePure t1.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
-  iFramePure t1; iFrame ( t2 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
-  iFramePure t1; iFrame ( t2 t3 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
-  iFramePure t1; iFrame ( t2 t3 t4 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) ")" :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) ")" :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) constr(t7) ")" :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).
-
-Tactic Notation "iFrame" constr(Hs) :=
-  let rec go Hs :=
-    match Hs with
-    | [] => idtac
-    | "%" :: ?Hs => iFrameAnyPure; go Hs
-    | "#" :: ?Hs => iFrameAnyPersistent; go Hs
-    | "★" :: ?Hs => iFrameAnySpatial; go Hs
-    | ?H :: ?Hs => iFrameHyp H; go Hs
-    end
-  in let Hs := words Hs in go Hs.
-Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
-  iFramePure t1; iFrame Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
-    constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) ")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) ")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
-Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
-    constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
-  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
-
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
   eapply tac_exist;
@@ -939,19 +939,20 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
   | [SGoalPersistent] =>
-     eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
+     eapply tac_assert_persistent with _ H Q;
        [env_cbv; reflexivity
        |(*goal*)
        |apply _ || fail "iAssert:" Q "not persistent"
        |tac H]
-  | [SGoal (SpecGoal ?vs ?lr ?Hs)] =>
-     eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
+  | [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
+     eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
        [match vs with
         | false => apply into_assert_default
         | true => apply _ || fail "iAssert: cannot generate view shifted goal"
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
-       |env_cbv; reflexivity|
+       |env_cbv; reflexivity
+       |iFrame Hs_frame (*goal*)
        |tac H]
   | ?pat => fail "iAssert: invalid pattern" pat
   end.