feat: iframe with existential quantifiers

Iris/Iris/Instances/Lib/Invariants.lean

@@ -139,7 +139,6 @@ theorem own_inv_alloc (N : Namespace) (E : CoPset) (P : IProp GF) :
   · intro E; apply fresh_name
   · isplitl [Hw] <;> iassumption
   · imodintro; iframe
-    iexists i; iframe
     itrivial
 
 @[rocq_alias own_inv_alloc_open]

Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean

@@ -148,8 +148,6 @@ theorem weakestpre_completeness {Cini : List Expr × State} {f : Forking} {γ :
     · imodintro
       imodintro
       iframe
-      iexists q
-      iframe
       ipureintro ; grind
   · imod AbstractLangCompletenessGen.lang_completeness $$ %HnotStuck' He [Hheap HtpInv]
         with (⟨%K, %e₁, %Hctx, %Heq, %Hval, %Hatom, H⟩|⟨Hheap, Htpinv, H⟩)

Iris/Iris/ProgramLogic/WeakestPre.lean

@@ -617,15 +617,12 @@ variable [ι : IrisGS_gen hlc Expr GF]
 variable {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ Ψ : Val → IProp GF} {P Q R : IProp GF}
 
 @[rocq_alias frame_wp]
-instance frameWp {p : Bool} [H : ∀ v, Frame p R (Φ v) (Ψ v)] :
-    -- TODO: move FrameInstantiateExistDisabled over the `FrameInstantiateExistDisabled` constant
-    -- Blocked by #390
-    -- see: https://github.com/leanprover-community/iris-lean/pull/393
+instance frameWp {p : Bool} [H : ∀ v, FrameInstantiateExistDisabled p R (Φ v) (Ψ v)] :
     Frame p R (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Ψ }}) where
   frame := by
     refine wp_frame_l.trans ?_
     apply wp_mono
-    exact fun v => frame
+    exact fun v => (H v).frame_instantiatiate_exist_disabled.frame
 
 @[rocq_alias is_except_0_wp]
 instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where

Iris/Iris/ProofMode/Classes.lean

@@ -215,6 +215,11 @@ class Frame {PROP} [BI PROP] (p : Bool) (R P : PROP) (Q : outParam $ PROP) where
   frame : □?p R ∗ Q ⊢ P
 export Frame (frame)
 
+@[ipm_class, rocq_alias FrameInstantiateExistDisabled]
+class FrameInstantiateExistDisabled {PROP} [BI PROP] (p : Bool) (R P : PROP) (Q : outParam $ PROP) where
+  frame_instantiatiate_exist_disabled : Frame p R P Q
+export FrameInstantiateExistDisabled (frame_instantiatiate_exist_disabled)
+
 /--
 `IntoLaterN` turns `P` into `▷^[n] Q`.
 The Boolean [only_head] indicates whether laters should only be stripped in head position or also below

Iris/Iris/ProofMode/InstancesFrame.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Alvin Tang
 -/
 module
 
@@ -11,6 +11,18 @@ public import Iris.ProofMode.ClassesMake
 public meta import Iris.ProofMode.Expr
 public import Iris.Std.TC
 
+public meta section
+
+register_option iris.frame.instantiateExists : Bool := {
+  defValue := true
+  descr := "When set as `true`, `iframe` may instantiate existential \
+    quantifiers in the goal while framing. Set to `false` to allow framing \
+    below existential quantifiers without instantiating any existentially \
+    quantified variables."
+}
+
+end
+
 @[expose] public section
 
 namespace Iris.ProofMode
@@ -60,8 +72,10 @@ instance frame_here_pure [BI PROP] {a : Bool} {φ : Prop} {Q : PROP}
 
 @[ipm_backtrack, rocq_alias frame_wand]
 instance frame_wand [BI PROP] p (R P1 P2 Q2 : PROP)
-    [h : Frame p R P2 Q2] : Frame p R iprop(P1 -∗ P2) iprop(P1 -∗ Q2) where
-  frame := wand_intro <| sep_assoc.1.trans <| (sep_mono_right wand_elim_left).trans h.frame
+    [h : FrameInstantiateExistDisabled p R P2 Q2] :
+    Frame p R iprop(P1 -∗ P2) iprop(P1 -∗ Q2) where
+  frame := wand_intro <| sep_assoc.1.trans <| (sep_mono_right wand_elim_left).trans
+    h.frame_instantiatiate_exist_disabled.frame
 
 @[ipm_backtrack, rocq_alias frame_affinely]
 instance frame_affinely [BI PROP] p (R P Q Q' : PROP)
@@ -108,19 +122,21 @@ instance frame_persistently [BI PROP] (R P Q Q' : PROP)
 
 @[ipm_backtrack, rocq_alias frame_forall]
 instance frame_forall {α} [BI PROP] p R (Φ Ψ : α → PROP)
--- TODO: add FrameInstantiateExistDisabled to the premise once supported
-    [h : ∀ a, Frame p R (Φ a) (Ψ a)] :
+    [h : ∀ a, FrameInstantiateExistDisabled p R (Φ a) (Ψ a)] :
     Frame p R iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
-  frame := forall_intro λ a => (sep_mono_right (forall_elim a)).trans (h a).1
+  frame := forall_intro λ a =>
+    (sep_mono_right (forall_elim a)).trans (h a).frame_instantiatiate_exist_disabled.frame
 
 @[ipm_backtrack, rocq_alias frame_impl_persistent]
 instance frame_impl_persistent [BI PROP] (R P1 P2 Q2 : PROP)
-    [h : Frame true R P2 Q2] : Frame true R iprop(P1 → P2) iprop(P1 → Q2) where
+    [h : FrameInstantiateExistDisabled true R P2 Q2] :
+    Frame true R iprop(P1 → P2) iprop(P1 → Q2) where
   frame := imp_intro <|
     (and_mono_left persistently_and_intuitionistically_sep_left.2).trans <|
     and_assoc.1.trans <|
     (and_mono_right (and_comm.1.trans imp_elim_right)).trans <|
-    persistently_and_intuitionistically_sep_left.1.trans h.frame
+    persistently_and_intuitionistically_sep_left.1.trans
+    h.frame_instantiatiate_exist_disabled.frame
 
 /-
 You may wonder why this uses [Persistent] and not [QuickPersistent].
@@ -132,14 +148,14 @@ a new typeclass just for this extremely rarely used instance.
 @[ipm_backtrack, rocq_alias frame_impl]
 instance frame_impl [BI PROP] (R P1 P2 Q2 : PROP)
     [hp : Persistent P1] [ha : QuickAbsorbing P1]
-    [h : Frame false R P2 Q2] : Frame false R iprop(P1 → P2) iprop(P1 → Q2) where
+    [h : FrameInstantiateExistDisabled false R P2 Q2] : Frame false R iprop(P1 → P2) iprop(P1 → Q2) where
   frame :=
     have : Absorbing P1 := ha.quick_absorbing
     imp_intro <|
       persistent_and_affinely_sep_right.1.trans <|
       sep_assoc.1.trans <|
       (sep_mono_right (sep_comm.1.trans (persistent_and_affinely_sep_left.2.trans imp_elim_right))).trans <|
-      h.frame
+      h.frame_instantiatiate_exist_disabled.frame
 
 @[ipm_backtrack, rocq_alias frame_later]
 instance frame_later [BI PROP] p (R R' P Q Q' : PROP)
@@ -236,10 +252,46 @@ theorem frame_or [BI PROP] p (R P1 P2 Q1 Q2 Q' : PROP)
     sep_or_left.1.trans <|
     or_mono h1.frame h2.frame
 
+@[rocq_alias frame_exist]
+theorem frame_exist [BI PROP] {α} (p : Bool) (R : PROP) (Φ : α → PROP)
+    (a : α) (Q : PROP) (inst : Frame p R (Φ a) Q) :
+    Frame p R iprop(BI.exists Φ) Q where
+  frame := inst.frame.trans <| exists_intro a
+
+@[rocq_alias frame_exist_no_instantiate]
+theorem frame_exist_no_instantiate [BI PROP] {α} (p : Bool) (R : PROP) (Φ Ψ : α → PROP)
+    (inst : ∀ a, Frame p R (Φ a) (Ψ a)) :
+    Frame p R iprop(BI.exists Φ) iprop(BI.exists Ψ) where
+  frame := sep_exists_left.mp.trans <|
+    exists_elim <| fun a => (inst a).frame.trans <| exists_intro a
+
 end tactic_theorems
 
 meta section tactics
-open Lean
+open Lean Elab Meta Std
+
+def frameInstantiateExistsEnabled : MetaM Bool := do
+  return iris.frame.instantiateExists.get (← getOptions)
+
+def withFrameInstantiateExistsDisabled {α} (x : MetaM α) : MetaM α :=
+  withOptions (iris.frame.instantiateExists.set · false) x
+
+theorem frameInstantiateExistsDisabled_of [BI PROP] {p} {R P Q : PROP} (h : Frame p R P Q) :
+    FrameInstantiateExistDisabled p R P Q := ⟨h⟩
+
+@[ipm_tactic_instance FrameInstantiateExistDisabled _ _ _ _]
+def frameNoInstantiateExist : SynthTactic := λ e => do
+  let_expr FrameInstantiateExistDisabled prop bi p R P G := e | return .continue
+  have u := e.getAppFn.constLevels![0]!
+  have prop : Q(Type u) := prop
+  have _bi : Q(BI $prop) := bi
+  have p : Q(Bool) := p
+  have R : Q($prop) := R
+  have P : Q($prop) := P
+  have G : Q($prop) := G
+  let some inst ← withFrameInstantiateExistsDisabled <|
+    synthInstanceRecursiveQ q(Frame $p $R $P $G) | return .continue
+  return .success q(frameInstantiateExistsDisabled_of $inst)
 
 /-- corresponds to the MaybeFrame typeclass in Rocq -/
 @[rocq_alias MaybeFrame', rocq_alias maybe_frame_frame]
@@ -353,3 +405,80 @@ def frameOr : SynthTactic := λ e => do
       throwError "MakeOr should always succeed"
     return .success q(frame_or $p $R $P1 $P2 $Q1 $Q2 $Q')
   return .continue
+
+def frameHereApplies {u : Level} {prop : Q(Type u)} (_bi : Q(BI $prop)) (R P : Q($prop)) :
+    MetaM Bool := withoutModifyingState do
+  if ← isDefEq P R then return true
+  let_expr BI.affinely _ _ R' := R | return false
+  isDefEq P R'
+
+/-- Analogous to `solve_gather_evars_eq` in the Rocq implementation. -/
+def solveGatherEvarsEq (a c : Expr) : MetaM Bool := do
+  match a with
+  | .mvar m =>
+    if ← m.isDelayedAssigned then return false
+    let decl ← m.getDecl
+    -- The metavaiable `m` cannot be older than `c`, or else assignment is out of scope
+    unless decl.lctx.contains c.fvarId! do
+      return false
+    unless decl.depth == (← getMCtx).depth do
+      return false
+    if decl.kind.isSyntheticOpaque then
+      return false
+    m.assign c
+    return true
+  | _ => return false
+
+@[ipm_tactic_instance Frame _ _ iprop(∃ _, _) _]
+def frameExist : SynthTactic := λ e => do
+  let_expr Frame prop bi p R P _ := e | return .continue
+  have u := e.getAppFn.constLevels![0]!
+  have prop : Q(Type u) := prop
+  have _bi : Q(BI $prop) := bi
+  have p : Q(Bool) := p
+  have R : Q($prop) := R
+  let_expr BI.exists _ _ α Φ := P | return .continue
+
+  let .sort v ← inferType α | return .continue
+  have α : Q(Sort v) := α
+  have Φ : Q($α → $prop) := Φ
+
+  -- Find the binder name so that it can be reused after framing
+  let bn := match Φ with | .lam n .. => n | _ => `x
+
+  -- Introduce a free variable `c` for the computation within `withLocalDeclDQ`
+  let some ⟨a, X, inst⟩ ← withLocalDeclDQ bn α fun c => do
+    let a : Q($α) ←
+      if ← frameInstantiateExistsEnabled then
+        mkFreshExprMVarQ q($α)
+      else pure c
+    let G ← mkFreshExprMVarQ q($prop)
+    have body : Q($prop) := Expr.headBeta q($Φ $a)
+    let some inst ← synthInstanceRecursiveQ q(Frame $p $R $body $G) | return none
+    -- The existential quantifier remains (`a == c` when framing of existential is disabled)
+    if a == c || (← solveGatherEvarsEq (← instantiateMVars a) c) then
+      return some (none, ← mkLambdaFVars #[c] (← instantiateMVars G),
+                          ← mkLambdaFVars #[c] (← instantiateMVars inst))
+    let a ← instantiateMVars a
+    let G ← instantiateMVars G
+    if a.containsFVar c.fvarId! || G.containsFVar c.fvarId! then return none
+    -- The existential quantifier does not remain as the existential variable is instantiated
+    return some (some a, G, ← instantiateMVars inst)
+  | return .continue
+
+  match a with
+  | none =>
+    have Ψ : Q($α → $prop) := X
+    let inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := inst
+    return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $inst)
+  | some a =>
+    have a : Q($α) := a
+    have G : Q($prop) := X
+    let inst : Q(Frame $p $R ($Φ $a) $G) := inst
+    return .success q(frame_exist $p $R $Φ $a $G $inst)
+
+#rocq_ignore frame_exist_helper "Logic already handled in the metaprogram frameExist"
+#rocq_ignore GatherEvarsEq "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"
+#rocq_ignore TCCbnTele "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"
+#rocq_ignore frame_texist "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"
+#rocq_ignore frame_tforall "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"

Iris/Iris/ProofMode/Porting.lean

@@ -31,7 +31,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iEmpIntro" ported "iempintro"
 #rocq_concept proofmode "Tactics" "iPureIntro" ported "ipureintro"
 #rocq_concept proofmode "Tactics" "iFrame (basic)" ported "iframe"
-#rocq_concept proofmode "Tactics" "iFrame (existential quantifiers)" missing ""
+#rocq_concept proofmode "Tactics" "iFrame (existential quantifiers)" ported "iframe"
 #rocq_concept proofmode "Tactics" "iRevert" ported "irevert"
 #rocq_concept proofmode "Tactics" "iPoseProof" ported "ihave _ := _"
 #rocq_concept proofmode "Tactics" "iSpecialize (basic)" ported "ispecialize"

Iris/Iris/Tests/Tactics.lean

@@ -11,11 +11,13 @@ public import Iris.Instances.IProp
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.Instances.Lib.Token
 public import Iris.Algebra.CMRA
+public import Iris.ProgramLogic.Language
+public import Iris.ProgramLogic.WeakestPre
 
 @[expose] public section
 
 namespace Iris.Tests
-open BI CMRA DFrac
+open BI CMRA DFrac ProgramLogic
 
 /- This file contains tests with various scenarios for all available tactics. -/
 
@@ -2467,6 +2469,105 @@ example [BI PROP] [BIAffine PROP] (Q : Nat → PROP) : (Q 0 ⊢ ∃ x, False ∨
   iexists _
   iframe
 
+/- Tests `iframe` with existential quantifiers -/
+example [BI PROP] {α} (a : α) {β} (b : β) (P : PROP)
+    (Q : α → PROP) (R : β → PROP) (S : PROP) :
+    ⊢ P -∗ Q a -∗ R b -∗ S -∗ ∃ n, Q n ∗ ∃ m, R m ∗ P ∗ S := by
+  iintro HP HQ HR HS
+  -- Instantiate the inner existential quantifier `m`
+  iframe HR
+  -- Keep the outer existential quantifier `n` around
+  iframe HP
+  -- Instantiate the outer existential quantifier `n`
+  iframe HQ
+  iassumption
+
+/- Tests `iframe` with multiple existential quantifiers framed at once -/
+example [BI PROP] {α} (a : α) {β} (b : β) (P : PROP)
+    (Q : α → PROP) (R : β → PROP) (S : PROP) :
+    ⊢ P -∗ Q a -∗ R b -∗ S -∗ ∃ n, Q n ∗ ∃ m, R m ∗ P ∗ S := by
+  iintro HP HQ HR HS
+  iframe HS HP HR HQ
+
+/- Tests `iframe` with existential quantifers in various orders -/
+example [BI PROP] {α} (a : α) {β} (b : β) {γ} (c : γ)
+    (P : α → β → PROP) (Q : β → α → γ → PROP) :
+    ⊢ P a b -∗ Q b a c -∗ ∃ x, ∃ y, (P x y ∗ ∃ z, Q y x z) := by
+  iintro HP HQ
+  iframe
+
+/-
+  Tests `iframe` with the framing of existential quantifiers disabled.
+  The tactic should succeed as `P`, which is under the existential
+  quantifier, can still be framed.
+-/
+set_option iris.frame.instantiateExists false in
+example [BI PROP] {α} (a : α) (P : PROP) (Q R : α → PROP) (S : PROP) :
+    ⊢ P -∗ Q a -∗ R a -∗ S -∗ ∃ n, P ∗ Q n ∗ ∃ m, R m ∗ S := by
+  iintro HP HQ HR HS
+  iframe ∗
+  iexists a
+  iframe HQ
+  iexists a
+  iassumption
+
+/-
+  Tests `iframe` with the framing of existential quantifiers disabled.
+  Since nothing else can be framed, the tactic should fail.
+-/
+/-- error: iframe: cannot frame P a -/
+#guard_msgs in
+set_option iris.frame.instantiateExists false in
+example [BI PROP] {α} (a : α) (P : α → PROP) :
+    ⊢ P a -∗ ∃ n, P n := by
+  iintro HP
+  iframe HP
+
+/- Tests `iframe` with an existential quantifier under a universal quantifier. -/
+example [BI PROP] (P : PROP) : P ⊢ ∀ (x : Nat), ∃ n, ⌜n = x⌝ ∗ P := by
+  iintro HP
+  iframe HP
+  iintro %x
+  iexists x
+  ipureintro; rfl
+
+/- Tests `iframe` with an existentially quantified binder instantiated with a metavariable. -/
+example [BI PROP] (P Q : Nat → PROP) (m : Nat) :
+    ⊢ P m -∗ ∃ n, Q n -∗ ∃ x y, P x ∗ Q y ∗ ⌜y = 3⌝ := by
+  iintro HP
+  iexists ?w
+  iintro HQ
+  -- The existentially quantified binder `y` instantiated with `?w`
+  iframe HQ
+  iframe HP
+  ipureintro
+  rfl
+
+/-
+  Tests `iframe` with an existentially quantified binder instantiated with
+  a value that involves a metavariable.
+-/
+example [BI PROP] (P : Option Nat → PROP) :
+    ⊢ (∀ n, P (some n)) -∗ ∃ x, P x := by
+  iintro HP
+  ispecialize HP $$ %(?n)
+  -- The existentially quantified binder `x` instantiated with `some ?n`
+  iframe HP
+  exact 0
+
+variable {hlc : outParam HasLC} {Expr State Obs Val} [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors}
+variable [IrisGS_gen hlc Expr GF]
+variable {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ : Val → IProp GF}
+
+/- Tests `iframe` with the `Frame` type class instance `frameWp`. -/
+example [inst : Language.IntoVal e v] (P : IProp GF) :
+    P ∗ Φ v ⊢ WP e @ s ; E {{ w, P ∗ Φ w }} := by
+  iintro ⟨HP, HΦ⟩
+  iframe HP
+  iapply wp_value $$ HΦ
+  exact inst
+
 end iframe
 
 section icombine

Iris/tactics.md

@@ -35,7 +35,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `isplitl [`*H₁* ... *Hₙ*`]` — Split a separating conjunction (`∗`); the hypotheses *Hᵢ* go to the left goal, all remaining spatial hypotheses to the right.
 - `isplitr [`*H₁* ... *Hₙ*`]` — Like `isplitl`, but the listed hypotheses go to the right goal.
 - `isplitl` / `isplitr` — Split a separating conjunction, giving *all* spatial hypotheses to the left (`isplitl`) or right (`isplitr`) goal.
-- `iframe` [*selPats*](#selection-patterns) — Cancel the selected hypotheses against matching parts of the goal. Solves the goal completely if the leftover is `True` or `emp` (with affine context).
+- `iframe` [*selPats*](#selection-patterns) — Cancel the selected hypotheses against matching parts of the goal. Solves the goal completely if the leftover is `True` or `emp` (with affine context). One can use `set_option iris.frame.instantiateExists false` to disable the framing of existentially quantified propositions.
 - `iframe` — Equivalent to `iframe ∗` (frame all spatial hypotheses).
 - `icombine` [*selPats*](#selection-patterns) `as` [*casesPat*](#cases-patterns) — Combine the selected hypotheses into one using the `CombineSepAs` type class (defaults to `∗`) and destruct the result with [*casesPat*](#cases-patterns).
 - `icombine` [*selPats*](#selection-patterns) `gives` [*casesPat*](#cases-patterns) — Derive persistent information (e.g. validity of combined ghost state) from the selected hypotheses via `CombineSepGives`, keeping the originals.