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/WeakestPre.lean

@@ -604,28 +604,54 @@ theorem wp_frame_wand {s : Stuckness} {E : CoPset} {e : Expr} {Φ :Val → IProp
 
 end Wp
 
-section ProofModeClasses
+meta section ProofModeClasses
 
-open ProofMode
+open ProofMode Lean Elab Meta Qq
 
 variable {hlc : outParam HasLC}
 variable {Expr State Obs Val : Type _}
 variable [Λ : 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} {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
+theorem frame_wp (p : Bool) (s : Stuckness) (E : CoPset) (e : Expr) (R : IProp GF) (Φ Ψ : Val → IProp GF)
+    (H : ∀ v, Frame 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
+
+@[ipm_tactic_instance Frame _ _ iprop(WP _ @ _ ; _ {{ _ }}) _]
+def frameWp : SynthTactic := fun goalExpr => do
+  let_expr Frame prop bi p R P _ := goalExpr | return .continue
+  have u := goalExpr.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 Wp.wp _ _exprTy val _instA _instWp av coE wpe Φ := P
+  | return .continue
+
+  let ΨTy ← mkArrow val prop
+  let Ψ ← mkFreshExprMVar ΨTy
+
+  let goalTy ← withLocalDeclD `v val fun v => do
+    let body := (mkApp Φ v).headBeta
+    let inner ← mkAppM ``Frame #[p, R, body, mkApp Ψ v]
+    mkForallFVars #[v] inner
+
+  let some H ← withFrameInstantiateExistsDisabled <| synthInstanceRecursive goalTy
+  | return .continue
+
+  let Ψ ← instantiateMVars Ψ
+  let H ← instantiateMVars H
+  let inst ← mkAppM ``frame_wp #[p, av, coE, wpe, R, Φ, Ψ, H]
+  return .success inst
+
+variable {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ Ψ : Val → IProp GF} {P Q R : IProp GF}
 
 @[rocq_alias is_except_0_wp]
 instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where

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
@@ -58,11 +70,6 @@ instance frame_here_pure [BI PROP] {a : Bool} {φ : Prop} {Q : PROP}
     | @TCOr.l _ _ heq => by cases heq; refine h1.1
     | TCOr.r => (affinely_intro .rfl).trans <| affinely_affinelyIf.trans h1.1
 
-@[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
-
 @[ipm_backtrack, rocq_alias frame_affinely]
 instance frame_affinely [BI PROP] p (R P Q Q' : PROP)
     [hor : TCOr (TCEq p true) (QuickAffine R)]
@@ -106,41 +113,6 @@ instance frame_persistently [BI PROP] (R P Q Q' : PROP)
     persistently_sep_mpr.trans <|
     persistently_mono h1.frame
 
-@[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)] :
-    Frame p R iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
-  frame := forall_intro λ a => (sep_mono_right (forall_elim a)).trans (h a).1
-
-@[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
-  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
-
-/-
-You may wonder why this uses [Persistent] and not [QuickPersistent].
-The reason is that [QuickPersistent] is not needed anywhere else, and even without [QuickPersistent],
-this instance avoids quadratic complexity: we usually use the [Quick*] classes to not traverse the
-same term over and over again, but here [P1] is encountered at most once. It is hence not worth adding
-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
-  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
-
 @[ipm_backtrack, rocq_alias frame_later]
 instance frame_later [BI PROP] p (R R' P Q Q' : PROP)
     [h1 : IntoLaterN true 1 R' R] [h2 : Frame p R P Q] [h3 : MakeLaterN 1 Q Q'] :
@@ -183,6 +155,45 @@ instance frame_except_0 [BI PROP] p (R P Q Q' : PROP)
 
 section tactic_theorems
 
+@[rocq_alias frame_wand]
+theorem 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
+
+@[rocq_alias frame_forall]
+theorem frame_forall {α} [BI PROP] p R (Φ Ψ : α → PROP)
+    (h : ∀ a, Frame 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
+
+@[rocq_alias frame_impl_persistent]
+theorem 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
+  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
+
+/-
+You may wonder why this uses [Persistent] and not [QuickPersistent].
+The reason is that [QuickPersistent] is not needed anywhere else, and even without [QuickPersistent],
+this instance avoids quadratic complexity: we usually use the [Quick*] classes to not traverse the
+same term over and over again, but here [P1] is encountered at most once. It is hence not worth adding
+a new typeclass just for this extremely rarely used instance.
+-/
+@[rocq_alias frame_impl]
+theorem 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
+  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
+
 @[rocq_alias maybe_frame_default_persistent]
 theorem maybeFrame_default_persistent [BI PROP] (R P : PROP) :
   Frame true R P P where
@@ -236,10 +247,29 @@ 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 :=
+  return iris.frame.instantiateExists.get (← getOptions)
+
+def withFrameInstantiateExistsDisabled {α} (x : MetaM α) : MetaM α :=
+  withOptions (iris.frame.instantiateExists.set · false) x
 
 /-- corresponds to the MaybeFrame typeclass in Rocq -/
 @[rocq_alias MaybeFrame', rocq_alias maybe_frame_frame]
@@ -353,3 +383,149 @@ 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'
+
+@[ipm_tactic_instance Frame _ _ iprop(_ → _) _]
+def frameImp : 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.imp _ _ P1 P2 := P | return .continue
+
+  -- `frame_here` has higher priority than this instance
+  if ← frameHereApplies bi R P then return .continue
+
+  have P1 : Q($prop) := P1
+  have P2 : Q($prop) := P2
+
+  match matchBool p with
+  | .inl _ =>
+    let Q2 : Q($prop) ← mkFreshExprMVarQ q($prop)
+    let some inst ← withFrameInstantiateExistsDisabled <|
+      synthInstanceRecursiveQ q(Frame true $R $P2 $Q2) | return .continue
+    return .success q(frame_impl_persistent $R $P1 $P2 $Q2 $inst)
+  | .inr _ =>
+    let .some instPers ← trySynthInstanceQ q(Persistent $P1) | return .continue
+    let .some instAbsorb ← trySynthInstanceQ q(QuickAbsorbing $P1) | return .continue
+    let Q2 : Q($prop) ← mkFreshExprMVarQ q($prop)
+    let some inst ← withFrameInstantiateExistsDisabled <|
+      synthInstanceRecursiveQ q(Frame false $R $P2 $Q2) | return .continue
+    return .success q(frame_impl $R $P1 $P2 $Q2 $instPers $instAbsorb $inst)
+
+@[ipm_tactic_instance Frame _ _ iprop(_ -∗ _) _]
+def frameWand : SynthTactic := fun 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.wand _ _ P1 P2 := P.headBeta | return .continue
+
+  -- `frame_here` has higher priority than this instance
+  if ← frameHereApplies bi R P then return .continue
+
+  have P1 : Q($prop) := P1
+  have P2 : Q($prop) := P2
+  let Q2 : Q($prop) ← mkFreshExprMVarQ q($prop)
+  let some h ← withFrameInstantiateExistsDisabled <|
+    synthInstanceRecursiveQ q(Frame $p $R $P2 $Q2) | return .continue
+  return .success q(frame_wand $p $R $P1 $P2 $Q2 $h)
+
+@[ipm_tactic_instance Frame _ _ iprop(∀ _, _) _]
+def frameForall : SynthTactic := fun 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.forall _ _ α Φ := P | return .continue
+
+  -- `frame_here` has higher priority than this instance
+  if ← frameHereApplies bi R P then return .continue
+
+  let .sort v ← inferType α | return .continue
+  have α : Q(Sort v) := α
+  have Φ : Q($α → $prop) := Φ
+
+  let Ψ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
+  let goalTy ← withLocalDeclDQ `a α fun a => do
+    have body : Q($prop) := Expr.headBeta q($Φ $a)
+    mkForallFVars #[a] q(Frame $p $R $body ($Ψ $a))
+
+  let some inst ← withFrameInstantiateExistsDisabled <|
+    synthInstanceRecursive goalTy | return .continue
+  let inst : Q(∀ a, Frame $p $R ($Φ a) ($Ψ a)) := inst
+  return .success q(frame_forall $p $R $Φ $Ψ $inst)
+
+@[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
+
+  let option ← frameInstantiateExistsEnabled
+  if option then
+    -- `iris.frame.instantiateExists` set as `true`
+    let a : Q($α) ← mkFreshExprMVarQ q($α)
+    let G : Q($prop) ← mkFreshExprMVarQ q($prop)
+    have body : Q($prop) := Expr.headBeta q($Φ $a)
+
+    let some inst ← synthInstanceRecursiveQ q(Frame $p $R $body $G)
+    | return .continue
+
+    let a ← instantiateMVars a
+    if !a.hasExprMVar then
+      -- Instantiate the existentially quantified variable with `a`
+      let inst : Q(Frame $p $R ($Φ $a) $G) := inst
+      return .success q(frame_exist $p $R $Φ $a $G $inst)
+    else if a.isMVar then
+      -- For handling inner existential variables
+      let G ← instantiateMVars G
+      let inst ← instantiateMVars inst
+      have Ψ : Q($α → $prop) := .lam bn α (G.abstract #[a]) .default
+      let inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam bn α (inst.abstract #[a]) .default
+      return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $inst)
+    else
+      return .continue
+  else
+    -- `iris.frame.instantiateExists` set as `false`
+    let some ⟨Ψ, inst⟩ ← withLocalDeclDQ bn α fun a => do
+      let G : Q($prop) ← mkFreshExprMVarQ q($prop)
+      have body : Q($prop) := Expr.headBeta q($Φ $a)
+      let some inst ← synthInstanceRecursiveQ q(Frame $p $R $body $G)
+      | return none
+      let G ← instantiateMVars G
+      let inst ← instantiateMVars inst
+      return some (← mkLambdaFVars #[a] G, ← mkLambdaFVars #[a] inst)
+    | return .continue
+
+    have Ψ : Q($α → $prop) := Ψ
+    let inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := inst
+    return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $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"