From 0a1c37a397b4adcc177e50e20945a382cf546d90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 2 Aug 2016 16:43:14 +0200
Subject: [PATCH] Syntax for framing the entire persistent context.

ProofMode.md  6 +++
proofmode/tactics.v  59 +++++++++++++++++++++++++++
2 files changed, 40 insertions(+), 25 deletions()
diff git a/ProofMode.md b/ProofMode.md
index cefa97d9..49a5bb57 100644
 a/ProofMode.md
+++ b/ProofMode.md
@@ 70,8 +70,10 @@ Elimination of logical connectives
Separating logic specific tactics

 `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. When
 `iFrame` is called without arguments, it attempts to frame all spatial
+ `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. The
+ symbol `★` can be used to frame as much of the spatial context as possible,
+ and the symbol `#` can be used to repeatedly frame as much of the persistent
+ context as possible. When without arguments, it attempts to frame all spatial
hypotheses.
 `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`.
diff git a/proofmode/tactics.v b/proofmode/tactics.v
index 4ce6a1b0..c878fa56 100644
 a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ 399,29 +399,6 @@ Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
apply _  fail "iSepDestruct:" H ":" P "not separating destructable"
env_cbv; reflexivity  fail "iSepDestruct:" H1 "or" H2 " not fresh"].
Tactic Notation "iFrame" constr(Hs) :=
 let rec go Hs :=
 match Hs with
  [] => idtac
  ?H :: ?Hs =>
 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
 lazy iota beta; go Hs]
 end
 in let Hs := words Hs in go Hs.

Tactic Notation "iFrame" :=
 let rec go Hs :=
 match Hs with
  [] => idtac
  ?H :: ?Hs => try iFrame 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 "iCombine" constr(H1) constr(H2) "as" constr(H) :=
eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
[env_cbv; reflexivity  fail "iCombine:" H1 "not found"
@@ 431,6 +408,42 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
apply _  fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
env_cbv; reflexivity  fail "iCombine:" H "not fresh"].
+(** Framing *)
+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
+ lazy iota beta].
+
+Local Ltac iFramePersistent :=
+ 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 iFrameSpatial :=
+ 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" constr(Hs) :=
+ let rec go Hs :=
+ match Hs with
+  [] => idtac
+  "#" :: ?Hs => iFramePersistent; go Hs
+  "★" :: ?Hs => iFrameSpatial; go Hs
+  ?H :: ?Hs => iFrameHyp H; go Hs
+ end
+ in let Hs := words Hs in go Hs.
+
+Tactic Notation "iFrame" := iFrameSpatial.
+
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
eapply tac_exist;

2.24.1