Syntax for framing the entire persistent context.

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`.

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;

[Ghost User]

it looks like I just tried to use iFrame frame out a thing in Coq context ... but never mind

[Ralf Jung]

Yeah, that still doesn't work.

[Robbert]

What exactly does not work. Do you have some code demonstrating the issue?

[Ghost User]

Sorry for not clarifying this ... for example,

H : heapN ⊥ N
o, n, n' : nat
============================
​​"~" : heap_ctx
​"~2" : inv N (lock_inv γ1 γ2 lo ln R)
​"IH" : own γ2 (Excl ()) -★ R -★ Φ #() -★ WP release (#lo, #ln) {{ v, Φ v }}
​"~3" : heapN ⊥ N
--------------------------------------□
​​"Hlo'" : lo ↦ #(o + 1)
​"HR" : R
​"Hγ" : own γ2 (Excl ())
--------------------------------------★
heapN ⊥ N
∧ lo ↦ #(o + 1%nat)
  ★ (own γ2 (Excl ()) ★ R ∨ auth_own γ1 (GSet {[(o + 1)%nat]}))

If I now iFrame, H in Coq context (or even ~3 ... this hypothesis is littered by me everywhere ...) have no effect on the heapN ⊥ N in goal. I have to do iSplit; first by auto.

The snippet is from ticket_lock.v (the version here https://gitlab.mpi-sws.org/FP/iris-coq/commit/3f3ead3512c0fba3b3682fb02b703987463dcb55)

[Ghost User]

More exactly: https://gitlab.mpi-sws.org/FP/iris-coq/blob/3f3ead3512c0fba3b3682fb02b703987463dcb55/heap_lang/lib/ticket_lock.v#L162