From 62e0fce6b3a3a4e61ca8665e98901ac0b8c28807 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 13:26:22 +0200 Subject: [PATCH 01/29] Create `frameExist` as a type class instance --- Iris/Iris/ProofMode/InstancesFrame.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 066accaa6..f8f4c330b 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -353,3 +353,7 @@ def frameOr : SynthTactic := λ e => do throwError "MakeOr should always succeed" return .success q(frame_or $p $R $P1 $P2 $Q1 $Q2 $Q') return .continue + +@[ipm_tactic_instance Frame _ _ iprop(∃ _, _) _] +def frameExist : SynthTactic := λ e => do + return .continue From 303b7e7297e3c7daf00ccc40c8f596d2f361d5c0 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 13:33:52 +0200 Subject: [PATCH 02/29] Perform parsing in `frameExist` --- Iris/Iris/ProofMode/InstancesFrame.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index f8f4c330b..58a004975 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -239,7 +239,7 @@ theorem frame_or [BI PROP] p (R P1 P2 Q1 Q2 Q' : PROP) end tactic_theorems meta section tactics -open Lean +open Lean Elab Meta Std /-- corresponds to the MaybeFrame typeclass in Rocq -/ @[rocq_alias MaybeFrame', rocq_alias maybe_frame_frame] @@ -356,4 +356,16 @@ def frameOr : SynthTactic := λ e => do @[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) := Φ + return .continue From 897e5d2ebc824d6d6156d4e574112841a49c1c28 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 13:43:11 +0200 Subject: [PATCH 03/29] Introduce `frame_exist`, use it in `frameExist` --- Iris/Iris/ProofMode/InstancesFrame.lean | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 58a004975..29fc38f5f 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -236,6 +236,12 @@ 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(∃ x, Φ x) Q where + frame := inst.frame.trans <| exists_intro a + end tactic_theorems meta section tactics @@ -368,4 +374,17 @@ def frameExist : SynthTactic := λ e => do have α : Q(Sort v) := α have Φ : Q($α → $prop) := Φ - return .continue + 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 + have w : Q($α) := a' + have inst : Q(Frame $p $R ($Φ $w) $G) := inst + return .success q(frame_exist $p $R $Φ $w $G $inst) + else + return .continue From 0f957aed0e338464a856f059b36ec4cb01aa7f73 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 13:55:42 +0200 Subject: [PATCH 04/29] First functioning version of `frameExist` --- Iris/Iris/ProofMode/InstancesFrame.lean | 4 ++-- Iris/Iris/Tests/Tactics.lean | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 29fc38f5f..e7c89ee50 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -381,9 +381,9 @@ def frameExist : SynthTactic := λ e => do let some inst ← synthInstanceRecursiveQ q(Frame $p $R $body $G) | return .continue - let a' ← instantiateMVars a + let a ← instantiateMVars a if !a.hasExprMVar then - have w : Q($α) := a' + have w : Q($α) := a have inst : Q(Frame $p $R ($Φ $w) $G) := inst return .success q(frame_exist $p $R $Φ $w $G $inst) else diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index fb8509a5f..e1ab7768c 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2384,6 +2384,12 @@ 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) : + ⊢ P a -∗ Q -∗ R b -∗ (∃ x, P x) ∗ Q ∗ (∃ x, R x) := by + iintro HP HQ HR + iframe + end iframe section icombine From 0645c20ee62742790d718745d31c54b3e3cf12f5 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 14:35:54 +0200 Subject: [PATCH 05/29] Port `frame_exist_no_instantiate` --- Iris/Iris/ProofMode/InstancesFrame.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index e7c89ee50..9693c0fed 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -242,6 +242,13 @@ theorem frame_exist [BI PROP] {α} (p : Bool) (R : PROP) (Φ : α → PROP) Frame p R iprop(∃ x, Φ x) 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(∃ x, Φ x) iprop(∃ x, Ψ x) where + frame := sep_exists_left.mp.trans <| + exists_elim <| fun a => (inst a).frame.trans <| exists_intro a + end tactic_theorems meta section tactics @@ -376,15 +383,14 @@ def frameExist : SynthTactic := λ e => do 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 - have w : Q($α) := a - have inst : Q(Frame $p $R ($Φ $w) $G) := inst - return .success q(frame_exist $p $R $Φ $w $G $inst) + have inst : Q(Frame $p $R ($Φ $a) $G) := inst + return .success q(frame_exist $p $R $Φ $a $G $inst) else return .continue From 15ac9bc25175ab8543f38cc30bcd443056b30bf9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 14:53:00 +0200 Subject: [PATCH 06/29] Handle inner existential variables --- Iris/Iris/ProofMode/InstancesFrame.lean | 8 ++++++++ Iris/Iris/Tests/Tactics.lean | 22 ++++++++++++++++++---- 2 files changed, 26 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 9693c0fed..ff8ced830 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -390,7 +390,15 @@ def frameExist : SynthTactic := λ e => do let a ← instantiateMVars a if !a.hasExprMVar then + -- Instantiate the existentially quantified variable with `a` have 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 `a α (G.abstract #[a]) .default + have hAll : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam `a α (inst.abstract #[a]) .default + return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $hAll) else return .continue diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index e1ab7768c..17699fb46 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2385,10 +2385,24 @@ example [BI PROP] [BIAffine PROP] (Q : Nat → PROP) : (Q 0 ⊢ ∃ x, False ∨ iframe /- Tests `iframe` with existential quantifiers -/ -example [BI PROP] {α} {β} (a : α) (b : β) (P : α → PROP) (Q : PROP) (R : β → PROP) : - ⊢ P a -∗ Q -∗ R b -∗ (∃ x, P x) ∗ Q ∗ (∃ x, R x) := by - iintro HP HQ HR - iframe +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 end iframe From 583f87a9a0986e39861f6fd17d63ef8456e4dcc9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 15:00:04 +0200 Subject: [PATCH 07/29] Add one more test --- Iris/Iris/Tests/Tactics.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 17699fb46..d18190bfb 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2404,6 +2404,12 @@ example [BI PROP] {α} (a : α) {β} (b : β) (P : PROP) iintro HP HQ HR HS iframe HS HP HR HQ +/- Tests `iframe` with existential quantifers in various orders -/ +example [BI PROP] {α} (a : α) {β} (b : β) (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 + end iframe section icombine From bb40d716949174da72239a2943877f3eb27b8b9e Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 15:20:01 +0200 Subject: [PATCH 08/29] Reuse the binder name --- Iris/Iris/ProofMode/InstancesFrame.lean | 11 +++++++---- Iris/Iris/Tests/Tactics.lean | 3 ++- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index ff8ced830..7d4c3fc0b 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -239,13 +239,13 @@ theorem frame_or [BI PROP] p (R P1 P2 Q1 Q2 Q' : PROP) @[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(∃ x, Φ x) Q where + 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(∃ x, Φ x) iprop(∃ x, Ψ x) where + 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 @@ -381,6 +381,9 @@ def frameExist : SynthTactic := λ e => do 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 a : Q($α) ← mkFreshExprMVarQ q($α) let G : Q($prop) ← mkFreshExprMVarQ q($prop) have body : Q($prop) := Expr.headBeta q($Φ $a) @@ -397,8 +400,8 @@ def frameExist : SynthTactic := λ e => do -- For handling inner existential variables let G ← instantiateMVars G let inst ← instantiateMVars inst - have Ψ : Q($α → $prop) := .lam `a α (G.abstract #[a]) .default - have hAll : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam `a α (inst.abstract #[a]) .default + have Ψ : Q($α → $prop) := .lam bn α (G.abstract #[a]) .default + have hAll : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam bn α (inst.abstract #[a]) .default return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $hAll) else return .continue diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index d18190bfb..a08890d46 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2405,7 +2405,8 @@ example [BI PROP] {α} (a : α) {β} (b : β) (P : PROP) iframe HS HP HR HQ /- Tests `iframe` with existential quantifers in various orders -/ -example [BI PROP] {α} (a : α) {β} (b : β) (P : α → β → PROP) (Q : β → α → γ → PROP) : +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 From 67047d5cd79b0d3748e16d1ad386346e9d0bb559 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 15:32:33 +0200 Subject: [PATCH 09/29] Add an option `iris.frame.instantiateExists` for disabling existential quantifiers framing --- Iris/Iris/ProofMode/InstancesFrame.lean | 17 +++++++++++++++++ Iris/Iris/Tests/Tactics.lean | 9 +++++++++ 2 files changed, 26 insertions(+) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 7d4c3fc0b..03f38ad4c 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -11,6 +11,17 @@ 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 restore the old\ + behaviour of framing below existentials without instantiating them." +} + +end + @[expose] public section namespace Iris.ProofMode @@ -254,6 +265,12 @@ end tactic_theorems meta section tactics 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] def maybeFrame {prop : Q(Type u)} {bi : Q(BI $prop)} (p : Q(Bool)) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index a08890d46..8160fd426 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2411,6 +2411,15 @@ example [BI PROP] {α} (a : α) {β} (b : β) {γ} (c : γ) iintro HP HQ iframe +/- Tests `iframe` with the framing of existential quantifiers disabled -/ +set_option iris.frame.instantiateExists false in +example [BI PROP] {α} (a : α) (P : PROP) (Q : α → PROP) : + ⊢ P -∗ Q a -∗ ∃ n, P ∗ Q n := by + iintro HP HQ + iframe + iexists a + iassumption + end iframe section icombine From e5ec8ec4124bc5a31c96c1e003547ee2888a8959 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 15:48:15 +0200 Subject: [PATCH 10/29] Handle the flag `iris.frame.instantiateExists` in `frameExist` --- Iris/Iris/ProofMode/InstancesFrame.lean | 58 ++++++++++++++++--------- Iris/Iris/Tests/Tactics.lean | 28 +++++++++--- 2 files changed, 61 insertions(+), 25 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 03f38ad4c..36ec7041f 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -401,24 +401,42 @@ def frameExist : SynthTactic := λ e => do -- Find the binder name so that it can be reused after framing let bn := match Φ with | .lam n .. => n | _ => `x - 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` - have 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 - have hAll : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam bn α (inst.abstract #[a]) .default - return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $hAll) + 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` + have 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 + have 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 - return .continue + -- `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) := Ψ + have inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := inst + return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $inst) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 8160fd426..1c9cf1bd9 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2411,15 +2411,33 @@ example [BI PROP] {α} (a : α) {β} (b : β) {γ} (c : γ) iintro HP HQ iframe -/- Tests `iframe` with the framing of existential quantifiers disabled -/ +/- + 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 : α → PROP) : - ⊢ P -∗ Q a -∗ ∃ n, P ∗ Q n := by - iintro HP HQ - iframe +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 + end iframe section icombine From 7eed7f8455cf307794a3253cfd9f506ab2ad9cfd Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 16:12:43 +0200 Subject: [PATCH 11/29] Implement `frameImp`, `frameWand` and `frameForall` as `SynthTactic` Necessary for using `withFrameInstantiateExistsDisabled` --- Iris/Iris/ProofMode/InstancesFrame.lean | 153 +++++++++++++++++------- Iris/Iris/Tests/Tactics.lean | 7 ++ 2 files changed, 117 insertions(+), 43 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 36ec7041f..6ba9c6eef 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -69,11 +69,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)] @@ -117,41 +112,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'] : @@ -194,6 +154,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 @@ -384,6 +383,74 @@ def frameOr : SynthTactic := λ e => do return .success q(frame_or $p $R $P1 $P2 $Q1 $Q2 $Q') return .continue +@[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 + + 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 + + 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 + + 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 @@ -414,14 +481,14 @@ def frameExist : SynthTactic := λ e => do let a ← instantiateMVars a if !a.hasExprMVar then -- Instantiate the existentially quantified variable with `a` - have inst : Q(Frame $p $R ($Φ $a) $G) := inst + 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 - have inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := .lam bn α (inst.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 @@ -438,5 +505,5 @@ def frameExist : SynthTactic := λ e => do | return .continue have Ψ : Q($α → $prop) := Ψ - have inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := inst + let inst : Q(∀ x, Frame $p $R ($Φ x) ($Ψ x)) := inst return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $inst) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 1c9cf1bd9..f48058d83 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2438,6 +2438,13 @@ example [BI PROP] {α} (a : α) (P : α → PROP) : iintro HP iframe HP +example [BI PROP] (P : PROP) : P ⊢ ∀ (x : Nat), ∃ n, ⌜n = x⌝ ∗ P := by + iintro HP + iframe HP + iintro %x + iexists x + ipureintro; rfl + end iframe section icombine From 6fbeb90b0d78bb259c763d1692e2822cd8efb5c3 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 16:32:27 +0200 Subject: [PATCH 12/29] Add `rocq_ignore` annotations --- Iris/Iris/ProofMode/InstancesFrame.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 6ba9c6eef..30e297efb 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -507,3 +507,10 @@ def frameExist : SynthTactic := λ e => do 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 FrameExistRequirements "Rocq-specific telescope infrastructure not needed in the Lean metaprogram" +#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" From c97962e5e27d8b9c72b68333cbc4afa971d1ea89 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 16:48:51 +0200 Subject: [PATCH 13/29] Update documentation --- Iris/Iris/ProofMode/Porting.lean | 2 +- Iris/tactics.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index dad0da8f9..1974953c4 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/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" diff --git a/Iris/tactics.md b/Iris/tactics.md index f9e465ec0..4d23c1723 100644 --- a/Iris/tactics.md +++ b/Iris/tactics.md @@ -33,7 +33,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. From 3c5f102b14e06949bfd7498ac77e54a14b0af3b1 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 16:50:10 +0200 Subject: [PATCH 14/29] Update proof due to changes in `iframe` --- Iris/Iris/Instances/Lib/Invariants.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Iris/Iris/Instances/Lib/Invariants.lean b/Iris/Iris/Instances/Lib/Invariants.lean index 66c14409a..bfc2acc46 100644 --- a/Iris/Iris/Instances/Lib/Invariants.lean +++ b/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] From e4e43c69a2104aa2ea8fe2fd489f54a0d56583ba Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 17:14:53 +0200 Subject: [PATCH 15/29] Bug fix: `frameImp`, `frameWand` and `frameForall` has lower priority --- Iris/Iris/ProofMode/InstancesFrame.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 30e297efb..bde6d9d94 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -383,6 +383,12 @@ def frameOr : SynthTactic := λ e => do 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 @@ -393,6 +399,9 @@ def frameImp : SynthTactic := λ e => do 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 @@ -420,6 +429,9 @@ def frameWand : SynthTactic := fun e => do 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) @@ -437,6 +449,9 @@ def frameForall : SynthTactic := fun e => do 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) := Φ From 6bcee85aaccaabd0cd55ade7f38c6cd3978a60f2 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 17:27:13 +0200 Subject: [PATCH 16/29] Minor refinements --- Iris/Iris/ProofMode/InstancesFrame.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index bde6d9d94..3f9809f76 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -16,8 +16,9 @@ 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 restore the old\ - behaviour of framing below existentials without instantiating them." + quantifiers in the goal while framing. Set to `false` to allow framing \ + below existential quantifiers without instantiating any existentially \ + quantified variables." } end From 0c58c915614400a17e29d9fbd6cd9afbcf6113d1 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 17:52:55 +0200 Subject: [PATCH 17/29] Port `FrameInstantiateExistDisabled` for `frameWp` (#400) --- Iris/Iris/ProgramLogic/WeakestPre.lean | 44 ++++++++++++++++++++------ Iris/Iris/Tests/Tactics.lean | 18 ++++++++++- 2 files changed, 52 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index 6ad568c26..2dbf0dd8d 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -604,9 +604,9 @@ 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 _} @@ -614,18 +614,44 @@ 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 diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index f48058d83..02b494a96 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/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. -/ @@ -2438,6 +2440,7 @@ example [BI PROP] {α} (a : α) (P : α → PROP) : 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 @@ -2445,6 +2448,19 @@ example [BI PROP] (P : PROP) : P ⊢ ∀ (x : Nat), ∃ n, ⌜n = x⌝ ∗ P := iexists x ipureintro; rfl +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 From 181b00f33c1b415240a1c3469af5d45d229516b3 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 20:40:46 +0200 Subject: [PATCH 18/29] Header update --- Iris/Iris/ProofMode/InstancesFrame.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 3f9809f76..c56c0a374 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/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 From a7f55d86d42c37aa57723d368acb480620ddaab5 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 12 Jul 2026 20:51:19 +0200 Subject: [PATCH 19/29] Remove stale `rocq_ignore` entry (`FrameExistRequirements`) --- Iris/Iris/ProofMode/InstancesFrame.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index c56c0a374..7277b3e33 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -525,7 +525,6 @@ def frameExist : SynthTactic := λ e => do return .success q(frame_exist_no_instantiate $p $R $Φ $Ψ $inst) #rocq_ignore frame_exist_helper "Logic already handled in the metaprogram frameExist" -#rocq_ignore FrameExistRequirements "Rocq-specific telescope infrastructure not needed in the Lean metaprogram" #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" From 2fa1f0ac3659abbf42d9b41e9d4a91ca23034b97 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:03:10 +0200 Subject: [PATCH 20/29] Introduce `FrameInstantiateExistDisabled` as its own type class --- Iris/Iris/ProgramLogic/WeakestPre.lean | 37 +---- Iris/Iris/ProofMode/InstancesFrame.lean | 181 +++++++++--------------- 2 files changed, 68 insertions(+), 150 deletions(-) diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index 2dbf0dd8d..d27d6ac7c 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -614,44 +614,15 @@ 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] -theorem frame_wp (p : Bool) (s : Stuckness) (E : CoPset) (e : Expr) (R : IProp GF) (Φ Ψ : Val → IProp GF) - (H : ∀ v, Frame p R (Φ v) (Ψ v)) : +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 => (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} + exact fun v => sorry --frame @[rocq_alias is_except_0_wp] instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 7277b3e33..f4873c0db 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -28,6 +28,11 @@ end namespace Iris.ProofMode open Qq Iris.BI Iris.Std +@[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) + /- When framing [R] against itself, we leave [True] if possible since it is a weaker goal. Otherwise we leave [emp]. Only if all those options fail, we start decomposing [R]. @@ -84,6 +89,12 @@ instance frame_affinely [BI PROP] p (R P Q Q' : PROP) affinely_sep_mpr.trans <| affinely_mono h1.frame +@[ipm_backtrack, rocq_alias frame_wand] +instance frame_wand [BI PROP] p (R P1 P2 Q2 : PROP) + [h : FrameInstantiateExistDisabled p R P2 Q2] : + Frame p R iprop(P1 -∗ P2) iprop(P1 -∗ Q2) where + frame := sorry--h.frame + @[ipm_backtrack, rocq_alias frame_intuitionistically] instance frame_intuitionistically [BI PROP] (R P Q Q' : PROP) [h1 : Frame true R P Q] [h2 : MakeIntuitionistically Q Q'] : @@ -113,6 +124,42 @@ 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) + [h : ∀ a, FrameInstantiateExistDisabled p R (Φ a) (Ψ a)] : + Frame p R iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where + frame := sorry -- (h a).1 + +@[ipm_backtrack, rocq_alias frame_impl_persistent] +instance frame_impl_persistent [BI PROP] (R P1 P2 Q2 : PROP) + [h : FrameInstantiateExistDisabled true R P2 Q2] : + Frame true R iprop(P1 → P2) iprop(P1 → Q2) where + frame := sorry + -- have : Absorbing P1 := ha.quick_absorbing + -- 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 : FrameInstantiateExistDisabled false R P2 Q2] : Frame false R iprop(P1 → P2) iprop(P1 → Q2) where + frame := sorry + -- 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'] : @@ -155,45 +202,6 @@ 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 @@ -265,11 +273,27 @@ end tactic_theorems meta section tactics open Lean Elab Meta Std -def frameInstantiateExistsEnabled : MetaM Bool := +def frameInstantiateExistsEnabled : MetaM Bool := do return iris.frame.instantiateExists.get (← getOptions) def withFrameInstantiateExistsDisabled {α} (x : MetaM α) : MetaM α := withOptions (iris.frame.instantiateExists.set · false) x +theorem frameNoInstantiateExist_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(frameNoInstantiateExist_of $inst) /-- corresponds to the MaybeFrame typeclass in Rocq -/ @[rocq_alias MaybeFrame', rocq_alias maybe_frame_frame] @@ -390,83 +414,6 @@ def frameHereApplies {u : Level} {prop : Q(Type u)} (_bi : Q(BI $prop)) (R P : Q 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 From 440a4a7a95c653d7232f70adf535d305385c328e Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:07:55 +0200 Subject: [PATCH 21/29] Restore the proofs for `Frame` instances --- Iris/Iris/ProgramLogic/WeakestPre.lean | 2 +- Iris/Iris/ProofMode/InstancesFrame.lean | 32 +++++++++++++------------ 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index d27d6ac7c..cb56901ec 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -622,7 +622,7 @@ instance frameWp {p : Bool} [H : ∀ v, FrameInstantiateExistDisabled p R (Φ v) frame := by refine wp_frame_l.trans ?_ apply wp_mono - exact fun v => sorry --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 diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index f4873c0db..3a74a4eb1 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -93,7 +93,8 @@ instance frame_affinely [BI PROP] p (R P Q Q' : PROP) instance frame_wand [BI PROP] p (R P1 P2 Q2 : PROP) [h : FrameInstantiateExistDisabled p R P2 Q2] : Frame p R iprop(P1 -∗ P2) iprop(P1 -∗ Q2) where - frame := sorry--h.frame + 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_intuitionistically] instance frame_intuitionistically [BI PROP] (R P Q Q' : PROP) @@ -128,19 +129,19 @@ instance frame_persistently [BI PROP] (R P Q Q' : PROP) instance frame_forall {α} [BI PROP] p R (Φ Ψ : α → PROP) [h : ∀ a, FrameInstantiateExistDisabled p R (Φ a) (Ψ a)] : Frame p R iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where - frame := sorry -- (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 : FrameInstantiateExistDisabled true R P2 Q2] : Frame true R iprop(P1 → P2) iprop(P1 → Q2) where - frame := sorry - -- have : Absorbing P1 := ha.quick_absorbing - -- 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 + 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_instantiatiate_exist_disabled.frame /- You may wonder why this uses [Persistent] and not [QuickPersistent]. @@ -153,12 +154,13 @@ a new typeclass just for this extremely rarely used instance. instance frame_impl [BI PROP] (R P1 P2 Q2 : PROP) [hp : Persistent P1] [ha : QuickAbsorbing P1] [h : FrameInstantiateExistDisabled false R P2 Q2] : Frame false R iprop(P1 → P2) iprop(P1 → Q2) where - frame := sorry - -- 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 + 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_instantiatiate_exist_disabled.frame @[ipm_backtrack, rocq_alias frame_later] instance frame_later [BI PROP] p (R R' P Q Q' : PROP) From 737c8d75e9234d869fd72af63a913bfb944d7131 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:09:54 +0200 Subject: [PATCH 22/29] Restore position of instance --- Iris/Iris/ProofMode/InstancesFrame.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 3a74a4eb1..3dbb3b4e3 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -75,6 +75,13 @@ 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 : 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) [hor : TCOr (TCEq p true) (QuickAffine R)] @@ -89,13 +96,6 @@ instance frame_affinely [BI PROP] p (R P Q Q' : PROP) affinely_sep_mpr.trans <| affinely_mono h1.frame -@[ipm_backtrack, rocq_alias frame_wand] -instance frame_wand [BI PROP] p (R P1 P2 Q2 : PROP) - [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_intuitionistically] instance frame_intuitionistically [BI PROP] (R P Q Q' : PROP) [h1 : Frame true R P Q] [h2 : MakeIntuitionistically Q Q'] : @@ -280,7 +280,8 @@ def frameInstantiateExistsEnabled : MetaM Bool := do def withFrameInstantiateExistsDisabled {α} (x : MetaM α) : MetaM α := withOptions (iris.frame.instantiateExists.set · false) x -theorem frameNoInstantiateExist_of [BI PROP] {p} {R P Q : PROP} (h : Frame p R P Q) : + +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 _ _ _ _] @@ -295,7 +296,7 @@ def frameNoInstantiateExist : SynthTactic := λ e => do have G : Q($prop) := G let some inst ← withFrameInstantiateExistsDisabled <| synthInstanceRecursiveQ q(Frame $p $R $P $G) | return .continue - return .success q(frameNoInstantiateExist_of $inst) + return .success q(frameInstantiateExistsDisabled_of $inst) /-- corresponds to the MaybeFrame typeclass in Rocq -/ @[rocq_alias MaybeFrame', rocq_alias maybe_frame_frame] From c6365b06187034f7e2199f4fb4306671d8f2fdbf Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:12:26 +0200 Subject: [PATCH 23/29] Update `AbstractLangCompleteness.lean` --- Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean index 90f9fb07c..b87d7a3ff 100644 --- a/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean +++ b/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⟩) From 14d4bf4d83be63e9df1124de239d56eece5934d6 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:14:49 +0200 Subject: [PATCH 24/29] Remove unnecessary imports --- Iris/Iris/ProgramLogic/WeakestPre.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index 3f454b16c..941fa31a0 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -604,9 +604,9 @@ theorem wp_frame_wand {s : Stuckness} {E : CoPset} {e : Expr} {Φ :Val → IProp end Wp -meta section ProofModeClasses +section ProofModeClasses -open ProofMode Lean Elab Meta Qq +open ProofMode variable {hlc : outParam HasLC} variable {Expr State Obs Val : Type _} From 8dfca0a21da2d35eb515f5282ec3deb3d728b302 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 11:17:02 +0200 Subject: [PATCH 25/29] Move `FrameInstantiateExistDisabled` to `Classes.lean` --- Iris/Iris/ProofMode/Classes.lean | 5 +++++ Iris/Iris/ProofMode/InstancesFrame.lean | 5 ----- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index a6227a704..361d5e33c 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/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 diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 3dbb3b4e3..367dd167e 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -28,11 +28,6 @@ end namespace Iris.ProofMode open Qq Iris.BI Iris.Std -@[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) - /- When framing [R] against itself, we leave [True] if possible since it is a weaker goal. Otherwise we leave [emp]. Only if all those options fail, we start decomposing [R]. From 142a286cb86e24d475cc2617b1ea3e1d245ae58b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 16:28:58 +0200 Subject: [PATCH 26/29] Implement `solveGatherEvarsEq` and fix bug in `iframe` --- Iris/Iris/ProofMode/InstancesFrame.lean | 58 ++++++++++++++++--------- Iris/Iris/Tests/Tactics.lean | 24 ++++++++++ 2 files changed, 62 insertions(+), 20 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 367dd167e..46d288893 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -412,6 +412,22 @@ def frameHereApplies {u : Level} {prop : Q(Type u)} (_bi : Q(BI $prop)) (R P : Q 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 + 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 @@ -431,30 +447,32 @@ def frameExist : SynthTactic := λ e => do 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) + -- Framing of existential quantifiers *enabled* + let some ⟨a, X, inst⟩ ← withLocalDeclDQ bn α fun c => do + let a ← mkFreshExprMVarQ q($α) + 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 + if ← 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 + return some (some a, G, ← instantiateMVars inst) | return .continue - - let a ← instantiateMVars a - if !a.hasExprMVar then - -- Instantiate the existentially quantified variable with `a` + 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) - 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` + -- Framing of existential quantifiers *disabled* let some ⟨Ψ, inst⟩ ← withLocalDeclDQ bn α fun a => do let G : Q($prop) ← mkFreshExprMVarQ q($prop) have body : Q($prop) := Expr.headBeta q($Φ $a) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 20bc27afb..bbaec7e4e 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2531,6 +2531,30 @@ example [BI PROP] (P : PROP) : P ⊢ ∀ (x : Nat), ∃ n, ⌜n = x⌝ ∗ P := 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] From b9f5c057a1cf1a818cee09415950373db8c2956b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 16:48:02 +0200 Subject: [PATCH 27/29] Add comments --- Iris/Iris/ProofMode/InstancesFrame.lean | 66 +++++++++++-------------- 1 file changed, 28 insertions(+), 38 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 46d288893..41857618e 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -418,6 +418,7 @@ def solveGatherEvarsEq (a c : Expr) : MetaM Bool := do | .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 @@ -445,47 +446,36 @@ def frameExist : SynthTactic := λ e => do -- 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 - -- Framing of existential quantifiers *enabled* - let some ⟨a, X, inst⟩ ← withLocalDeclDQ bn α fun c => do - let a ← mkFreshExprMVarQ q($α) - 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 - if ← 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 - 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) - else - -- Framing of existential quantifiers *disabled* - 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 + -- 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 - have Ψ : Q($α → $prop) := Ψ + 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" From 0f9968b4ed71818ae27a031e61addbed0b0e0f29 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Mon, 27 Jul 2026 15:58:29 +0200 Subject: [PATCH 28/29] simplify code --- Iris/Iris/ProofMode/InstancesFrame.lean | 47 +++++-------------------- Iris/Iris/Tests/Tactics.lean | 17 +++++++++ 2 files changed, 26 insertions(+), 38 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index 41857618e..ceb3a3770 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -406,29 +406,6 @@ def frameOr : SynthTactic := λ e => do 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 @@ -444,26 +421,22 @@ def frameExist : SynthTactic := λ e => do have Φ : Q($α → $prop) := Φ -- Find the binder name so that it can be reused after framing - let bn := match Φ with | .lam n .. => n | _ => `x + let .lam bn _ _ bi := Φ | throwError "iframe: argument to BI.exists must be a lambda" -- 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 some ⟨a, X, inst⟩ ← withLocalDeclQ bn bi α 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 + -- If `a` is defEq to `c`, the existential quantifier remains. This can be either since the framing + -- did not instantiate the existential quantifer or since the instiation of existentials was disabled. + if ← withTransparency .none <| isDefEq (← 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) + else + -- The existential quantifier does not remain as the existential variable is instantiated + return some (some <| ← instantiateMVars a, ← instantiateMVars G, ← instantiateMVars inst) | return .continue match a with @@ -480,5 +453,3 @@ def frameExist : SynthTactic := λ e => do #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" diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 1df9ebaaa..cfc94ffc7 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2515,6 +2515,23 @@ example [BI PROP] {α} (a : α) {β} (b : β) (P : PROP) iintro HP HQ HR HS iframe HS HP HR HQ +/- Tests `iframe` with multiple existential quantifiers framed at once -/ +/-- +error: unsolved goals +PROP : Type u_1 +inst✝ : BI PROP +α : Sort u_2 +P : PROP +Q : α → PROP +⊢ ⏎ + ⊢ «exists» fun {n} => Q n +-/ +#guard_msgs in +example [BI PROP] {α} (P : PROP) (Q : α → PROP) : + ⊢ P -∗ BI.exists fun {n} => iprop(Q n ∗ P) := by + iintro HP + iframe HP + /- Tests `iframe` with existential quantifers in various orders -/ example [BI PROP] {α} (a : α) {β} (b : β) {γ} (c : γ) (P : α → β → PROP) (Q : β → α → γ → PROP) : From 6878531a1932897041804aafdee945fb5f0b9967 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Mon, 27 Jul 2026 16:07:48 +0200 Subject: [PATCH 29/29] fix --- Iris/Iris/ProofMode/InstancesFrame.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index ceb3a3770..f239bd004 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -431,11 +431,12 @@ def frameExist : SynthTactic := λ e => do let some inst ← synthInstanceRecursiveQ q(Frame $p $R $body $G) | return none -- If `a` is defEq to `c`, the existential quantifier remains. This can be either since the framing -- did not instantiate the existential quantifer or since the instiation of existentials was disabled. - if ← withTransparency .none <| isDefEq (← instantiateMVars a) c then + -- The `withConfig` is necessary to disable stuck defEq exceptions. + if ← withTransparency .none <| withConfig (λ _ => {}) (isDefEq (← instantiateMVars a) c) then return some (none, ← mkLambdaFVars #[c] (← instantiateMVars G), ← mkLambdaFVars #[c] (← instantiateMVars inst)) else - -- The existential quantifier does not remain as the existential variable is instantiated + -- The existential quantifier does not remain as the existential variable is instantiated. return some (some <| ← instantiateMVars a, ← instantiateMVars G, ← instantiateMVars inst) | return .continue