From e9113b8bc4e2ca474d8b7b1c3c0c6082b722c4d8 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 30 Jun 2026 17:35:52 +0200 Subject: [PATCH 01/53] Specify `u`, `prop` and `bi` in `iCasesCore` as implicit arguments So that `bi` does not have to be an argument when `iCasesCore` is used --- Iris/Iris/ProofMode/Tactics/Cases.lean | 7 ++++--- Iris/Iris/ProofMode/Tactics/Combine.lean | 6 +++--- Iris/Iris/ProofMode/Tactics/Have.lean | 4 ++-- Iris/Iris/ProofMode/Tactics/Intro.lean | 8 ++++---- 4 files changed, 13 insertions(+), 12 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 9f5ec3854..018a288dd 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -195,7 +195,8 @@ possibly an updated goal. ## Returns A proof of `hyps ∗ □?p A ⊢ goal`. -/ -partial def iCasesCore {P} (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat) +partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} + (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat) (p : Q(Bool)) (A : Q($prop)) (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal') := addBIGoal) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := @@ -262,7 +263,7 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t -- parse syntax let pmt ← liftMacroM <| PMTerm.parse pmt let pat ← liftMacroM <| iCasesPat.parse pat - ProofModeM.runTactic λ mvar { bi, goal, hyps, .. } => do + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do -- We keep the persistent hypothesis if it is required by the user (+keep is set by ihave) -- or if we perform specialization @@ -270,7 +271,7 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t (try_dup_context := pat.should_try_dup_context) -- process pattern - let pf2 ← iCasesCore bi hyps goal pat p A + let pf2 ← iCasesCore hyps goal pat p A mvar.assign q(($pf).trans $pf2) diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index 1b5cca40b..ec5635610 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -228,7 +228,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* let hs ← iCombineParseSelPats hyps patSels let st ← iCombineCore hs hyps goal - let pf ← iCasesCore _ st.newHyps goal pat q($(st.p)) st.outAs addBIGoal + let pf ← iCasesCore st.newHyps goal pat q($(st.p)) st.outAs addBIGoal mvar.assign q($(st.pfAs).trans $pf) /-- @@ -250,7 +250,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* match st.outGives, st.pfGives with | some outGives, pfGives => - let pf ← iCasesCore _ hyps goal pat q(true) outGives addBIGoal + let pf ← iCasesCore hyps goal pat q(true) outGives addBIGoal mvar.assign q($(pfGives).trans $pf) | none, _ => throwNoInstanceForGives @@ -279,7 +279,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* match st.outGives, st.pfGives with | some outGives, pfGives => - let pf ← iCasesCore _ st.newHyps goal (.conjunction [pat1, .intuitionistic pat2]) + let pf ← iCasesCore st.newHyps goal (.conjunction [pat1, .intuitionistic pat2]) q($st.p) q(iprop($st.outAs ∗ □ $outGives)) addBIGoal mvar.assign q(combine_as_gives $st.pfAs $pfGives $pf) | none, _ => throwNoInstanceForGives diff --git a/Iris/Iris/ProofMode/Tactics/Have.lean b/Iris/Iris/ProofMode/Tactics/Have.lean index 3c97cd888..abe101fdf 100644 --- a/Iris/Iris/ProofMode/Tactics/Have.lean +++ b/Iris/Iris/ProofMode/Tactics/Have.lean @@ -36,9 +36,9 @@ macro "ihave " colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icas elab "ihave " colGt pat:icasesPat " : " P:term " $$ " spat:specPat : tactic => do let spat ← liftMacroM <| SpecPat.parse spat let pat ← liftMacroM <| iCasesPat.parse pat - ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do + ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do let P ← elabTermEnsuringTypeQ (← `(iprop($P))) prop -- establish `P` with `spat` let ⟨_, hyps', p, A, pf⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) [spat] (try_dup_context := pat.should_try_dup_context) - let pf2 ← iCasesCore bi hyps' goal pat p A + let pf2 ← iCasesCore hyps' goal pat p A mvar.assign q(ihave_assert (($pf).trans $pf2)) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index f6cf3fd62..e7cc2cb22 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -103,7 +103,7 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} | .intuitionistic pat, some _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) | throwError "iintro: {A1} not persistent" - let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats k) + let pf ← iCasesCore hyps A2 pat q(true) B (iIntroCore · · pats k) return q(imp_intro_intuitionistic (Q := $Q) $pf) | .intuitionistic pat, none => let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) @@ -112,19 +112,19 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} | throwError "iintro: {A1} not persistent" let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2)) | throwError "iintro: {A1} not affine and the goal not absorbing" - let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats k) + let pf ← iCasesCore hyps A2 pat q(true) B (iIntroCore · · pats k) return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf) | _, some _ => -- should always succeed let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1) let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) | throwError "iintro: {A1} is not persistent and spatial context is non-empty" - let pf ← iCasesCore bi hyps A2 pat q(false) B (iIntroCore · · pats k) + let pf ← iCasesCore hyps A2 pat q(false) B (iIntroCore · · pats k) return q(imp_intro_spatial (Q := $Q) $pf) | _, none => let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) | throwError "iintro: {Q} not a wand" - let pf ← iCasesCore bi hyps A2 pat q(false) A1 (iIntroCore · · pats k) + let pf ← iCasesCore hyps A2 pat q(false) A1 (iIntroCore · · pats k) return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf) /-- From 2d487158664a1ec16cb7f5b6cc85b85d69d93663 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 11:36:00 +0200 Subject: [PATCH 02/53] Add a test for `iintro`: false elimination --- Iris/Iris/Tests/Tactics.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index fb8509a5f..4d7d027ec 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -273,6 +273,10 @@ example [BI PROP] (P Q : PROP) : ⊢ P → Q := by example [BI PROP] (P : PROP) : P -∗ P → P := by iintro HP1 HP2 +/- Tests `iintro` using the introduction pattern `⟨⟩` to solve the goal -/ +example [BI PROP] (P : PROP) : False ∗ □ P ⊢@{PROP} P := by + iintro ⟨⟨⟩, #_⟩ + end intro -- revert From 8730105d42835461984b212e58905430cb8188a8 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 11:58:20 +0200 Subject: [PATCH 03/53] Extend introduction pattern syntax: top-level only --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 51fad31bb..ef73fd8b7 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -6,6 +6,7 @@ Authors: Michael Sammler module public import Iris.ProofMode.Patterns.CasesPattern +public import Iris.ProofMode.Patterns.SelPattern meta import Iris.Std.RocqPorting @[expose] public section @@ -18,6 +19,12 @@ declare_syntax_cat introPat syntax icasesPat : introPat syntax "!>" : introPat syntax "//" : introPat +syntax "/=" : introPat +syntax "//=" : introPat +syntax "*" : introPat +syntax "**" : introPat +syntax "!%" : introPat +syntax "{" selPat* "}" : introPat @[rocq_alias intro_pat] inductive IntroPat From 7e3ce2c1106a42b3b03ba6f33856b957ec235f3f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 14:29:26 +0200 Subject: [PATCH 04/53] Implement the introduction pattern `/=` for simplification --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 2 ++ Iris/Iris/ProofMode/Tactics/Intro.lean | 7 ++++++- Iris/Iris/Tests/Tactics.lean | 14 ++++++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index ef73fd8b7..a33a22adf 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -31,6 +31,7 @@ inductive IntroPat | intro (case : iCasesPat) | trivial | modintro + | simpl deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -38,6 +39,7 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case)) | `(introPat| //) => return (term, .trivial) | `(introPat| !>) => return (term, .modintro) + | `(introPat| /=) => return (term, .simpl) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index e7cc2cb22..58d9e2b88 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König, Mario Carneiro, Michael Sammler +Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang -/ module @@ -75,6 +75,11 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} return r else iIntroCore hyps Q pats k + | (ref, .simpl) :: pats => + withRef ref do + let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems]) + let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] + iIntroCore hyps Q' pats k | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 4d7d027ec..b760801d2 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -277,6 +277,20 @@ example [BI PROP] (P : PROP) : P -∗ P → P := by example [BI PROP] (P : PROP) : False ∗ □ P ⊢@{PROP} P := by iintro ⟨⟨⟩, #_⟩ +@[simp] +private def def1 := 3 + +/- Tests `iintro` using the introduction pattern for simplification (`/=`) -/ +example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by + iintro /= HP + iexact HP + +/- Tests `iintro` where the lack of simplification (`/=`) causes a failure -/ +/-- error: iintro: if def1 = 3 then iprop(P -∗ P) else Q not a wand -/ +#guard_msgs in +example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by + iintro HP + end intro -- revert From 8cafc478f6c847fc6ab63e388d4bfcb945a0198c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 14:34:43 +0200 Subject: [PATCH 05/53] Implement `//=` introduction pattern --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 6 ++++-- Iris/Iris/ProofMode/Tactics/Intro.lean | 4 +++- Iris/Iris/Tests/Tactics.lean | 4 ++++ 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index a33a22adf..a417fc98b 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -31,7 +31,8 @@ inductive IntroPat | intro (case : iCasesPat) | trivial | modintro - | simpl + | simp + | simptrivial deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -39,7 +40,8 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case)) | `(introPat| //) => return (term, .trivial) | `(introPat| !>) => return (term, .modintro) - | `(introPat| /=) => return (term, .simpl) + | `(introPat| /=) => return (term, .simp) + | `(introPat| //=) => return (term, .simptrivial) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 58d9e2b88..a2490671e 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -75,11 +75,13 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} return r else iIntroCore hyps Q pats k - | (ref, .simpl) :: pats => + | (ref, .simp) :: pats => withRef ref do let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems]) let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] iIntroCore hyps Q' pats k + | (ref, .simptrivial) :: pats => + iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index b760801d2..9c2930f8d 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -291,6 +291,10 @@ example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by iintro HP +/- Tests `iintro` with simplification and trivial (`//=`) -/ +example [BI PROP] : ⊢@{PROP} if def1 = 3 then True else False := by + iintro //= + end intro -- revert From 147a68258216206b783538e3eba7284706ae5a9f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 15:15:06 +0200 Subject: [PATCH 06/53] Implement anonymous forall introduction pattern (`*`) --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 2 ++ Iris/Iris/ProofMode/Tactics/Intro.lean | 16 ++++++++++++++++ Iris/Iris/Tests/Tactics.lean | 12 +++++++++++- 3 files changed, 29 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index a417fc98b..7ba418825 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -33,6 +33,7 @@ inductive IntroPat | modintro | simp | simptrivial + | all deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -42,6 +43,7 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| !>) => return (term, .modintro) | `(introPat| /=) => return (term, .simp) | `(introPat| //=) => return (term, .simptrivial) + | `(introPat| *) => return (term, .all) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index a2490671e..53b7a3236 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -82,6 +82,22 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q' pats k | (ref, .simptrivial) :: pats => iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k + | (ref, .all) :: pats => + withRef ref do + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) with + | none => + iIntroCore hyps Q pats k + | some _ => + let (n, ref') ← getFreshName (← `(binderIdent| _)) + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref' (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + have : $B =Q $Φ $x := ⟨⟩ + let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <| ← iIntroCore hyps q($Φ $x) ((ref, .all) :: pats) k + return q(from_forall_intro (Q := $Q) $pf) | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 9c2930f8d..4742c1ac3 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -291,10 +291,20 @@ example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by iintro HP -/- Tests `iintro` with simplification and trivial (`//=`) -/ +/- Tests `iintro` with the pattern for simplification and solving trivial goals (`//=`) -/ example [BI PROP] : ⊢@{PROP} if def1 = 3 then True else False := by iintro //= +/- Tests `iintro` with the pattern for ∀-introduction (`*`) -/ +example {Val} [BI PROP] (P Q : Val → PROP) : ⊢@{PROP} ∀ x y, P x -∗ Q y -∗ P x ∗ Q y := by + iintro * _ _ + iframe + +example {Val} [BI PROP] (P : Val → Val → PROP) (Q : Val → PROP) : + ⊢@{PROP} ∀ x y, P x y -∗ ∀ z, (Q z -∗ P x y ∗ Q z) := by + iintro * _ * _ + iframe + end intro -- revert From 46cd6cc3b986214fea7ac6b2bff63eef6291db6c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 15:45:07 +0200 Subject: [PATCH 07/53] Implement introduction pattern `**` for iterative premise introduction --- .../Iris/ProofMode/Patterns/IntroPattern.lean | 2 ++ Iris/Iris/ProofMode/Tactics/Intro.lean | 27 +++++++++++++++++++ Iris/Iris/Tests/Tactics.lean | 12 ++++++--- 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 7ba418825..3a69fe41c 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -34,6 +34,7 @@ inductive IntroPat | simp | simptrivial | all + | allwand deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -44,6 +45,7 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| /=) => return (term, .simp) | `(introPat| //=) => return (term, .simptrivial) | `(introPat| *) => return (term, .all) + | `(introPat| **) => return (term, .allwand) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 53b7a3236..ed1679373 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -98,6 +98,33 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} have : $B =Q $Φ $x := ⟨⟩ let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <| ← iIntroCore hyps q($Φ $x) ((ref, .all) :: pats) k return q(from_forall_intro (Q := $Q) $pf) + | (ref, .allwand) :: pats => + withRef ref do + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) with + -- Introduction of a universally quantified variable + | some _ => + let (n, ref') ← getFreshName (← `(binderIdent| _)) + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref' (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + have : $B =Q $Φ $x := ⟨⟩ + let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <| ← iIntroCore hyps B ((ref, .allwand) :: pats) k + return q(from_forall_intro (Q := $Q) $pf) + -- Introduction of a wand premise or an implication premise, if possible + | none => + let A1 ← mkFreshExprMVarQ q($prop) + let A2 ← mkFreshExprMVarQ q($prop) + let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) + let instFromWand ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) + let instPersistent ← ProofModeM.trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) + match instFromWand, instFromImp, instPersistent with + | some _, _, _ | _, some _, some _ => + iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k + | _, _, _ => + iIntroCore hyps Q pats k | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 4742c1ac3..9a2772f16 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -296,14 +296,18 @@ example [BI PROP] : ⊢@{PROP} if def1 = 3 then True else False := by iintro //= /- Tests `iintro` with the pattern for ∀-introduction (`*`) -/ -example {Val} [BI PROP] (P Q : Val → PROP) : ⊢@{PROP} ∀ x y, P x -∗ Q y -∗ P x ∗ Q y := by +example {Val : Type} [BI PROP] (P Q : Val → PROP) : + ⊢@{PROP} ∀ x y, P x -∗ Q y -∗ P x ∗ Q y := by iintro * _ _ iframe -example {Val} [BI PROP] (P : Val → Val → PROP) (Q : Val → PROP) : - ⊢@{PROP} ∀ x y, P x y -∗ ∀ z, (Q z -∗ P x y ∗ Q z) := by - iintro * _ * _ +/-- Tests `iintro` with the pattern for repeating ∀-introduction and premise introduction (`**`) -/ +example {Val : Type} {ϕ : Prop} [BI PROP] (P : Val → Val → PROP) (Q : Val → PROP) : + ⊢@{PROP} ∀ x y, P x y -∗ ∀ z, (⌜ϕ⌝ → Q z -∗ P x y ∗ Q z ∗ ⌜ϕ⌝) := by + iintro ** iframe + ipureintro + assumption end intro From 0429f30dbf078513edbd701655ad0e88177c6e5f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 16:28:48 +0200 Subject: [PATCH 08/53] Towards implementing the introduction pattern for pure goal (`!%`) Currently requires `!%` to be the last pattern --- .../Iris/ProofMode/Patterns/IntroPattern.lean | 2 ++ Iris/Iris/ProofMode/Tactics/Intro.lean | 19 +++++++++++++++++++ Iris/Iris/Tests/Tactics.lean | 5 +++++ 3 files changed, 26 insertions(+) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 3a69fe41c..8e5c1abfe 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -35,6 +35,7 @@ inductive IntroPat | simptrivial | all | allwand + | pureintro deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -46,6 +47,7 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| //=) => return (term, .simptrivial) | `(introPat| *) => return (term, .all) | `(introPat| **) => return (term, .allwand) + | `(introPat| !%) => return (term, .pureintro) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index ed1679373..d9530e225 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -7,6 +7,7 @@ module public meta import Iris.ProofMode.Patterns.IntroPattern public meta import Iris.ProofMode.Tactics.Cases +public meta import Iris.ProofMode.Tactics.Pure public meta import Iris.ProofMode.Tactics.ModIntro public meta import Iris.ProofMode.Tactics.Trivial @@ -125,6 +126,24 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k | _, _, _ => iIntroCore hyps Q pats k + | (ref, .pureintro) :: _ => + withRef ref do + let b ← mkFreshExprMVarQ q(Bool) + let ϕ ← mkFreshExprMVarQ q(Prop) + let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) + | throwError "iintro: {Q} is not a pure" + let m : Q($ϕ) ← mkFreshExprMVar (← instantiateMVars ϕ) + addMVarGoal m.mvarId! + match ← whnf b with + | .const ``true _ => + have : $b =Q true := ⟨⟩ + let .some _ ← trySynthInstanceQ q(Affine $P) + | throwError "iintro: unable to introduce a pure goal as the context is not affine" + return q(pure_intro_affine (Q := $Q) $inst $m) + | .const ``false _ => + have : $b =Q false := ⟨⟩ + return q(pure_intro_spatial (Q := $Q) $inst $m) + | _ => throwError "iintro: bug in typeclass instances, cannot reduce {b} to true or false" | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 9a2772f16..05b105124 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -309,6 +309,11 @@ example {Val : Type} {ϕ : Prop} [BI PROP] (P : Val → Val → PROP) (Q : Val ipureintro assumption +/-- Tests `iintro` with the pattern for introducing a pure goal and exiting the proof mode (`!%`) -/ +example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ □ Q -∗ ⌜n = n⌝ := by + iintro - - !% + rfl + end intro -- revert From f0158b93d417488065876be64bd90eb6f93e2d56 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 17:30:00 +0200 Subject: [PATCH 09/53] Slight refactoring for the `.pureintro` case in `iIntroCore` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 13 ++++++++----- Iris/Iris/Tests/Tactics.lean | 10 ++++++++++ 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index d9530e225..6dbc5f82c 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -126,24 +126,27 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k | _, _, _ => iIntroCore hyps Q pats k - | (ref, .pureintro) :: _ => + | (ref, .pureintro) :: pats => withRef ref do let b ← mkFreshExprMVarQ q(Bool) let ϕ ← mkFreshExprMVarQ q(Prop) let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) | throwError "iintro: {Q} is not a pure" let m : Q($ϕ) ← mkFreshExprMVar (← instantiateMVars ϕ) - addMVarGoal m.mvarId! - match ← whnf b with + + let pf ← do match ← whnf b with | .const ``true _ => have : $b =Q true := ⟨⟩ let .some _ ← trySynthInstanceQ q(Affine $P) | throwError "iintro: unable to introduce a pure goal as the context is not affine" - return q(pure_intro_affine (Q := $Q) $inst $m) + pure q(pure_intro_affine (Q := $Q) $inst $m) | .const ``false _ => have : $b =Q false := ⟨⟩ - return q(pure_intro_spatial (Q := $Q) $inst $m) + pure q(pure_intro_spatial (Q := $Q) $inst $m) | _ => throwError "iintro: bug in typeclass instances, cannot reduce {b} to true or false" + + addMVarGoal m.mvarId! + return pf | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 05b105124..9a65120ba 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -314,8 +314,16 @@ example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ □ Q -∗ ⌜n = n⌝ := by iintro - - !% rfl +example [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := by + iintro !% + iintro %_ + iintro !% + assumption + end intro +/- + -- revert namespace revert @@ -2817,3 +2825,5 @@ example (P Q : PROP) : iloeb as IH end iloeb + +-/ From 9d84dd68333a00a4177246146f97d7f44ca3e37c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 1 Jul 2026 18:11:23 +0200 Subject: [PATCH 10/53] Generalise `iIntroCore` so that `!%` does not have to be the last pattern --- Iris/Iris/ProofMode/Tactics/Intro.lean | 13 ++++++++++--- Iris/Iris/ProofMode/Tactics/RevertIntro.lean | 6 +++--- Iris/Iris/Tests/Tactics.lean | 11 +++-------- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 6dbc5f82c..58542ee2e 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,6 +54,7 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std +set_option maxHeartbeats 205000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). The type of the current goal is given by `Q`. @@ -63,7 +64,7 @@ This function returns the proof of `P ⊢ Q` to be assigned. The new context is -/ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) - (k : ∀ {prop : Q(Type $u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : + (k : ∀ {u} {prop : Q(Type $u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : ProofModeM (Q($P ⊢ $Q)) := do match pats with | [] => k hyps Q @@ -132,7 +133,7 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} let ϕ ← mkFreshExprMVarQ q(Prop) let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) | throwError "iintro: {Q} is not a pure" - let m : Q($ϕ) ← mkFreshExprMVar (← instantiateMVars ϕ) + let m : Q($ϕ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars ϕ) let pf ← do match ← whnf b with | .const ``true _ => @@ -145,7 +146,13 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} pure q(pure_intro_spatial (Q := $Q) $inst $m) | _ => throwError "iintro: bug in typeclass instances, cannot reduce {b} to true or false" - addMVarGoal m.mvarId! + if pats.isEmpty then + addMVarGoal m.mvarId! + else + let ⟨newM, g⟩ ← startProofMode m.mvarId! + let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats k + newM.assign pf' + return pf | (ref, .intro (.pure n)) :: pats => withRef ref do diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean index 380de3c6d..4b16f1196 100644 --- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean +++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean @@ -13,8 +13,8 @@ open Lean Meta Elab.Tactic Qq public meta section -abbrev ProofModeContinuation (u : Level) := - ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} +abbrev ProofModeContinuation := + ∀ {u : Level} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (_hyps : Hyps bi e)(goal: Q($prop)), ProofModeM Q($e ⊢ $goal) @@ -22,7 +22,7 @@ def iRevertIntro {prop: Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (hyps : Hyps bi e) (goal: Q($prop)) (hs : List SelTarget) (k : ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} - (_hyps : Hyps bi e) (goal: Q($prop)), ProofModeContinuation u → + (_hyps : Hyps bi e) (goal: Q($prop)), ProofModeContinuation → ProofModeM Q($e ⊢ $goal)) : ProofModeM Q($e ⊢ $goal) := do let names : List (Syntax × IntroPat) ← hs.mapM fun diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 9a65120ba..345328a44 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -314,16 +314,13 @@ example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ □ Q -∗ ⌜n = n⌝ := by iintro - - !% rfl -example [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := by - iintro !% - iintro %_ - iintro !% +/-- Tests `iintro` with introduction patterns coming after `!%` -/ +example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := by + iintro !% %_ !% assumption end intro -/- - -- revert namespace revert @@ -2825,5 +2822,3 @@ example (P Q : PROP) : iloeb as IH end iloeb - --/ From 74811441b6a9aeffbc7415943620efd0ceb72a7a Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 10:58:07 +0200 Subject: [PATCH 11/53] Towards implementing `{ selPat* }` for clearing hypotheses --- .../Iris/ProofMode/Patterns/IntroPattern.lean | 4 ++- Iris/Iris/ProofMode/Tactics/Cases.lean | 2 +- Iris/Iris/ProofMode/Tactics/Clear.lean | 36 +++++++++++-------- Iris/Iris/ProofMode/Tactics/Intro.lean | 15 +++++--- Iris/Iris/Tests/Tactics.lean | 5 +++ 5 files changed, 41 insertions(+), 21 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 8e5c1abfe..e2d393678 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 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 @@ -36,6 +36,7 @@ inductive IntroPat | all | allwand | pureintro + | clear (selPats : List SelPat) deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -48,6 +49,7 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| *) => return (term, .all) | `(introPat| **) => return (term, .allwand) | `(introPat| !%) => return (term, .pureintro) + | `(introPat| { $spats:selPat* }) => return (term, .clear (← SelPat.parse spats)) | _ => Macro.throwUnsupported #rocq_ignore gallina_ident "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 018a288dd..d1c9cfb44 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -211,7 +211,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} else k (.mkSep hyps hyp) goal | .clear => do - let pf ← iClearCore bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) + let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) pure q($pf $(← k hyps goal)) | .frame => do diff --git a/Iris/Iris/ProofMode/Tactics/Clear.lean b/Iris/Iris/ProofMode/Tactics/Clear.lean index 8ec4be8a8..f40a1cdcf 100644 --- a/Iris/Iris/ProofMode/Tactics/Clear.lean +++ b/Iris/Iris/ProofMode/Tactics/Clear.lean @@ -25,7 +25,7 @@ theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP} public meta section open Lean Elab Tactic Meta Qq -def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) +def iClearCoreOne {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) (p : Q(Bool)) (out goal : Q($prop)) (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do match matchBool p with @@ -44,28 +44,36 @@ private def ClearState.clearProofModeHyp {u prop bi origE goal} : ProofModeM (@ClearState u prop bi origE goal) | { e, hyps, pf }, ivar => do let ⟨e', hyps', _, out', p, _, hrem⟩ := hyps.remove true ivar - let step ← iClearCore bi e e' p out' goal hrem + let step ← iClearCoreOne bi e e' p out' goal hrem let pf' : Q(($e' ⊢ $goal) → ($origE ⊢ $goal)) := q(λ h => $pf ($step h)) return { e := e', hyps := hyps', pf := pf' } -/-- - `iclear pats` discards the hypotheses selected by the selection pattern `pats`. --/ -elab "iclear " pats:(colGt ppSpace selPat)+ : tactic => do - let pats ← liftMacroM <| SelPat.parse pats - - ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do +def iClearCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} + (hyps : Hyps bi e) (goal : Q($prop)) (pats : List SelPat) + (k : ∀ {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} + (_ : Hyps bi e) (goal : Q($prop)) (_ : Array FVarId), ProofModeM Q($e ⊢ $goal)) : + ProofModeM Q($e ⊢ $goal) := do let (ivars, fvars) := (← SelPat.resolve hyps pats).partitionMap fun - | {kind := .ipm ivar, ..} => .inl ivar - | {kind := .pure id, ..} => .inr id + | {kind := .ipm ivar, ..} => .inl ivar + | {kind := .pure id, ..} => .inr id -- Clear the selected Iris hypotheses first, updating the proof-mode context and proof term. - let mut st : ClearState e goal := { e, hyps, pf := q(fun h => h) } + let mut st : ClearState e goal := { e, hyps, pf := q(id) } for ivar in ivars do st ← st.clearProofModeHyp ivar -- Lean locals are cleared afterwards; first ensure no remaining hypothesis or goal depends on them. for fvar in fvars do let _ ← st.hyps.checkRemovableFVar "iclear" fvar (some goal) fvars.contains - let pf' ← addBIGoalWithoutFVars st.hyps goal fvars.reverse.toArray - mvar.assign q($(st.pf) $pf') + let pf' ← k st.hyps goal fvars.reverse.toArray + return q($(st.pf) $pf') + +/-- + `iclear pats` discards the hypotheses selected by the selection pattern `pats`. +-/ +elab "iclear " pats:(colGt ppSpace selPat)+ : tactic => do + let pats ← liftMacroM <| SelPat.parse pats + + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do + let pf ← iClearCore hyps goal pats (addBIGoalWithoutFVars · ·) + mvar.assign pf diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 58542ee2e..34b9005d6 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,7 +54,7 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std -set_option maxHeartbeats 205000 in +set_option maxHeartbeats 210000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). The type of the current goal is given by `Q`. @@ -62,7 +62,7 @@ The type of the current goal is given by `Q`. This function returns the proof of `P ⊢ Q` to be assigned. The new context is included in the `goals` directly by the tactic. -/ -partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} +partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) (k : ∀ {u} {prop : Q(Type $u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : ProofModeM (Q($P ⊢ $Q)) := do @@ -134,7 +134,6 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) | throwError "iintro: {Q} is not a pure" let m : Q($ϕ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars ϕ) - let pf ← do match ← whnf b with | .const ``true _ => have : $b =Q true := ⟨⟩ @@ -145,15 +144,21 @@ partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} have : $b =Q false := ⟨⟩ pure q(pure_intro_spatial (Q := $Q) $inst $m) | _ => throwError "iintro: bug in typeclass instances, cannot reduce {b} to true or false" - if pats.isEmpty then addMVarGoal m.mvarId! else let ⟨newM, g⟩ ← startProofMode m.mvarId! let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats k newM.assign pf' - return pf + | (ref, .clear selPats) :: pats => + withRef ref do + match selPats with + | [] => iIntroCore hyps Q pats k + | s :: selPats => + iClearCore hyps Q [s] + fun hyps' goal' fvars => withoutFVars (u := 0) fvars + <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 345328a44..29236f9e5 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -319,6 +319,11 @@ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := iintro !% %_ !% assumption +/-- Tests `iintro` with an introduction pattern for clearing hypotheses (`{ selPats* }`) -/ +example [BI PROP] (P Q R : PROP) : ⊢ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by + iintro HP HQ HR #HS {HR #} + iframe HP HQ + end intro -- revert From d367ca7d1e59c91d693f3f855e620929f22e6700 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 11:12:00 +0200 Subject: [PATCH 12/53] Use `addLocalVarInfo` in `SelPat.resolveOne` for IDE syntax highlighting --- Iris/Iris/ProofMode/Patterns/SelPattern.lean | 1 + Iris/Iris/Tests/Tactics.lean | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/SelPattern.lean b/Iris/Iris/ProofMode/Patterns/SelPattern.lean index 588426efb..94c4f2c26 100644 --- a/Iris/Iris/ProofMode/Patterns/SelPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SelPattern.lean @@ -69,6 +69,7 @@ def SelPat.resolveOne (hyps : Hyps bi e) : SelPat → ProofModeM (List SelTarget return [⟨.ipm ivar, true⟩] | .leanIdent name => do let ldecl ← getLocalDeclFromUserName name.getId + addLocalVarInfo name (← getLCtx) ldecl.toExpr ldecl.type return [⟨.pure ldecl.fvarId, true⟩] | .intuitionistic => return hyps.intuitionisticIVarIds.map (⟨.ipm ·, false⟩) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 29236f9e5..f91dec513 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -320,8 +320,8 @@ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := assumption /-- Tests `iintro` with an introduction pattern for clearing hypotheses (`{ selPats* }`) -/ -example [BI PROP] (P Q R : PROP) : ⊢ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by - iintro HP HQ HR #HS {HR #} +example [BI PROP] (P Q R : PROP) (x y : Nat) : ⊢ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by + iintro HP HQ HR #HS {HR %x %y #} iframe HP HQ end intro From 4a10b97556af482214e67a5cabeb0293a5397c09 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 11:17:38 +0200 Subject: [PATCH 13/53] Slight test refinements --- Iris/Iris/Tests/Tactics.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index f91dec513..a064864c6 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -320,8 +320,8 @@ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := assumption /-- Tests `iintro` with an introduction pattern for clearing hypotheses (`{ selPats* }`) -/ -example [BI PROP] (P Q R : PROP) (x y : Nat) : ⊢ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by - iintro HP HQ HR #HS {HR %x %y #} +example [BI PROP] (P Q R : PROP) (ϕ : Prop) : ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by + iintro %hϕ HP HQ HR #HS {HR %hϕ %ϕ #} iframe HP HQ end intro From 6e8d9afd489a3d10288b00d465618f30d624dab3 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 11:53:08 +0200 Subject: [PATCH 14/53] Add a Boolean value to the `clear` constructor (`IntroPat`) to indicate whether to use `iclear` or `iframe` --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 7 +++++-- Iris/Iris/ProofMode/Tactics/Intro.lean | 3 +++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index e2d393678..7c4a36eb4 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -36,7 +36,7 @@ inductive IntroPat | all | allwand | pureintro - | clear (selPats : List SelPat) + | clear (selPats : List <| Bool × SelPat) deriving Repr, Inhabited partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do @@ -49,8 +49,11 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| *) => return (term, .all) | `(introPat| **) => return (term, .allwand) | `(introPat| !%) => return (term, .pureintro) - | `(introPat| { $spats:selPat* }) => return (term, .clear (← SelPat.parse spats)) + | `(introPat| { $spats:selPat* }) => return (term, .clear (← spats.toList.mapM parseSelPats)) | _ => Macro.throwUnsupported + where parseSelPats (spat : TSyntax `selPat) : MacroM <| Bool × SelPat := do + let spat ← SelPat.parseOne spat + return ⟨false, spat⟩ #rocq_ignore gallina_ident "Not necessary in Lean" #rocq_ignore intro_pat.big_conj "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 34b9005d6..999f1f29e 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -156,9 +156,12 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} match selPats with | [] => iIntroCore hyps Q pats k | s :: selPats => + match s.fst, s.snd with + | false, s => iClearCore hyps Q [s] fun hyps' goal' fvars => withoutFVars (u := 0) fvars <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k + | true, s => throwUnsupportedSyntax | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar From fb57a1cdb9de97c9f937db99623b157235d20666 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 13:09:08 +0200 Subject: [PATCH 15/53] Introduce `selPatFrame` for introduction pattern for framing --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 12 +++++++----- Iris/Iris/ProofMode/Tactics/Intro.lean | 8 +++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 7c4a36eb4..585ad1124 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -14,6 +14,9 @@ meta import Iris.Std.RocqPorting namespace Iris.ProofMode open Lean +declare_syntax_cat selPatFrame +syntax ("$" noWs)? selPat : selPatFrame + declare_syntax_cat introPat syntax icasesPat : introPat @@ -24,7 +27,7 @@ syntax "//=" : introPat syntax "*" : introPat syntax "**" : introPat syntax "!%" : introPat -syntax "{" selPat* "}" : introPat +syntax "{" (colGt ppSpace selPatFrame)* "}" : introPat @[rocq_alias intro_pat] inductive IntroPat @@ -49,11 +52,10 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do | `(introPat| *) => return (term, .all) | `(introPat| **) => return (term, .allwand) | `(introPat| !%) => return (term, .pureintro) - | `(introPat| { $spats:selPat* }) => return (term, .clear (← spats.toList.mapM parseSelPats)) + | `(introPat| { $spats:selPatFrame* }) => return (term, .clear (← spats.toList.mapM parseSelPats)) | _ => Macro.throwUnsupported - where parseSelPats (spat : TSyntax `selPat) : MacroM <| Bool × SelPat := do - let spat ← SelPat.parseOne spat - return ⟨false, spat⟩ + where parseSelPats (spat : TSyntax `selPatFrame) : MacroM <| Bool × SelPat := do + return ⟨!spat.raw[0].getArgs.isEmpty, ← SelPat.parseOne ⟨spat.raw[1]⟩⟩ #rocq_ignore gallina_ident "Not necessary in Lean" #rocq_ignore intro_pat.big_conj "Not necessary in Lean" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 999f1f29e..bc8f700f3 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,7 +54,7 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std -set_option maxHeartbeats 210000 in +set_option maxHeartbeats 220000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). The type of the current goal is given by `Q`. @@ -155,13 +155,11 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} withRef ref do match selPats with | [] => iIntroCore hyps Q pats k - | s :: selPats => - match s.fst, s.snd with - | false, s => + | ⟨false, s⟩ :: selPats => iClearCore hyps Q [s] fun hyps' goal' fvars => withoutFVars (u := 0) fvars <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k - | true, s => throwUnsupportedSyntax + | ⟨true, s⟩ :: selPats => throwUnsupportedSyntax | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar From f06233115963e1e4292426d3f4245903e645d1f7 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 13:33:12 +0200 Subject: [PATCH 16/53] Implement clearing and framing with introduction pattern --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 4 ++-- Iris/Iris/ProofMode/Tactics/Intro.lean | 10 ++++++---- Iris/Iris/Tests/Tactics.lean | 8 ++++---- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 585ad1124..f56c955aa 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -15,7 +15,7 @@ namespace Iris.ProofMode open Lean declare_syntax_cat selPatFrame -syntax ("$" noWs)? selPat : selPatFrame +syntax ("!" noWs)? selPat : selPatFrame declare_syntax_cat introPat @@ -27,7 +27,7 @@ syntax "//=" : introPat syntax "*" : introPat syntax "**" : introPat syntax "!%" : introPat -syntax "{" (colGt ppSpace selPatFrame)* "}" : introPat +syntax "{" (colGt selPatFrame)* "}" : introPat @[rocq_alias intro_pat] inductive IntroPat diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index bc8f700f3..8f0df39fa 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -156,10 +156,12 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} match selPats with | [] => iIntroCore hyps Q pats k | ⟨false, s⟩ :: selPats => - iClearCore hyps Q [s] - fun hyps' goal' fvars => withoutFVars (u := 0) fvars - <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k - | ⟨true, s⟩ :: selPats => throwUnsupportedSyntax + iClearCore hyps Q [s] + fun hyps' goal' fvars => withoutFVars (u := 0) fvars + <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k + | ⟨true, s⟩ :: selPats => + let res ← s.resolveOne hyps >>= iFrame _ _ hyps Q + res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index a064864c6..5e8811aed 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -319,10 +319,10 @@ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := iintro !% %_ !% assumption -/-- Tests `iintro` with an introduction pattern for clearing hypotheses (`{ selPats* }`) -/ -example [BI PROP] (P Q R : PROP) (ϕ : Prop) : ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ R -∗ □ S -∗ P ∗ Q := by - iintro %hϕ HP HQ HR #HS {HR %hϕ %ϕ #} - iframe HP HQ +/-- Tests `iintro` with an introduction pattern for clearing and framing hypotheses (`{ selPats* }`) -/ +example [BI PROP] (P Q R : PROP) (ϕ : Prop) : ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ R -∗ □ S -∗ □ T -∗ P ∗ Q ∗ T := by + iintro %hϕ HP HQ HR #HS #HT {HR %hϕ %ϕ !HP !# #} + iexact HQ end intro From ac309e7a10633d7cdc911d8ef44d4d1eeadbf18d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 13:34:42 +0200 Subject: [PATCH 17/53] `iFrame`: Make `bi` and `e` implicit --- Iris/Iris/ProofMode/Tactics/Cases.lean | 2 +- Iris/Iris/ProofMode/Tactics/Frame.lean | 6 +++--- Iris/Iris/ProofMode/Tactics/Intro.lean | 2 +- Iris/Iris/ProofMode/Tactics/Specialize.lean | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index d1c9cfb44..e83dab6b8 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -216,7 +216,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} | .frame => do let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps - let res ← iFrame bi _ hyps' goal [⟨.ipm ivar, true⟩] + let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩] res.finish @k | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A @k diff --git a/Iris/Iris/ProofMode/Tactics/Frame.lean b/Iris/Iris/ProofMode/Tactics/Frame.lean index af5be77c3..371bcadd4 100644 --- a/Iris/Iris/ProofMode/Tactics/Frame.lean +++ b/Iris/Iris/ProofMode/Tactics/Frame.lean @@ -86,7 +86,7 @@ private def FrameResult.step {u prop bi origE origGoal} : else return st -def iFrame {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) +def iFrame {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (hyps : Hyps bi e) (goal : Q($prop)) (sels : List SelTarget) : ProofModeM (FrameResult bi e goal) := do let mut st : FrameResult bi e goal := { progress := false, e, hyps, goal, pf := q(frame_init) } @@ -136,10 +136,10 @@ def FrameResult.finishClose {u prop bi origE origGoal} (res : @FrameResult u pro elab "iframe " pats:(colGt ppSpace selPat)+ : tactic => do let pats ← liftMacroM <| SelPat.parse pats - ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do let pats ← SelPat.resolve hyps pats - let res ← iFrame bi e hyps goal pats + let res ← iFrame hyps goal pats mvar.assign (← res.finish (addBIGoal · ·)) /-- diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 8f0df39fa..635832e4b 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -160,7 +160,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} fun hyps' goal' fvars => withoutFVars (u := 0) fvars <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k | ⟨true, s⟩ :: selPats => - let res ← s.resolveOne hyps >>= iFrame _ _ hyps Q + let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) | (ref, .intro (.pure n)) :: pats => withRef ref do diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean index 88c7c68da..e017b824e 100644 --- a/Iris/Iris/ProofMode/Tactics/Specialize.lean +++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean @@ -108,7 +108,7 @@ private def processWand : let out₂ ← mkFreshExprMVarQ prop let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂) | throwError m!"ispecialize: {out} is not a wand" - let res ← iFrame bi _ hypsr' out₁ (frameIVars.map (⟨.ipm ·, true⟩)) + let res ← iFrame hypsr' out₁ (frameIVars.map (⟨.ipm ·, true⟩)) let pf'' ← res.finish λ hyps goal => do if trivial then let some r ← iTrivial hyps goal @@ -127,7 +127,7 @@ private def processWand : let out₂ ← mkFreshExprMVarQ prop let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂) | throwError m!"ispecialize: {out} is not a wand" - let res ← iFrame bi _ hyps out₁ (← SelPat.resolve hyps [.spatial, .intuitionistic]) + let res ← iFrame hyps out₁ (← SelPat.resolve hyps [.spatial, .intuitionistic]) let ⟨_, hyps', pf'⟩ ← res.finishClose return { e := _, hyps := hyps', p := q(false), out := out₂, pf := q(specialize_wand_autoframe $out₂ $pf $pf') } From 2edbb8f896201e95aaaa8b6a27560e3c39613996 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 13:44:59 +0200 Subject: [PATCH 18/53] Introduce rewrite to case destruction pattern syntax --- Iris/Iris/ProofMode/Patterns/CasesPattern.lean | 7 ++++++- Iris/Iris/ProofMode/Tactics/Cases.lean | 4 +++- Iris/Iris/ProofMode/Tactics/Specialize.lean | 3 +-- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index 2013eb220..be684aa10 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König +Authors: Lars König, Alvin Tang -/ module @@ -23,6 +23,8 @@ syntax "%" binderIdent : icasesPat syntax "#" icasesPat : icasesPat syntax "∗" icasesPat : icasesPat syntax ">" icasesPat : icasesPat +syntax "←" : icasesPat +syntax "→" : icasesPat -- TODO: attach syntax to iCasesPat such that one can use withRef to -- associate the errors with the right part of the syntax @@ -36,6 +38,7 @@ inductive iCasesPat | intuitionistic (pat : iCasesPat) | spatial (pat : iCasesPat) | mod (pat : iCasesPat) + | rewrite (forward : Bool) deriving Repr, Inhabited partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do @@ -53,6 +56,8 @@ where | `(icasesPat| ∗$pat) => go pat |>.map .spatial | `(icasesPat| >$pat) => go pat |>.map .mod | `(icasesPat| ($pat)) => goAlts pat + | `(icasesPat| ←) => some <| .rewrite false + | `(icasesPat| →) => some <| .rewrite true | _ => none goAlts : TSyntax ``icasesPatAlts → Option iCasesPat | `(icasesPatAlts| $args|*) => diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index e83dab6b8..5bf069b79 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang +Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang, Alvin Tang -/ module @@ -256,6 +256,8 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A @k + | .rewrite _ => throwUnsupportedSyntax + /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. -/ diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean index e017b824e..e46032fbe 100644 --- a/Iris/Iris/ProofMode/Tactics/Specialize.lean +++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean @@ -141,8 +141,7 @@ TODO: This also needs to check that there are no modality addition patterns in ` @[rocq_alias intro_pat_intuitionistic, rocq_alias use_tac_specialize_intuitionistic_helper] def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool := match pat with - | .intuitionistic _ => true - | .pure _ => true + | .intuitionistic _ | .pure _ | .rewrite _ => true | _ => false /-- Specialize a proposition `A` by applying a sequence of specialization patterns. From b1cf2ab5fbad7f234a4ba10ab3d5de3722b2b071 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 16:09:07 +0200 Subject: [PATCH 19/53] Towards implementing rewriting as case destruction pattern --- Iris/Iris/ProofMode/Tactics/Cases.lean | 24 +++++++++++++++++++++++- Iris/Iris/ProofMode/Tactics/Intro.lean | 1 + Iris/Iris/Tests/Tactics.lean | 18 ++++++++++++++++-- 3 files changed, 40 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 5bf069b79..280de97a2 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -256,7 +256,29 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A @k - | .rewrite _ => throwUnsupportedSyntax + | .rewrite direction => do + iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) + fun _ h => do + let some _ ← inferType h <&> (pure <| Expr.eq? ·) + | throwError "not a pure equality" + + let target : Q(Prop) := q($(hyps.tm) ⊢ $goal) + let g := (← mkFreshExprSyntheticOpaqueMVar target).mvarId! + let ⟨eNew, eqPf, []⟩ ← g.rewrite target h (symm := !direction) + | throwError "rewriting should not give additional subgoals" + + let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails + | throwError "error" + + let some ⟨_, hyps'⟩ := parseHyps? bi tm' + | throwError "unable to parse" + + let gNew ← g.replaceTargetEq eNew eqPf + + gNew.assign (← k hyps' goal') + + instantiateMVars (.mvar g) + /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 635832e4b..8edbeedf3 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -162,6 +162,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | ⟨true, s⟩ :: selPats => let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) + -- | (ref, .intro (.rewrite _)) :: pats => throwUnsupportedSyntax | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 5e8811aed..8b36a485c 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -320,10 +320,24 @@ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := assumption /-- Tests `iintro` with an introduction pattern for clearing and framing hypotheses (`{ selPats* }`) -/ -example [BI PROP] (P Q R : PROP) (ϕ : Prop) : ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ R -∗ □ S -∗ □ T -∗ P ∗ Q ∗ T := by - iintro %hϕ HP HQ HR #HS #HT {HR %hϕ %ϕ !HP !# #} +example [BI PROP] (P Q R S T : PROP) (ϕ : Prop) : + ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ R -∗ □ S -∗ □ T -∗ P ∗ Q ∗ T := by + iintro %hϕ HP HQ {!HP} HR #HS #HT {HR %hϕ %ϕ !# #} iexact HQ +example (m n : Nat) : m = 2 → n = 3 → m.succ = n := by + intro hm hn + rewrite [hm, hn] + rfl + +example [BI PROP] (m n : Nat) : + ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜n = 3⌝ -∗ ⌜m.succ = n⌝ := by + iintro #H1 #H2 + icases H1 with → + icases H2 with → + ipureintro + rfl + end intro -- revert From 87ec06cbbcb8dae877db761016e1db4cf88b18f9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 16:23:11 +0200 Subject: [PATCH 20/53] Code and test cleanup --- Iris/Iris/ProofMode/Tactics/Cases.lean | 15 ++------ Iris/Iris/Tests/Tactics.lean | 50 ++++++++++++++++++++------ 2 files changed, 42 insertions(+), 23 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 280de97a2..8db19e6b4 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -259,27 +259,18 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} | .rewrite direction => do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) fun _ h => do - let some _ ← inferType h <&> (pure <| Expr.eq? ·) - | throwError "not a pure equality" - let target : Q(Prop) := q($(hyps.tm) ⊢ $goal) let g := (← mkFreshExprSyntheticOpaqueMVar target).mvarId! let ⟨eNew, eqPf, []⟩ ← g.rewrite target h (symm := !direction) - | throwError "rewriting should not give additional subgoals" - + | throwError "icases: rewriting should not give additional subgoals" let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails - | throwError "error" - + | throwError "icases: unable to parse the Iris entailment {eNew}" let some ⟨_, hyps'⟩ := parseHyps? bi tm' - | throwError "unable to parse" - + | throwError "icases: unable to parse the Iris entailment {tm'}" let gNew ← g.replaceTargetEq eNew eqPf - gNew.assign (← k hyps' goal') - instantiateMVars (.mvar g) - /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. -/ diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 8b36a485c..372fad885 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -325,18 +325,23 @@ example [BI PROP] (P Q R S T : PROP) (ϕ : Prop) : iintro %hϕ HP HQ {!HP} HR #HS #HT {HR %hϕ %ϕ !# #} iexact HQ -example (m n : Nat) : m = 2 → n = 3 → m.succ = n := by - intro hm hn - rewrite [hm, hn] - rfl - -example [BI PROP] (m n : Nat) : - ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜n = 3⌝ -∗ ⌜m.succ = n⌝ := by - iintro #H1 #H2 - icases H1 with → - icases H2 with → +/-- Tests `iintro` with introduction patterns for rewriting pure equalities -/ +example [BI PROP] (m n : Nat) (a b c : Prop) : + ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜3 = n⌝ -∗ ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by + iintro → ← ← → ipureintro - rfl + and_intros <;> rfl + +/- + Tests `iintro` with an introduction pattern for rewriting but the + hypothesis is not a pure equality +-/ +/-- error: Invalid rewrite argument: Expected an equality or iff proof or +definition name, but `x✝` is a proof of + P -/ +#guard_msgs in +example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by + iintro → end intro @@ -1768,6 +1773,29 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by iintro H icases H with ⟨HA, HB⟩ +/-- Tests `icases` with a case destruction pattern for rewriting pure equalities -/ +example [BI PROP] (m n : Nat) (a b c : Prop) : + ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜3 = n⌝ -∗ ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by + iintro #H1 H2 #H3 H4 + icases H1 with → + icases H2 with ← + icases H3 with ← + icases H4 with → + ipureintro + and_intros <;> rfl + +/- + Tests `icases` with a case destruction pattern for rewriting but the + hypothesis is not a pure equality +-/ +/-- error: Invalid rewrite argument: Expected an equality or iff proof or +definition name, but `x✝` is a proof of + P -/ +#guard_msgs in +example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by + iintro HP + icases HP with → + end cases section imodintro From c6327e1caab28b37077ef6bdd18104da47be3080 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 16:42:54 +0200 Subject: [PATCH 21/53] Handle `.intro (.rewrite ...)` case in `iIntroCore` --- Iris/Iris/ProofMode/Tactics/Cases.lean | 30 +++++++++++++++----------- Iris/Iris/ProofMode/Tactics/Intro.lean | 18 ++++++++++++++-- Iris/Iris/Tests/Tactics.lean | 2 +- 3 files changed, 35 insertions(+), 15 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 8db19e6b4..b42929b9d 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -177,6 +177,23 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A $p) return q(spatial_elim $(← k B)) +/-- Rewrite pure Lean equalities -/ +def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} + (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) + (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : + ProofModeM Q($e ⊢ $goal) := do + let target : Q(Prop) := q($(hyps.tm) ⊢ $goal) + let g := (← mkFreshExprSyntheticOpaqueMVar target).mvarId! + let ⟨eNew, eqPf, []⟩ ← g.rewrite target h (symm := !direction) + | throwError "icases: rewriting should not give additional subgoals" + let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails + | throwError "icases: unable to parse the Iris entailment {eNew}" + let some ⟨_, hyps'⟩ := parseHyps? bi tm' + | throwError "icases: unable to parse the Iris entailment {tm'}" + let gNew ← g.replaceTargetEq eNew eqPf + gNew.assign (← k hyps' goal') + instantiateMVars (.mvar g) + variable {prop : Q(Type u)} (bi : Q(BI $prop)) in /-- Recursively destruct the current hypothesis `□?p A` in the proof-mode context `hyps` @@ -258,18 +275,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} | .rewrite direction => do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) - fun _ h => do - let target : Q(Prop) := q($(hyps.tm) ⊢ $goal) - let g := (← mkFreshExprSyntheticOpaqueMVar target).mvarId! - let ⟨eNew, eqPf, []⟩ ← g.rewrite target h (symm := !direction) - | throwError "icases: rewriting should not give additional subgoals" - let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails - | throwError "icases: unable to parse the Iris entailment {eNew}" - let some ⟨_, hyps'⟩ := parseHyps? bi tm' - | throwError "icases: unable to parse the Iris entailment {tm'}" - let gNew ← g.replaceTargetEq eNew eqPf - gNew.assign (← k hyps' goal') - instantiateMVars (.mvar g) + <| fun _ h => iCasesPureRewrite hyps goal h direction k /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 8edbeedf3..f8bff335e 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,7 +54,7 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std -set_option maxHeartbeats 220000 in +set_option maxHeartbeats 250000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). The type of the current goal is given by `Q`. @@ -162,7 +162,21 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | ⟨true, s⟩ :: selPats => let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) - -- | (ref, .intro (.rewrite _)) :: pats => throwUnsupportedSyntax + | (ref, .intro (.rewrite direction)) :: pats => + withRef ref do + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) + | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" + let (n, ref) ← getFreshName (← `(binderIdent| _)) + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + have : $B =Q $Φ $x := ⟨⟩ + let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← + iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) + return q(from_forall_intro (Q := $Q) $pf) | (ref, .intro (.pure n)) :: pats => withRef ref do let v ← mkFreshLevelMVar diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 372fad885..c2ad440db 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -327,7 +327,7 @@ example [BI PROP] (P Q R S T : PROP) (ϕ : Prop) : /-- Tests `iintro` with introduction patterns for rewriting pure equalities -/ example [BI PROP] (m n : Nat) (a b c : Prop) : - ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜3 = n⌝ -∗ ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by + m = 2 → 3 = n → ⊢@{PROP} ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by iintro → ← ← → ipureintro and_intros <;> rfl From fa6414871a27aee9a2785e1d5a9fdae2928ad566 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 16:45:08 +0200 Subject: [PATCH 22/53] Typo fix --- Iris/Iris/ProofMode/Tactics/Cases.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index b42929b9d..d71ae8d0b 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -189,7 +189,7 @@ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails | throwError "icases: unable to parse the Iris entailment {eNew}" let some ⟨_, hyps'⟩ := parseHyps? bi tm' - | throwError "icases: unable to parse the Iris entailment {tm'}" + | throwError "icases: unable to parse the Iris context {tm'}" let gNew ← g.replaceTargetEq eNew eqPf gNew.assign (← k hyps' goal') instantiateMVars (.mvar g) From d7cc6994f183320aa0c73d88d145fe397e24b424 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 16:53:35 +0200 Subject: [PATCH 23/53] Apply `withoutFVars` to remove used pure equalities --- Iris/Iris/ProofMode/Tactics/Cases.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index d71ae8d0b..716f43f03 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -177,7 +177,10 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A $p) return q(spatial_elim $(← k B)) -/-- Rewrite pure Lean equalities -/ +/-- + Rewrite an Iris entailment using the pure Lean equality `h`, + removing `h` from the context afterwards. +-/ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : @@ -191,7 +194,7 @@ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} let some ⟨_, hyps'⟩ := parseHyps? bi tm' | throwError "icases: unable to parse the Iris context {tm'}" let gNew ← g.replaceTargetEq eNew eqPf - gNew.assign (← k hyps' goal') + gNew.assign (← withoutFVars (u := 0) #[h.fvarId!] <| k hyps' goal') instantiateMVars (.mvar g) variable {prop : Q(Type u)} (bi : Q(BI $prop)) in From e77e61e3b9b34d9ea7a737e3a7f7b95853bef257 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 18:00:55 +0200 Subject: [PATCH 24/53] Minor code style formatting --- Iris/Iris/ProofMode/Tactics/Cases.lean | 18 +++++++++--------- Iris/Iris/ProofMode/Tactics/Intro.lean | 12 +++++++----- 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 716f43f03..20fcdf0da 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -185,16 +185,16 @@ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : ProofModeM Q($e ⊢ $goal) := do - let target : Q(Prop) := q($(hyps.tm) ⊢ $goal) - let g := (← mkFreshExprSyntheticOpaqueMVar target).mvarId! - let ⟨eNew, eqPf, []⟩ ← g.rewrite target h (symm := !direction) + let target := q($(hyps.tm) ⊢ $goal) + let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!) + let ⟨newE, eq, []⟩ ← g.rewrite target h (symm := !direction) | throwError "icases: rewriting should not give additional subgoals" - let some #[_, _, tm', goal'] := eNew.consumeMData.appM? ``BIBase.Entails - | throwError "icases: unable to parse the Iris entailment {eNew}" - let some ⟨_, hyps'⟩ := parseHyps? bi tm' - | throwError "icases: unable to parse the Iris context {tm'}" - let gNew ← g.replaceTargetEq eNew eqPf - gNew.assign (← withoutFVars (u := 0) #[h.fvarId!] <| k hyps' goal') + let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails + | throwError "icases: unable to parse the Iris entailment {newE}" + let some ⟨_, hyps'⟩ := parseHyps? bi newTm + | throwError "icases: unable to parse the Iris context {newTm}" + let gNew ← g.replaceTargetEq newE eq + (withoutFVars (u := 0) #[h.fvarId!] <| k hyps' newGoal) >>= (gNew.assign ·) instantiateMVars (.mvar g) variable {prop : Q(Type u)} (bi : Q(BI $prop)) in diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index f8bff335e..06ece2cd5 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -98,7 +98,8 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} addLocalVarInfo ref' (← getLCtx) x α have B : Q($prop) := Expr.headBeta q($Φ $x) have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <| ← iIntroCore hyps q($Φ $x) ((ref, .all) :: pats) k + let pf : Q(∀ x, $P ⊢ $Φ x) ← + mkLambdaFVars #[x] <|← iIntroCore hyps q($Φ $x) ((ref, .all) :: pats) k return q(from_forall_intro (Q := $Q) $pf) | (ref, .allwand) :: pats => withRef ref do @@ -113,8 +114,9 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} addLocalVarInfo ref' (← getLCtx) x α have B : Q($prop) := Expr.headBeta q($Φ $x) have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <| ← iIntroCore hyps B ((ref, .allwand) :: pats) k - return q(from_forall_intro (Q := $Q) $pf) + let pf : Q(∀ x, $P ⊢ $Φ x) ← + mkLambdaFVars #[x] <|← iIntroCore hyps B ((ref, .allwand) :: pats) k + return q(from_forall_intro (Q := $Q) $pf) -- Introduction of a wand premise or an implication premise, if possible | none => let A1 ← mkFreshExprMVarQ q($prop) @@ -174,8 +176,8 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} addLocalVarInfo ref (← getLCtx) x α have B : Q($prop) := Expr.headBeta q($Φ $x) have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← - iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) + let pf : Q(∀ x, $P ⊢ $Φ x) ← + mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) return q(from_forall_intro (Q := $Q) $pf) | (ref, .intro (.pure n)) :: pats => withRef ref do From a014b62c4c69966ba0e1c94e0293cb074f5f6433 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 18:57:48 +0200 Subject: [PATCH 25/53] Minor fixes --- Iris/Iris/ProofMode/Tactics/Intro.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 06ece2cd5..90a8372b7 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -64,7 +64,7 @@ This function returns the proof of `P ⊢ Q` to be assigned. The new context is -/ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) - (k : ∀ {u} {prop : Q(Type $u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : + (k : ∀ {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : ProofModeM (Q($P ⊢ $Q)) := do match pats with | [] => k hyps Q @@ -99,7 +99,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} have B : Q($prop) := Expr.headBeta q($Φ $x) have : $B =Q $Φ $x := ⟨⟩ let pf : Q(∀ x, $P ⊢ $Φ x) ← - mkLambdaFVars #[x] <|← iIntroCore hyps q($Φ $x) ((ref, .all) :: pats) k + mkLambdaFVars #[x] <|← iIntroCore hyps B ((ref, .all) :: pats) k return q(from_forall_intro (Q := $Q) $pf) | (ref, .allwand) :: pats => withRef ref do From de6b3d9b3b8c59c8c9d0255aca85750b67008247 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 19:21:19 +0200 Subject: [PATCH 26/53] Refactor `iIntroCore`: `.intro (.pure ...)` and `.intro (.rewrite ...)` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 46 ++++++++++++-------------- 1 file changed, 21 insertions(+), 25 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 90a8372b7..a87e599bf 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,6 +54,23 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std +private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} + {P} (hyps : Hyps bi P) (ref : Syntax) (n : Name) (Q : Q($prop)) + (k : Expr → Q($prop) → ProofModeM Expr): + ProofModeM Q($P ⊢ $Q) := do + withRef ref do + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) + | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + have : $B =Q $Φ $x := ⟨⟩ + let pf : Q(∀ x, $P ⊢ $Φ x) ← k x B + return q(from_forall_intro (Q := $Q) $pf) + set_option maxHeartbeats 250000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). @@ -165,34 +182,13 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) | (ref, .intro (.rewrite direction)) :: pats => - withRef ref do - let v ← mkFreshLevelMVar - let α ← mkFreshExprMVarQ q(Sort v) - let Φ ← mkFreshExprMVarQ q($α → $prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) - | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" let (n, ref) ← getFreshName (← `(binderIdent| _)) - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← - mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) - return q(from_forall_intro (Q := $Q) $pf) + iIntroCoreForallIntro hyps ref n Q <| + fun x B => do mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) | (ref, .intro (.pure n)) :: pats => - withRef ref do - let v ← mkFreshLevelMVar - let α ← mkFreshExprMVarQ q(Sort v) - let Φ ← mkFreshExprMVarQ q($α → $prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) - | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" let (n, ref) ← getFreshName n - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore hyps B pats k - return q(from_forall_intro (Q := $Q) $pf) + iIntroCoreForallIntro hyps ref n Q <| + fun x B => do mkLambdaFVars #[x] <|← iIntroCore hyps B pats k | (ref, .intro pat) :: pats => withRef ref do let A1 ← mkFreshExprMVarQ q($prop) From a4aeb3b1719ef07855ee362fc55670cc82d0e91f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 19:38:34 +0200 Subject: [PATCH 27/53] Further refactor code --- Iris/Iris/ProofMode/Tactics/Intro.lean | 81 +++++++++++--------------- 1 file changed, 34 insertions(+), 47 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index a87e599bf..50123936d 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -54,22 +54,34 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} public meta section open Lean Elab Tactic Meta Qq BI Std +/-- + Used by `iIntroCore` for the cases `.intro (.pure …)`, `.intro (.rewrite …)`, + `.all` and `.allwand`. + + The function `k'` is the fallback option when type class synthesis with `Q` + using `FromForall` fails. The fallback option is applicable only for + `.all` and `.allwand`. +-/ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} - {P} (hyps : Hyps bi P) (ref : Syntax) (n : Name) (Q : Q($prop)) - (k : Expr → Q($prop) → ProofModeM Expr): + {P : Q($prop)} (ref : Syntax) (n : Name) (Q : Q($prop)) + (k' : Option <| ProofModeM Q($P ⊢ $Q)) + (k : Expr → Q($prop) → ProofModeM Expr) : ProofModeM Q($P ⊢ $Q) := do withRef ref do let v ← mkFreshLevelMVar let α ← mkFreshExprMVarQ q(Sort v) let Φ ← mkFreshExprMVarQ q($α → $prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) - | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← k x B - return q(from_forall_intro (Q := $Q) $pf) + match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ), k' with + | none, none => + throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" + | none, some k' => k' + | some _, _ => + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + have : $B =Q $Φ $x := ⟨⟩ + let pf : Q(∀ x, $P ⊢ $Φ x) ← k x B + return q(from_forall_intro (Q := $Q) $pf) set_option maxHeartbeats 250000 in /-- @@ -102,40 +114,13 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | (ref, .simptrivial) :: pats => iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k | (ref, .all) :: pats => - withRef ref do - let v ← mkFreshLevelMVar - let α ← mkFreshExprMVarQ q(Sort v) - let Φ ← mkFreshExprMVarQ q($α → $prop) - match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) with - | none => - iIntroCore hyps Q pats k - | some _ => - let (n, ref') ← getFreshName (← `(binderIdent| _)) - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref' (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← - mkLambdaFVars #[x] <|← iIntroCore hyps B ((ref, .all) :: pats) k - return q(from_forall_intro (Q := $Q) $pf) + let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) + iIntroCoreForallIntro ref n Q (iIntroCore hyps Q pats k) <| + (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) k) | (ref, .allwand) :: pats => - withRef ref do - let v ← mkFreshLevelMVar - let α ← mkFreshExprMVarQ q(Sort v) - let Φ ← mkFreshExprMVarQ q($α → $prop) - match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) with - -- Introduction of a universally quantified variable - | some _ => - let (n, ref') ← getFreshName (← `(binderIdent| _)) - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref' (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← - mkLambdaFVars #[x] <|← iIntroCore hyps B ((ref, .allwand) :: pats) k - return q(from_forall_intro (Q := $Q) $pf) + let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) -- Introduction of a wand premise or an implication premise, if possible - | none => + let kPremiseIntro : ProofModeM Q($P ⊢ $Q) := do let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) @@ -146,6 +131,8 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k | _, _, _ => iIntroCore hyps Q pats k + iIntroCoreForallIntro ref n Q kPremiseIntro <| + (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) k) | (ref, .pureintro) :: pats => withRef ref do let b ← mkFreshExprMVarQ q(Bool) @@ -182,13 +169,13 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) | (ref, .intro (.rewrite direction)) :: pats => - let (n, ref) ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro hyps ref n Q <| + let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) + iIntroCoreForallIntro ref n Q none <| fun x B => do mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) | (ref, .intro (.pure n)) :: pats => - let (n, ref) ← getFreshName n - iIntroCoreForallIntro hyps ref n Q <| - fun x B => do mkLambdaFVars #[x] <|← iIntroCore hyps B pats k + let ⟨n, _⟩ ← getFreshName n + iIntroCoreForallIntro ref n Q none <| + (do mkLambdaFVars #[·] <|← iIntroCore hyps · pats k) | (ref, .intro pat) :: pats => withRef ref do let A1 ← mkFreshExprMVarQ q($prop) From 86ff71d4303c59bbeca3712b6ba1bba15f8587bb Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 19:44:35 +0200 Subject: [PATCH 28/53] Typo fix --- Iris/Iris/ProofMode/Tactics/Intro.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 50123936d..303bf0776 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -138,7 +138,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let b ← mkFreshExprMVarQ q(Bool) let ϕ ← mkFreshExprMVarQ q(Prop) let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) - | throwError "iintro: {Q} is not a pure" + | throwError "iintro: {Q} is not pure" let m : Q($ϕ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars ϕ) let pf ← do match ← whnf b with | .const ``true _ => From be4da14a2d467b95613f1e924fdf68c5f340300f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 2 Jul 2026 20:28:26 +0200 Subject: [PATCH 29/53] Comments and code formatting --- Iris/Iris/ProofMode/Tactics/Intro.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 303bf0776..5eb2b839b 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -81,9 +81,8 @@ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} have B : Q($prop) := Expr.headBeta q($Φ $x) have : $B =Q $Φ $x := ⟨⟩ let pf : Q(∀ x, $P ⊢ $Φ x) ← k x B - return q(from_forall_intro (Q := $Q) $pf) + return q(from_forall_intro $pf) -set_option maxHeartbeats 250000 in /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). The type of the current goal is given by `Q`. @@ -115,23 +114,28 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k | (ref, .all) :: pats => let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro ref n Q (iIntroCore hyps Q pats k) <| + iIntroCoreForallIntro ref n Q + -- No more universally quantified variable to be introduced + (iIntroCore hyps Q pats k) + -- Introduction of a universally quantified variable (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) k) | (ref, .allwand) :: pats => let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - -- Introduction of a wand premise or an implication premise, if possible - let kPremiseIntro : ProofModeM Q($P ⊢ $Q) := do + let k' : ProofModeM Q($P ⊢ $Q) := do let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) let instFromWand ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) let instPersistent ← ProofModeM.trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) match instFromWand, instFromImp, instPersistent with + -- Introduction of a wand premise or a pure premise, if possible | some _, _, _ | _, some _, some _ => iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k | _, _, _ => + -- No more universally quantified variable or premise to be introduced iIntroCore hyps Q pats k - iIntroCoreForallIntro ref n Q kPremiseIntro <| + iIntroCoreForallIntro ref n Q k' + -- Introduction of a universally quantified variable (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) k) | (ref, .pureintro) :: pats => withRef ref do From 3d36c8b158f250b3da191b8402236ff38ff4f6a7 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:05:44 +0200 Subject: [PATCH 30/53] Code refactoring: theorems belong to `public section` --- Iris/Iris/ProofMode/Tactics/Combine.lean | 7 +++++-- Iris/Iris/ProofMode/Tactics/Pure.lean | 16 ++++++++-------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index ec5635610..d9a8b683d 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -12,8 +12,8 @@ public meta import Iris.ProofMode.ClassesMake namespace Iris.ProofMode -public meta section -open Lean Elab Tactic Meta Qq BI Std +public section +open BI Std /-- Auxiliary lemma for combining two hypotheses using `CombineSepAs` -/ theorem combine_as_step [BI PROP] {p1 p2 : Bool} {e e1 e2 out1 out2 out : PROP} @@ -95,6 +95,9 @@ theorem combine_as_gives [BI PROP] {p : Bool} {newE e outAs outGives goal : PROP _ ⊢ newE ∗ □?p (outAs ∗ □ outGives) := sep_mono_right intuitionisticallyIf_sep_mpr _ ⊢ goal := pfAsGives +public meta section +open Lean Elab Tactic Meta Qq BI Std + /-- The `icombine` tactic with the `as` syntax transforms the hypotheses corresponding to `origE` into `newE ∗ □?$p $outAs`, where `outAs` is the diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 6901ce5a2..9696d9b56 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -29,6 +29,14 @@ theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop} [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q := pure_elim_spatial h h' +theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop} + (h : FromPure true Q .out φ) [Affine P] (hφ : φ) : P ⊢ Q := + (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1 + +theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} + (h : FromPure false Q .out φ) (hφ : φ) : P ⊢ Q := + (pure_intro hφ).trans h.1 + public meta section open Lean Elab Tactic Meta Qq @@ -78,14 +86,6 @@ elab "iempintro" : tactic => do | throwError "iempintro: context is not affine" mvar.assign q(affine (P := $e)) -theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop} - (h : FromPure true Q .out φ) [Affine P] (hφ : φ) : P ⊢ Q := - (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1 - -theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} - (h : FromPure false Q .out φ) (hφ : φ) : P ⊢ Q := - (pure_intro hφ).trans h.1 - /-- `ipureintro` turns a goal of the form `⌜φ⌝` into the Lean goal `φ`. -/ From 4db7727a083cf373c962205c0371e8bbd1409468 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:16:35 +0200 Subject: [PATCH 31/53] Move code in `ipureintro` into new helper function `iPureIntroCore` for reusability --- Iris/Iris/ProofMode/Tactics/Pure.lean | 48 ++++++++++++++++----------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 9696d9b56..f75e56884 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -61,6 +61,30 @@ def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) | throwError "ipure: {A} is not affine and the goal not absorbing" return q(pure_elim_spatial (A:=$A) $pf $f) +def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop)) + (e goal : Q($prop)) (tacName : String) : + ProofModeM <| Q($e ⊢ $goal) × MVarId := do + let b : Q(Bool) ← mkFreshExprMVarQ q(Bool) + let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) + let .some h ← ProofModeM.trySynthInstanceQ q(FromPure $b $goal .out $φ) + | throwError "{tacName}: {goal} is not pure" + let m : Q($φ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars φ) + + let pf : Q($e ⊢ $goal) ← do + match ← whnf b with + | .const ``true _ => + have : $b =Q true := ⟨⟩ + let .some _ ← trySynthInstanceQ q(Affine $e) + | throwError "{tacName}: context is not affine" + pure q(pure_intro_affine (P := $e) (Q := $goal) $h $m) + | .const ``false _ => + have : $b =Q false := ⟨⟩ + pure q(pure_intro_spatial (P := $e) (Q := $goal) $h $m) + -- the following indicates a bug in the typeclass instances that generate b + | _ => throwError "{tacName}: bug in typeclass instances, cannot reduce {b} to true or false" + + return ⟨pf, m.mvarId!⟩ + /-- `ipure H` moves a pure hypothesis `H` from the Iris context into the regular Lean context. @@ -90,26 +114,10 @@ elab "iempintro" : tactic => do `ipureintro` turns a goal of the form `⌜φ⌝` into the Lean goal `φ`. -/ elab "ipureintro" : tactic => do - ProofModeM.runTactic λ mvar { e, goal, .. } => do - - let b : Q(Bool) ← mkFreshExprMVarQ q(Bool) - let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) - let .some h ← ProofModeM.trySynthInstanceQ q(FromPure $b $goal .out $φ) - | throwError "ipureintro: {goal} is not pure" - let m : Q($φ) ← mkFreshExprMVar (← instantiateMVars φ) - addMVarGoal m.mvarId! - - match ← whnf b with - | .const ``true _ => - have : $b =Q true := ⟨⟩ - let .some _ ← trySynthInstanceQ q(Affine $e) - | throwError "ipureintro: context is not affine" - mvar.assign q(pure_intro_affine (P := $e) (Q := $goal) $h $m) - | .const ``false _ => - have : $b =Q false := ⟨⟩ - mvar.assign q(pure_intro_spatial (P := $e) (Q := $goal) $h $m) - -- the following indicates a bug in the typeclass instances that generate b - | _ => throwError "ipureintro: bug in typeclass instances, cannot reduce {b} to true or false" + ProofModeM.runTactic λ mvar { bi, e, goal, .. } => do + let ⟨pf, m⟩ ← iPureIntroCore bi e goal "ipureintro" + addMVarGoal m + mvar.assign pf -- TODO: what is the best lean automation tactic to call here? -- `assumption` is necessary if the goal contains mvars From 60041fcb46a04402aa50e9e178839b147d9adafb Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:18:54 +0200 Subject: [PATCH 32/53] Add missing `withRef ref do ...` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 5eb2b839b..1dc47b9b6 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -111,8 +111,10 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] iIntroCore hyps Q' pats k | (ref, .simptrivial) :: pats => + withRef ref do iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k | (ref, .all) :: pats => + withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) iIntroCoreForallIntro ref n Q -- No more universally quantified variable to be introduced @@ -120,6 +122,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} -- Introduction of a universally quantified variable (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) k) | (ref, .allwand) :: pats => + withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) let k' : ProofModeM Q($P ⊢ $Q) := do let A1 ← mkFreshExprMVarQ q($prop) @@ -173,10 +176,12 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) | (ref, .intro (.rewrite direction)) :: pats => + withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) iIntroCoreForallIntro ref n Q none <| fun x B => do mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) | (ref, .intro (.pure n)) :: pats => + withRef ref do let ⟨n, _⟩ ← getFreshName n iIntroCoreForallIntro ref n Q none <| (do mkLambdaFVars #[·] <|← iIntroCore hyps · pats k) From e0021b6b98a91280467bca2df494680786a48025 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:21:12 +0200 Subject: [PATCH 33/53] Use the helper function `iPureIntroCore` in `iIntroCore` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 20 +++----------------- Iris/Iris/Tests/Tactics.lean | 6 ++++++ 2 files changed, 9 insertions(+), 17 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 1dc47b9b6..1f0c913f1 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -142,25 +142,11 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) k) | (ref, .pureintro) :: pats => withRef ref do - let b ← mkFreshExprMVarQ q(Bool) - let ϕ ← mkFreshExprMVarQ q(Prop) - let some inst ← ProofModeM.trySynthInstanceQ q(FromPure $b $Q .out $ϕ) - | throwError "iintro: {Q} is not pure" - let m : Q($ϕ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars ϕ) - let pf ← do match ← whnf b with - | .const ``true _ => - have : $b =Q true := ⟨⟩ - let .some _ ← trySynthInstanceQ q(Affine $P) - | throwError "iintro: unable to introduce a pure goal as the context is not affine" - pure q(pure_intro_affine (Q := $Q) $inst $m) - | .const ``false _ => - have : $b =Q false := ⟨⟩ - pure q(pure_intro_spatial (Q := $Q) $inst $m) - | _ => throwError "iintro: bug in typeclass instances, cannot reduce {b} to true or false" + let ⟨pf, m⟩ ← iPureIntroCore bi P Q "iintro" if pats.isEmpty then - addMVarGoal m.mvarId! + addMVarGoal m else - let ⟨newM, g⟩ ← startProofMode m.mvarId! + let ⟨newM, g⟩ ← startProofMode m let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats k newM.assign pf' return pf diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index c2ad440db..e489b07ad 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -314,6 +314,12 @@ example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ □ Q -∗ ⌜n = n⌝ := by iintro - - !% rfl +/- Tests `iintro` with pure introduction failure -/ +/-- error: iintro: Q is not pure -/ +#guard_msgs in +example [BI PROP] (P Q : PROP) : P ⊢ Q := by + iintro HP !% + /-- Tests `iintro` with introduction patterns coming after `!%` -/ example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := by iintro !% %_ !% From b3e4c9ca467fd684a9ab104356eec41abb96c55b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:37:44 +0200 Subject: [PATCH 34/53] Take the tactic names of `iIntroCore` and `iCasesCore` as an argument For more accurate printing of error messages --- Iris/Iris/ProofMode/Tactics/Cases.lean | 73 ++++++++++---------- Iris/Iris/ProofMode/Tactics/Clear.lean | 6 +- Iris/Iris/ProofMode/Tactics/Combine.lean | 6 +- Iris/Iris/ProofMode/Tactics/Have.lean | 2 +- Iris/Iris/ProofMode/Tactics/Intro.lean | 71 +++++++++---------- Iris/Iris/ProofMode/Tactics/Loeb.lean | 6 +- Iris/Iris/ProofMode/Tactics/ModIntro.lean | 7 +- Iris/Iris/ProofMode/Tactics/RevertIntro.lean | 4 +- 8 files changed, 89 insertions(+), 86 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 20fcdf0da..4fcf15776 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -64,23 +64,24 @@ public meta section open Lean Elab Tactic Meta Qq Std private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) - {P} (_hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) : + {P} (_hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) (tacName : String) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do if let .defEq _ ← isDefEqQ A q(iprop(False)) then return q(false_elim') else - throwError "icases: cannot destruct {A} as an empty conjunct" + throwError "{tacName}: cannot destruct {A} as an empty conjunct" /-- Destruct an existential hypothesis [A] by introducing its witness and continuing with the body [B]. -/ -private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (name : TSyntax ``binderIdent) - (p : Q(Bool)) (P A goal : Q($prop)) +private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) + (name : TSyntax ``binderIdent) + (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do let v ← mkFreshLevelMVar let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v) let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ) - | throwError "icases: {A} is not an existential quantifier" + | throwError "{tacName}: {A} is not an existential quantifier" let (name, ref) ← getFreshName name withLocalDeclDQ name α fun x => do addLocalVarInfo ref (← getLCtx) x α @@ -102,7 +103,7 @@ private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) /-- Destruct a conjunction hypothesis [A] into two parts and continue with the left and right subpatterns in sequence. -/ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) - {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) + {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) (tacName : String) (k : ∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal)) (k1 k2 : ∀ {P}, Hyps bi P → (goal B : Q($prop)) → (∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal)) → @@ -113,36 +114,36 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) match matchBool p with | .inl _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A $A1 $A2) - | throwError "icases: cannot destruct {A}" + | throwError "{tacName}: cannot destruct {A}" let goal' := q(iprop(□ $A2 -∗ $goal)) let pf ← k1 hyps goal' A1 fun hyps goal' => do let goal'' ← mkFreshExprMVarQ q($prop) let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'') - | throwError "icases: internal error: {goal'} is not a wand" + | throwError "{tacName}: internal error: {goal'} is not a wand" let pf ← k2 hyps goal'' A2 k return q((wand_intro $pf).trans (from_wand .in (Q1:=iprop(□ $A2)))) return q(and_elim_intuitionistic $pf) | .inr _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A $A1 $A2) - | throwError "icases: cannot destruct {A}" + | throwError "{tacName}: cannot destruct {A}" let goal' := q(iprop($A2 -∗ $goal)) let pf ← k1 hyps goal' A1 fun hyps goal' => do let goal'' ← mkFreshExprMVarQ q($prop) let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'') - | throwError "icases: internal error: {goal'} is not a wand" + | throwError "{tacName}: internal error: {goal'} is not a wand" let pf ← k2 hyps goal'' A2 k return q((wand_intro $pf).trans (from_wand .in (Q1:=$A2))) return q(sep_elim_spatial (A := $A) $pf) /-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/ private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) - (p : Q(Bool)) (P A goal : Q($prop)) + (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k1 k2 : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoOr $A $A1 $A2) - | throwError "icases: {A} is not a disjunction" + | throwError "{tacName}: {A} is not a disjunction" return q(or_elim' $(← k1 A1) $(← k2 A2)) /-- @@ -150,18 +151,18 @@ Destruct a persistent hypothesis [A] by turning it into an explicit [□ B] and the persistent body. -/ private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) - (p : Q(Bool)) (P A goal : Q($prop)) + (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k : (B : Q($prop)) → ProofModeM Q($P ∗ □ $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do let B ← mkFreshExprMVarQ q($prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A $B) - | throwError "icases: {A} not persistent" + | throwError "{tacName}: {A} not persistent" match matchBool p with | .inl _ => return q(intuitionistic_elim_intuitionistic $(← k B)) | .inr _ => let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $goal)) - | throwError "icases: {A} not affine and the goal not absorbing" + | throwError "{tacName}: {A} not affine and the goal not absorbing" return q(intuitionistic_elim_spatial (A := $A) $(← k B)) /-- @@ -182,17 +183,17 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) removing `h` from the context afterwards. -/ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} - (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) + (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) (tacName : String) (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : ProofModeM Q($e ⊢ $goal) := do let target := q($(hyps.tm) ⊢ $goal) let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!) let ⟨newE, eq, []⟩ ← g.rewrite target h (symm := !direction) - | throwError "icases: rewriting should not give additional subgoals" + | throwError "{tacName}: rewriting should not give additional subgoals" let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails - | throwError "icases: unable to parse the Iris entailment {newE}" + | throwError "{tacName}: unable to parse the Iris entailment {newE}" let some ⟨_, hyps'⟩ := parseHyps? bi newTm - | throwError "icases: unable to parse the Iris context {newTm}" + | throwError "{tacName}: unable to parse the Iris context {newTm}" let gNew ← g.replaceTargetEq newE eq (withoutFVars (u := 0) #[h.fvarId!] <| k hyps' newGoal) >>= (gNew.assign ·) instantiateMVars (.mvar g) @@ -217,7 +218,7 @@ A proof of `hyps ∗ □?p A ⊢ goal`. -/ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat) - (p : Q(Bool)) (A : Q($prop)) + (p : Q(Bool)) (A : Q($prop)) (tacName : String) (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal') := addBIGoal) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := match pat with @@ -231,54 +232,54 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} else k (.mkSep hyps hyp) goal | .clear => do - let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) + let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) tacName pure q($pf $(← k hyps goal)) | .frame => do let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩] - res.finish @k + res.finish k - | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A @k + | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A tacName k | .disjunction [] => throwUnsupportedSyntax - | .conjunction [] => iCasesEmptyConj bi hyps p A goal + | .conjunction [] => iCasesEmptyConj bi hyps p A goal tacName -- pure conjunctions are always handled as existentials. There is `intoExist_and_pure` and -- `intoExist_sep_pure` to make this work as expected for pure assertions that are not explicit existentials. | .conjunction (.pure arg :: args) => do - iCasesExists bi arg p P A goal (iCasesCore hyps goal (.conjunction args) p · k) + iCasesExists bi arg p P A goal tacName (iCasesCore hyps goal (.conjunction args) p · tacName k) | .conjunction (arg :: args) => do if arg matches .clear then if let some pf ← iCasesAndLR bi p P A goal true λ B => - iCasesCore hyps goal (.conjunction args) p B @k then return pf + iCasesCore hyps goal (.conjunction args) p B tacName k then return pf if args matches [.clear] then if let some pf ← iCasesAndLR bi p P A goal false λ B => - iCasesCore hyps goal arg p B @k then return pf - iCasesSep bi hyps p A goal @k (iCasesCore · · arg p · ·) - (iCasesCore · · (.conjunction args) p · ·) + iCasesCore hyps goal arg p B tacName k then return pf + iCasesSep bi hyps p A goal tacName k (iCasesCore · · arg p · tacName ·) + (iCasesCore · · (.conjunction args) p · tacName ·) | .disjunction (arg :: args) => - iCasesOr bi p P A goal (iCasesCore hyps goal arg p · k) - (iCasesCore hyps goal (.disjunction args) p · k) + iCasesOr bi p P A goal tacName (iCasesCore hyps goal arg p · tacName k) + (iCasesCore hyps goal (.disjunction args) p · tacName k) | .pure arg => do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal | .intuitionistic arg => - iCasesIntuitionistic bi p P A goal (iCasesCore hyps goal arg q(true) · @k) + iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) | .spatial arg => - iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · @k) + iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · tacName k) | .mod arg => iModCore bi P goal p A λ p' A goal' => - iCasesCore hyps goal' arg p' A @k + iCasesCore hyps goal' arg p' A tacName k | .rewrite direction => do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) - <| fun _ h => iCasesPureRewrite hyps goal h direction k + <| fun _ h => iCasesPureRewrite hyps goal h direction tacName k /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. @@ -295,7 +296,7 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t (try_dup_context := pat.should_try_dup_context) -- process pattern - let pf2 ← iCasesCore hyps goal pat p A + let pf2 ← iCasesCore hyps goal pat p A "icases" mvar.assign q(($pf).trans $pf2) diff --git a/Iris/Iris/ProofMode/Tactics/Clear.lean b/Iris/Iris/ProofMode/Tactics/Clear.lean index f40a1cdcf..8330cea9e 100644 --- a/Iris/Iris/ProofMode/Tactics/Clear.lean +++ b/Iris/Iris/ProofMode/Tactics/Clear.lean @@ -26,13 +26,13 @@ public meta section open Lean Elab Tactic Meta Qq def iClearCoreOne {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) - (p : Q(Bool)) (out goal : Q($prop)) - (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do + (p : Q(Bool)) (out goal : Q($prop)) (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) + (tacName : String := "iclear") : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do match matchBool p with | .inl _ => return q(clear_intuitionistic (Q := $goal) $pf) | .inr _ => let .some _ ← trySynthInstanceQ q(TCOr (Affine $out) (Absorbing $goal)) - | throwError "iclear: {out} is not affine and the goal not absorbing" + | throwError "{tacName}: {out} is not affine and the goal not absorbing" return q(clear_spatial (A:=$out) $pf) private structure ClearState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (origE goal : Q($prop)) where diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index d9a8b683d..eea53aa54 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -231,7 +231,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* let hs ← iCombineParseSelPats hyps patSels let st ← iCombineCore hs hyps goal - let pf ← iCasesCore st.newHyps goal pat q($(st.p)) st.outAs addBIGoal + let pf ← iCasesCore st.newHyps goal pat q($(st.p)) st.outAs "icombine" mvar.assign q($(st.pfAs).trans $pf) /-- @@ -253,7 +253,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* match st.outGives, st.pfGives with | some outGives, pfGives => - let pf ← iCasesCore hyps goal pat q(true) outGives addBIGoal + let pf ← iCasesCore hyps goal pat q(true) outGives "icombine" mvar.assign q($(pfGives).trans $pf) | none, _ => throwNoInstanceForGives @@ -283,6 +283,6 @@ elab "icombine " patSels:(colGt ppSpace selPat)* match st.outGives, st.pfGives with | some outGives, pfGives => let pf ← iCasesCore st.newHyps goal (.conjunction [pat1, .intuitionistic pat2]) - q($st.p) q(iprop($st.outAs ∗ □ $outGives)) addBIGoal + q($st.p) q(iprop($st.outAs ∗ □ $outGives)) "icombine" mvar.assign q(combine_as_gives $st.pfAs $pfGives $pf) | none, _ => throwNoInstanceForGives diff --git a/Iris/Iris/ProofMode/Tactics/Have.lean b/Iris/Iris/ProofMode/Tactics/Have.lean index abe101fdf..c40cf96a5 100644 --- a/Iris/Iris/ProofMode/Tactics/Have.lean +++ b/Iris/Iris/ProofMode/Tactics/Have.lean @@ -40,5 +40,5 @@ elab "ihave " colGt pat:icasesPat " : " P:term " $$ " spat:specPat : tactic => d let P ← elabTermEnsuringTypeQ (← `(iprop($P))) prop -- establish `P` with `spat` let ⟨_, hyps', p, A, pf⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) [spat] (try_dup_context := pat.should_try_dup_context) - let pf2 ← iCasesCore hyps' goal pat p A + let pf2 ← iCasesCore hyps' goal pat p A "ihave" mvar.assign q(ihave_assert (($pf).trans $pf2)) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 1f0c913f1..8a8fe657e 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -63,7 +63,7 @@ open Lean Elab Tactic Meta Qq BI Std `.all` and `.allwand`. -/ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} - {P : Q($prop)} (ref : Syntax) (n : Name) (Q : Q($prop)) + {P : Q($prop)} (ref : Syntax) (n : Name) (Q : Q($prop)) (tacName : String) (k' : Option <| ProofModeM Q($P ⊢ $Q)) (k : Expr → Q($prop) → ProofModeM Expr) : ProofModeM Q($P ⊢ $Q) := do @@ -73,7 +73,7 @@ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let Φ ← mkFreshExprMVarQ q($α → $prop) match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ), k' with | none, none => - throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis" + throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" | none, some k' => k' | some _, _ => withLocalDeclDQ n α fun x => do @@ -91,36 +91,36 @@ This function returns the proof of `P ⊢ Q` to be assigned. The new context is `goals` directly by the tactic. -/ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} - {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) + {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) (tacName : String) (k : ∀ {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) : ProofModeM (Q($P ⊢ $Q)) := do match pats with | [] => k hyps Q | (ref, .modintro) :: pats => withRef ref do - iModIntroCore hyps Q (← `(_)) (iIntroCore · · pats k) + iModIntroCore hyps Q (← `(_)) tacName (iIntroCore · · pats tacName k) | (ref, .trivial) :: pats => withRef ref do if let some r ← iTrivial hyps Q then return r else - iIntroCore hyps Q pats k + iIntroCore hyps Q pats tacName k | (ref, .simp) :: pats => withRef ref do let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems]) let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] - iIntroCore hyps Q' pats k + iIntroCore hyps Q' pats tacName k | (ref, .simptrivial) :: pats => withRef ref do - iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) k + iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) tacName k | (ref, .all) :: pats => withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro ref n Q + iIntroCoreForallIntro ref n Q tacName -- No more universally quantified variable to be introduced - (iIntroCore hyps Q pats k) + (iIntroCore hyps Q pats tacName k) -- Introduction of a universally quantified variable - (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) k) + (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) tacName k) | (ref, .allwand) :: pats => withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) @@ -133,80 +133,81 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} match instFromWand, instFromImp, instPersistent with -- Introduction of a wand premise or a pure premise, if possible | some _, _, _ | _, some _, some _ => - iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) k + iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k | _, _, _ => -- No more universally quantified variable or premise to be introduced - iIntroCore hyps Q pats k - iIntroCoreForallIntro ref n Q k' + iIntroCore hyps Q pats tacName k + iIntroCoreForallIntro ref n Q tacName k' -- Introduction of a universally quantified variable - (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) k) + (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) tacName k) | (ref, .pureintro) :: pats => withRef ref do - let ⟨pf, m⟩ ← iPureIntroCore bi P Q "iintro" + let ⟨pf, m⟩ ← iPureIntroCore bi P Q tacName if pats.isEmpty then addMVarGoal m else let ⟨newM, g⟩ ← startProofMode m - let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats k + let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats tacName k newM.assign pf' return pf | (ref, .clear selPats) :: pats => withRef ref do match selPats with - | [] => iIntroCore hyps Q pats k + | [] => iIntroCore hyps Q pats tacName k | ⟨false, s⟩ :: selPats => iClearCore hyps Q [s] fun hyps' goal' fvars => withoutFVars (u := 0) fvars - <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) k + <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) tacName k | ⟨true, s⟩ :: selPats => let res ← s.resolveOne hyps >>= iFrame hyps Q - res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) k) + res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) | (ref, .intro (.rewrite direction)) :: pats => withRef ref do let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro ref n Q none <| - fun x B => do mkLambdaFVars #[x] <|← iCasesPureRewrite hyps B x direction (iIntroCore · · pats k) + iIntroCoreForallIntro ref n Q tacName none <| + fun x B => do mkLambdaFVars #[x] <|← + iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) | (ref, .intro (.pure n)) :: pats => withRef ref do let ⟨n, _⟩ ← getFreshName n - iIntroCoreForallIntro ref n Q none <| - (do mkLambdaFVars #[·] <|← iIntroCore hyps · pats k) + iIntroCoreForallIntro ref n Q tacName none <| + (do mkLambdaFVars #[·] <|← iIntroCore hyps · pats tacName k) | (ref, .intro pat) :: pats => withRef ref do let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) if let (.clear, some _) := (pat, fromImp) then - let pf ← iIntroCore hyps A2 pats k + let pf ← iIntroCore hyps A2 pats tacName k return q(imp_intro_drop (Q := $Q) $pf) else let B ← mkFreshExprMVarQ q($prop) match pat, fromImp with | .intuitionistic pat, some _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) - | throwError "iintro: {A1} not persistent" - let pf ← iCasesCore hyps A2 pat q(true) B (iIntroCore · · pats k) + | throwError "{tacName}: {A1} not persistent" + let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) return q(imp_intro_intuitionistic (Q := $Q) $pf) | .intuitionistic pat, none => let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) - | throwError "iintro: {Q} not a wand" + | throwError "{tacName}: {Q} not a wand" let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) - | throwError "iintro: {A1} not persistent" + | throwError "{tacName}: {A1} not persistent" let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2)) - | throwError "iintro: {A1} not affine and the goal not absorbing" - let pf ← iCasesCore hyps A2 pat q(true) B (iIntroCore · · pats k) + | throwError "{tacName}: {A1} not affine and the goal not absorbing" + let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf) | _, some _ => -- should always succeed let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1) let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) - | throwError "iintro: {A1} is not persistent and spatial context is non-empty" - let pf ← iCasesCore hyps A2 pat q(false) B (iIntroCore · · pats k) + | throwError "{tacName}: {A1} is not persistent and spatial context is non-empty" + let pf ← iCasesCore hyps A2 pat q(false) B tacName (iIntroCore · · pats tacName k) return q(imp_intro_spatial (Q := $Q) $pf) | _, none => let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) - | throwError "iintro: {Q} not a wand" - let pf ← iCasesCore hyps A2 pat q(false) A1 (iIntroCore · · pats k) + | throwError "{tacName}: {Q} not a wand" + let pf ← iCasesCore hyps A2 pat q(false) A1 tacName (iIntroCore · · pats tacName k) return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf) /-- @@ -217,6 +218,6 @@ elab "iintro " pats:(colGt ppSpace introPat)* : tactic => do let pats ← liftMacroM <| pats.mapM <| IntroPat.parse ProofModeM.runTactic λ mvar { hyps, goal, .. } => do - let pf ← iIntroCore hyps goal pats.toList + let pf ← iIntroCore hyps goal pats.toList "iintro" mvar.assign pf diff --git a/Iris/Iris/ProofMode/Tactics/Loeb.lean b/Iris/Iris/ProofMode/Tactics/Loeb.lean index 06f28ca2a..fb4182751 100644 --- a/Iris/Iris/ProofMode/Tactics/Loeb.lean +++ b/Iris/Iris/ProofMode/Tactics/Loeb.lean @@ -23,15 +23,15 @@ elab "iloeb" " as " colGt IH:binderIdent " generalizing " hs:(colGt ppSpace selP let pats ← Elab.liftMacroM <| SelPat.parse hs ProofModeM.runTactic fun mvid {hyps, goal, ..} => do let targets : List SelTarget ← SelPat.resolve hyps (pats ++ [.spatial]) - let expr ← iRevertIntro hyps goal targets fun {prop _ _} hyps goal k => do + let expr ← iRevertIntro hyps goal targets "iloeb" fun {prop _ _} hyps goal k => do let some _ ← ProofModeM.trySynthInstanceQ q(BI.BILoeb $prop) | throwError m!"iloeb: no `{←ppExpr q(BI.BILoeb $prop)}` instance found" let pf := q(BI.loeb_wand_intuitionistically (P := $goal)) let pf' ← do -- We have applied BI.loeb_wand_intuitionistically let goal := q(iprop(□ (□ ▷ $goal -∗ $goal))) - iModIntroCore hyps goal (← `(_)) fun hyps goal => do - iIntroCore hyps goal [(IH, .intro <| .intuitionistic <| .one IH)] k + iModIntroCore hyps goal (← `(_)) "iloeb" fun hyps goal => do + iIntroCore hyps goal [(IH, .intro <| .intuitionistic <| .one IH)] "iloeb" k return q($(pf').trans $pf) mvid.assign expr diff --git a/Iris/Iris/ProofMode/Tactics/ModIntro.lean b/Iris/Iris/ProofMode/Tactics/ModIntro.lean index 9ac73cfde..9044f765f 100644 --- a/Iris/Iris/ProofMode/Tactics/ModIntro.lean +++ b/Iris/Iris/ProofMode/Tactics/ModIntro.lean @@ -159,7 +159,8 @@ where go {e} # Returns Proof term of `hyps ⊢ goal` -/ -def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSyntax `term) +def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) + (sel : TSyntax `term) (tacName : String) (k : ∀ {prop' bi' P}, @Hyps u prop' bi' P → ∀ Q : Q($prop'), ProofModeM Q($P ⊢ $Q) := addBIGoal) : ProofModeM (Q($e ⊢ $goal)) := do let prop' : Q(Type u) ← mkFreshExprMVarQ q(Type u) @@ -170,7 +171,7 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta let Q ← mkFreshExprMVarQ q($prop') -- `M Q ⊢ goal` let .some _ ← ProofModeM.trySynthInstanceQ q(@FromModal $prop' $prop $bi' $bi $Φ $M $sel $goal $Q) - | throwError "imodintro: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}" + | throwError "{tacName}: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}" -- show the side condition let hΦ ← iSolveSidecondition q($Φ) -- perform modality actions, get transformed context `hyps'` and `pf : hyps ⊢ M hyps'` @@ -186,7 +187,7 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta -/ elab "imodintro " colGt sel:term : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do - let pf ← iModIntroCore hyps goal sel + let pf ← iModIntroCore hyps goal sel "imodintro" mvar.assign pf diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean index 4b16f1196..8d0a880eb 100644 --- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean +++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean @@ -20,7 +20,7 @@ abbrev ProofModeContinuation := def iRevertIntro {prop: Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (hyps : Hyps bi e) (goal: Q($prop)) - (hs : List SelTarget) + (hs : List SelTarget) (tacName : String) (k : ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (_hyps : Hyps bi e) (goal: Q($prop)), ProofModeContinuation → ProofModeM Q($e ⊢ $goal)) @@ -37,6 +37,6 @@ def iRevertIntro trace[irevertintro] s!"Calling `iRevertIntro` with {names.map (·.1)} on context {←ppExpr <| IrisGoal.toExpr {hyps, goal ..}}" iRevertCore hs hyps goal fun hyps goal => do k hyps goal fun hyps goal => do - iIntroCore hyps goal names + iIntroCore hyps goal names tacName initialize registerTraceClass `irevertintro From 4b74264fdbe85befdee5d3c115c11401efa58d95 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:45:45 +0200 Subject: [PATCH 35/53] Pretty printing with `ppSpace` --- Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 2 +- Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index f56c955aa..2f719d310 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -27,7 +27,7 @@ syntax "//=" : introPat syntax "*" : introPat syntax "**" : introPat syntax "!%" : introPat -syntax "{" (colGt selPatFrame)* "}" : introPat +syntax "{" (colGt ppSpace selPatFrame)* ppSpace "}" : introPat @[rocq_alias intro_pat] inductive IntroPat diff --git a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean index 73eec6df9..468c94eb3 100644 --- a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean +++ b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean @@ -16,7 +16,7 @@ open Lean declare_syntax_cat pmTerm syntax term : pmTerm -syntax term colGt " $$ " (colGt specPat)+ : pmTerm +syntax term colGt " $$ " (colGt ppSpace specPat)+ : pmTerm @[rocq_alias iTrm] structure PMTerm where From fc64e9c96e4e392348fd282159e3dff3b4016274 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 10:59:17 +0200 Subject: [PATCH 36/53] Refactor `iIntroCoreForallIntro` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 32 +++++++++++--------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 8a8fe657e..77c567081 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -63,10 +63,11 @@ open Lean Elab Tactic Meta Qq BI Std `.all` and `.allwand`. -/ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} - {P : Q($prop)} (ref : Syntax) (n : Name) (Q : Q($prop)) (tacName : String) - (k' : Option <| ProofModeM Q($P ⊢ $Q)) - (k : Expr → Q($prop) → ProofModeM Expr) : + {P : Q($prop)} (ref : Syntax) (n : Option <| TSyntax ``binderIdent) + (Q : Q($prop)) (tacName : String) (k' : Option <| ProofModeM Q($P ⊢ $Q)) + (k : Q($prop) → (B : Q($prop)) → ProofModeM Q($P ⊢ $B)) : ProofModeM Q($P ⊢ $Q) := do + let ⟨n, _⟩ ← getFreshName <| n.getD (← `(binderIdent| _)) withRef ref do let v ← mkFreshLevelMVar let α ← mkFreshExprMVarQ q(Sort v) @@ -79,8 +80,7 @@ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} withLocalDeclDQ n α fun x => do addLocalVarInfo ref (← getLCtx) x α have B : Q($prop) := Expr.headBeta q($Φ $x) - have : $B =Q $Φ $x := ⟨⟩ - let pf : Q(∀ x, $P ⊢ $Φ x) ← k x B + let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← k x B return q(from_forall_intro $pf) /-- @@ -115,15 +115,13 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) tacName k | (ref, .all) :: pats => withRef ref do - let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro ref n Q tacName + iIntroCoreForallIntro ref none Q tacName -- No more universally quantified variable to be introduced (iIntroCore hyps Q pats tacName k) -- Introduction of a universally quantified variable - (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .all) :: pats) tacName k) + (fun _ B => iIntroCore hyps B ((ref, .all) :: pats) tacName k) | (ref, .allwand) :: pats => withRef ref do - let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) let k' : ProofModeM Q($P ⊢ $Q) := do let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) @@ -137,9 +135,9 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | _, _, _ => -- No more universally quantified variable or premise to be introduced iIntroCore hyps Q pats tacName k - iIntroCoreForallIntro ref n Q tacName k' - -- Introduction of a universally quantified variable - (do mkLambdaFVars #[·] <|← iIntroCore hyps · ((ref, .allwand) :: pats) tacName k) + -- Introduction of a universally quantified variable + iIntroCoreForallIntro ref none Q tacName k' + (fun _ B => iIntroCore hyps B ((ref, .allwand) :: pats) tacName k) | (ref, .pureintro) :: pats => withRef ref do let ⟨pf, m⟩ ← iPureIntroCore bi P Q tacName @@ -163,15 +161,11 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) | (ref, .intro (.rewrite direction)) :: pats => withRef ref do - let ⟨n, _⟩ ← getFreshName (← `(binderIdent| _)) - iIntroCoreForallIntro ref n Q tacName none <| - fun x B => do mkLambdaFVars #[x] <|← - iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) + iIntroCoreForallIntro ref none Q tacName none <| + fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) | (ref, .intro (.pure n)) :: pats => withRef ref do - let ⟨n, _⟩ ← getFreshName n - iIntroCoreForallIntro ref n Q tacName none <| - (do mkLambdaFVars #[·] <|← iIntroCore hyps · pats tacName k) + iIntroCoreForallIntro ref n Q tacName none (fun _ B => iIntroCore hyps B pats tacName k) | (ref, .intro pat) :: pats => withRef ref do let A1 ← mkFreshExprMVarQ q($prop) From 8c7852e41343e87a48f3fcd7fa842fa8b8a6bd64 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 11:17:57 +0200 Subject: [PATCH 37/53] Simplify `iIntroCore` to avoid repetitive `withRef ref do ...` --- Iris/Iris/ProofMode/Tactics/Intro.lean | 226 ++++++++++++------------- 1 file changed, 108 insertions(+), 118 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 77c567081..a643a2d12 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -68,20 +68,19 @@ private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (k : Q($prop) → (B : Q($prop)) → ProofModeM Q($P ⊢ $B)) : ProofModeM Q($P ⊢ $Q) := do let ⟨n, _⟩ ← getFreshName <| n.getD (← `(binderIdent| _)) - withRef ref do - let v ← mkFreshLevelMVar - let α ← mkFreshExprMVarQ q(Sort v) - let Φ ← mkFreshExprMVarQ q($α → $prop) - match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ), k' with - | none, none => - throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" - | none, some k' => k' - | some _, _ => - withLocalDeclDQ n α fun x => do - addLocalVarInfo ref (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← k x B - return q(from_forall_intro $pf) + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ), k' with + | none, none => + throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" + | none, some k' => k' + | some _, _ => + withLocalDeclDQ n α fun x => do + addLocalVarInfo ref (← getLCtx) x α + have B : Q($prop) := Expr.headBeta q($Φ $x) + let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← k x B + return q(from_forall_intro $pf) /-- Introduce the hypothesis specified by `pats` into the context given by `P` (structured as `hyps`). @@ -96,113 +95,104 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} ProofModeM (Q($P ⊢ $Q)) := do match pats with | [] => k hyps Q - | (ref, .modintro) :: pats => - withRef ref do - iModIntroCore hyps Q (← `(_)) tacName (iIntroCore · · pats tacName k) - | (ref, .trivial) :: pats => - withRef ref do - if let some r ← iTrivial hyps Q then - return r - else - iIntroCore hyps Q pats tacName k - | (ref, .simp) :: pats => - withRef ref do - let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems]) - let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] - iIntroCore hyps Q' pats tacName k - | (ref, .simptrivial) :: pats => - withRef ref do - iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) tacName k - | (ref, .all) :: pats => - withRef ref do - iIntroCoreForallIntro ref none Q tacName - -- No more universally quantified variable to be introduced - (iIntroCore hyps Q pats tacName k) + | (ref, pat) :: pats => + withRef ref do match pat with + | .modintro => + iModIntroCore hyps Q (← `(_)) tacName (iIntroCore · · pats tacName k) + | .trivial => + if let some r ← iTrivial hyps Q then + return r + else + iIntroCore hyps Q pats tacName k + | .simp => + let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems]) + let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs] + iIntroCore hyps Q' pats tacName k + | .simptrivial => + iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) tacName k + | .all => + iIntroCoreForallIntro ref none Q tacName + -- No more universally quantified variable to be introduced + (iIntroCore hyps Q pats tacName k) + -- Introduction of a universally quantified variable + (fun _ B => iIntroCore hyps B ((ref, .all) :: pats) tacName k) + | .allwand => + let k' : ProofModeM Q($P ⊢ $Q) := do + let A1 ← mkFreshExprMVarQ q($prop) + let A2 ← mkFreshExprMVarQ q($prop) + let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) + let instFromWand ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) + let instPersistent ← ProofModeM.trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) + match instFromWand, instFromImp, instPersistent with + -- Introduction of a wand premise or a pure premise, if possible + | some _, _, _ | _, some _, some _ => + iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k + | _, _, _ => + -- No more universally quantified variable or premise to be introduced + iIntroCore hyps Q pats tacName k -- Introduction of a universally quantified variable - (fun _ B => iIntroCore hyps B ((ref, .all) :: pats) tacName k) - | (ref, .allwand) :: pats => - withRef ref do - let k' : ProofModeM Q($P ⊢ $Q) := do + iIntroCoreForallIntro ref none Q tacName k' + (fun _ B => iIntroCore hyps B ((ref, .allwand) :: pats) tacName k) + | .pureintro => + let ⟨pf, m⟩ ← iPureIntroCore bi P Q tacName + if pats.isEmpty then + addMVarGoal m + else + let ⟨newM, g⟩ ← startProofMode m + let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats tacName k + newM.assign pf' + return pf + | .clear selPats => + match selPats with + | [] => iIntroCore hyps Q pats tacName k + | ⟨false, s⟩ :: selPats => + iClearCore hyps Q [s] + fun hyps' goal' fvars => withoutFVars (u := 0) fvars + <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) tacName k + | ⟨true, s⟩ :: selPats => + let res ← s.resolveOne hyps >>= iFrame hyps Q + res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) + | .intro (.rewrite direction) => + iIntroCoreForallIntro ref none Q tacName none <| + fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) + | .intro (.pure n) => + iIntroCoreForallIntro ref n Q tacName none (fun _ B => iIntroCore hyps B pats tacName k) + | .intro pat => let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) - let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) - let instFromWand ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) - let instPersistent ← ProofModeM.trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) - match instFromWand, instFromImp, instPersistent with - -- Introduction of a wand premise or a pure premise, if possible - | some _, _, _ | _, some _, some _ => - iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k - | _, _, _ => - -- No more universally quantified variable or premise to be introduced - iIntroCore hyps Q pats tacName k - -- Introduction of a universally quantified variable - iIntroCoreForallIntro ref none Q tacName k' - (fun _ B => iIntroCore hyps B ((ref, .allwand) :: pats) tacName k) - | (ref, .pureintro) :: pats => - withRef ref do - let ⟨pf, m⟩ ← iPureIntroCore bi P Q tacName - if pats.isEmpty then - addMVarGoal m - else - let ⟨newM, g⟩ ← startProofMode m - let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats tacName k - newM.assign pf' - return pf - | (ref, .clear selPats) :: pats => - withRef ref do - match selPats with - | [] => iIntroCore hyps Q pats tacName k - | ⟨false, s⟩ :: selPats => - iClearCore hyps Q [s] - fun hyps' goal' fvars => withoutFVars (u := 0) fvars - <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) tacName k - | ⟨true, s⟩ :: selPats => - let res ← s.resolveOne hyps >>= iFrame hyps Q - res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) - | (ref, .intro (.rewrite direction)) :: pats => - withRef ref do - iIntroCoreForallIntro ref none Q tacName none <| - fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) - | (ref, .intro (.pure n)) :: pats => - withRef ref do - iIntroCoreForallIntro ref n Q tacName none (fun _ B => iIntroCore hyps B pats tacName k) - | (ref, .intro pat) :: pats => - withRef ref do - let A1 ← mkFreshExprMVarQ q($prop) - let A2 ← mkFreshExprMVarQ q($prop) - let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) - if let (.clear, some _) := (pat, fromImp) then - let pf ← iIntroCore hyps A2 pats tacName k - return q(imp_intro_drop (Q := $Q) $pf) - else - let B ← mkFreshExprMVarQ q($prop) - match pat, fromImp with - | .intuitionistic pat, some _ => - let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) - | throwError "{tacName}: {A1} not persistent" - let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) - return q(imp_intro_intuitionistic (Q := $Q) $pf) - | .intuitionistic pat, none => - let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) - | throwError "{tacName}: {Q} not a wand" - let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) - | throwError "{tacName}: {A1} not persistent" - let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2)) - | throwError "{tacName}: {A1} not affine and the goal not absorbing" - let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) - return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf) - | _, some _ => - -- should always succeed - let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1) - let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) - | throwError "{tacName}: {A1} is not persistent and spatial context is non-empty" - let pf ← iCasesCore hyps A2 pat q(false) B tacName (iIntroCore · · pats tacName k) - return q(imp_intro_spatial (Q := $Q) $pf) - | _, none => - let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) - | throwError "{tacName}: {Q} not a wand" - let pf ← iCasesCore hyps A2 pat q(false) A1 tacName (iIntroCore · · pats tacName k) - return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf) + let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) + if let (.clear, some _) := (pat, fromImp) then + let pf ← iIntroCore hyps A2 pats tacName k + return q(imp_intro_drop (Q := $Q) $pf) + else + let B ← mkFreshExprMVarQ q($prop) + match pat, fromImp with + | .intuitionistic pat, some _ => + let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) + | throwError "{tacName}: {A1} not persistent" + let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) + return q(imp_intro_intuitionistic (Q := $Q) $pf) + | .intuitionistic pat, none => + let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) + | throwError "{tacName}: {Q} not a wand" + let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) + | throwError "{tacName}: {A1} not persistent" + let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2)) + | throwError "{tacName}: {A1} not affine and the goal not absorbing" + let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) + return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf) + | _, some _ => + -- should always succeed + let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1) + let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P)) + | throwError "{tacName}: {A1} is not persistent and spatial context is non-empty" + let pf ← iCasesCore hyps A2 pat q(false) B tacName (iIntroCore · · pats tacName k) + return q(imp_intro_spatial (Q := $Q) $pf) + | _, none => + let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) + | throwError "{tacName}: {Q} not a wand" + let pf ← iCasesCore hyps A2 pat q(false) A1 tacName (iIntroCore · · pats tacName k) + return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf) /-- `iintro pats` introduces hypotheses using the introduction pattern `pats`. From 26fb3070ab5f7629ebb8840549cec1a0e208d00f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 11:56:37 +0200 Subject: [PATCH 38/53] Attach `ref : Syntax` to `iCasesPat` for more precise syntax highlighting, TODO solved --- .../Iris/ProofMode/Patterns/CasesPattern.lean | 68 ++++++++++--------- Iris/Iris/ProofMode/Tactics/Cases.lean | 43 ++++++------ Iris/Iris/ProofMode/Tactics/Combine.lean | 2 +- Iris/Iris/ProofMode/Tactics/Intro.lean | 12 ++-- Iris/Iris/ProofMode/Tactics/Loeb.lean | 2 +- Iris/Iris/ProofMode/Tactics/RevertIntro.lean | 4 +- Iris/Iris/ProofMode/Tactics/Specialize.lean | 2 +- 7 files changed, 71 insertions(+), 62 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index be684aa10..429c86002 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -26,44 +26,50 @@ syntax ">" icasesPat : icasesPat syntax "←" : icasesPat syntax "→" : icasesPat --- TODO: attach syntax to iCasesPat such that one can use withRef to --- associate the errors with the right part of the syntax inductive iCasesPat - | one (name : TSyntax ``binderIdent) - | clear - | frame - | conjunction (args : List iCasesPat) - | disjunction (args : List iCasesPat) - | pure (pat : TSyntax ``binderIdent) - | intuitionistic (pat : iCasesPat) - | spatial (pat : iCasesPat) - | mod (pat : iCasesPat) - | rewrite (forward : Bool) + | one (ref : Syntax) (name : TSyntax ``binderIdent) + | clear (ref : Syntax) + | frame (ref : Syntax) + | conjunction (ref : Syntax) (args : List iCasesPat) + | disjunction (ref : Syntax) (args : List iCasesPat) + | pure (ref : Syntax) (pat : TSyntax ``binderIdent) + | intuitionistic (ref : Syntax) (pat : iCasesPat) + | spatial (ref : Syntax) (pat : iCasesPat) + | mod (ref : Syntax) (pat : iCasesPat) + | rewrite (ref : Syntax) (forward : Bool) deriving Repr, Inhabited +def iCasesPat.ref : iCasesPat → Syntax + | .one r _ | .clear r | .frame r | .conjunction r _ | .disjunction r _ + | .pure r _ | .intuitionistic r _ | .spatial r _ | .mod r _ | .rewrite r _ => r + partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do match go ⟨← expandMacros pat⟩ with | none => Macro.throwUnsupported | some pat => return pat where - go : TSyntax `icasesPat → Option iCasesPat - | `(icasesPat| $name:binderIdent) => some <| .one name - | `(icasesPat| -) => some <| .clear - | `(icasesPat| $) => some <| .frame - | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList) - | `(icasesPat| %$pat:binderIdent) => some <| .pure pat - | `(icasesPat| #$pat) => go pat |>.map .intuitionistic - | `(icasesPat| ∗$pat) => go pat |>.map .spatial - | `(icasesPat| >$pat) => go pat |>.map .mod - | `(icasesPat| ($pat)) => goAlts pat - | `(icasesPat| ←) => some <| .rewrite false - | `(icasesPat| →) => some <| .rewrite true - | _ => none - goAlts : TSyntax ``icasesPatAlts → Option iCasesPat - | `(icasesPatAlts| $args|*) => - match args.getElems with - | #[arg] => go arg - | args => args.mapM go |>.map (.disjunction ·.toList) - | _ => none + go (stx : TSyntax `icasesPat) : Option iCasesPat := + let ref := stx.raw + match ref with + | `(icasesPat| $name:binderIdent) => some <| .one ref name + | `(icasesPat| -) => some <| .clear ref + | `(icasesPat| $) => some <| .frame ref + | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ref ·.toList) + | `(icasesPat| %$pat:binderIdent) => some <| .pure ref pat + | `(icasesPat| #$pat) => go pat |>.map <| .intuitionistic ref + | `(icasesPat| ∗$pat) => go pat |>.map <| .spatial ref + | `(icasesPat| >$pat) => go pat |>.map <| .mod ref + | `(icasesPat| ($pat)) => goAlts pat + | `(icasesPat| ←) => some <| .rewrite ref false + | `(icasesPat| →) => some <| .rewrite ref true + | _ => none + goAlts (stx : TSyntax ``icasesPatAlts) : Option iCasesPat := + let ref := stx.raw + match stx with + | `(icasesPatAlts| $args|*) => + match args.getElems with + | #[arg] => go arg + | args => args.mapM go |>.map (.disjunction ref ·.toList) + | _ => none end Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 4fcf15776..f69cf9101 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -222,7 +222,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal') := addBIGoal) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := match pat with - | .one name => do + | .one ref name => withRef ref do -- TODO: use Hyps.addWithInfo here? let (name, ref) ← getFreshName name let ivar ← mkFreshIVarId (isTrue p) @@ -231,53 +231,56 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} if let .emp _ := hyps then pure q(of_emp_sep $(← k hyp goal)) else k (.mkSep hyps hyp) goal - | .clear => do + | .clear ref => withRef ref do let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) tacName pure q($pf $(← k hyps goal)) - | .frame => do + | .frame ref => do + withRef ref do let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩] res.finish k - | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A tacName k + | .conjunction ref [arg] | .disjunction ref [arg] => + withRef ref do + iCasesCore hyps goal arg p A tacName k - | .disjunction [] => throwUnsupportedSyntax + | .disjunction ref [] => withRef ref do throwUnsupportedSyntax - | .conjunction [] => iCasesEmptyConj bi hyps p A goal tacName + | .conjunction ref [] => withRef ref do iCasesEmptyConj bi hyps p A goal tacName -- pure conjunctions are always handled as existentials. There is `intoExist_and_pure` and -- `intoExist_sep_pure` to make this work as expected for pure assertions that are not explicit existentials. - | .conjunction (.pure arg :: args) => do - iCasesExists bi arg p P A goal tacName (iCasesCore hyps goal (.conjunction args) p · tacName k) - | .conjunction (arg :: args) => do - if arg matches .clear then + | .conjunction ref (.pure _ arg :: args) => do + iCasesExists bi arg p P A goal tacName (iCasesCore hyps goal (.conjunction ref args) p · tacName k) + | .conjunction ref (arg :: args) => withRef ref do + if arg matches .clear _ then if let some pf ← iCasesAndLR bi p P A goal true λ B => - iCasesCore hyps goal (.conjunction args) p B tacName k then return pf - if args matches [.clear] then + iCasesCore hyps goal (.conjunction ref args) p B tacName k then return pf + if args matches [.clear _] then if let some pf ← iCasesAndLR bi p P A goal false λ B => iCasesCore hyps goal arg p B tacName k then return pf iCasesSep bi hyps p A goal tacName k (iCasesCore · · arg p · tacName ·) - (iCasesCore · · (.conjunction args) p · tacName ·) + (iCasesCore · · (.conjunction ref args) p · tacName ·) - | .disjunction (arg :: args) => + | .disjunction ref (arg :: args) => withRef ref do iCasesOr bi p P A goal tacName (iCasesCore hyps goal arg p · tacName k) - (iCasesCore hyps goal (.disjunction args) p · tacName k) + (iCasesCore hyps goal (.disjunction ref args) p · tacName k) - | .pure arg => do + | .pure ref arg => withRef ref do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal - | .intuitionistic arg => + | .intuitionistic ref arg => withRef ref do iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) - | .spatial arg => + | .spatial ref arg => withRef ref do iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · tacName k) - | .mod arg => + | .mod ref arg => withRef ref do iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A tacName k - | .rewrite direction => do + | .rewrite ref direction => withRef ref do iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) <| fun _ h => iCasesPureRewrite hyps goal h direction tacName k diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index eea53aa54..1fdd2cdbe 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -282,7 +282,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)* match st.outGives, st.pfGives with | some outGives, pfGives => - let pf ← iCasesCore st.newHyps goal (.conjunction [pat1, .intuitionistic pat2]) + let pf ← iCasesCore st.newHyps goal (.conjunction pat1.ref [pat1, .intuitionistic pat2.ref pat2]) q($st.p) q(iprop($st.outAs ∗ □ $outGives)) "icombine" mvar.assign q(combine_as_gives $st.pfAs $pfGives $pf) | none, _ => throwNoInstanceForGives diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index a643a2d12..63b872e6c 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -126,7 +126,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} match instFromWand, instFromImp, instPersistent with -- Introduction of a wand premise or a pure premise, if possible | some _, _, _ | _, some _, some _ => - iIntroCore hyps Q ((ref, .intro (.one (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k + iIntroCore hyps Q ((ref, .intro (.one ref (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k | _, _, _ => -- No more universally quantified variable or premise to be introduced iIntroCore hyps Q pats tacName k @@ -152,27 +152,27 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | ⟨true, s⟩ :: selPats => let res ← s.resolveOne hyps >>= iFrame hyps Q res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) - | .intro (.rewrite direction) => + | .intro (.rewrite _ direction) => iIntroCoreForallIntro ref none Q tacName none <| fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) - | .intro (.pure n) => + | .intro (.pure _ n) => iIntroCoreForallIntro ref n Q tacName none (fun _ B => iIntroCore hyps B pats tacName k) | .intro pat => let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2) - if let (.clear, some _) := (pat, fromImp) then + if let (.clear _, some _) := (pat, fromImp) then let pf ← iIntroCore hyps A2 pats tacName k return q(imp_intro_drop (Q := $Q) $pf) else let B ← mkFreshExprMVarQ q($prop) match pat, fromImp with - | .intuitionistic pat, some _ => + | .intuitionistic _ pat, some _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) | throwError "{tacName}: {A1} not persistent" let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k) return q(imp_intro_intuitionistic (Q := $Q) $pf) - | .intuitionistic pat, none => + | .intuitionistic _ pat, none => let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2) | throwError "{tacName}: {Q} not a wand" let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B) diff --git a/Iris/Iris/ProofMode/Tactics/Loeb.lean b/Iris/Iris/ProofMode/Tactics/Loeb.lean index fb4182751..be5cebbd0 100644 --- a/Iris/Iris/ProofMode/Tactics/Loeb.lean +++ b/Iris/Iris/ProofMode/Tactics/Loeb.lean @@ -31,7 +31,7 @@ elab "iloeb" " as " colGt IH:binderIdent " generalizing " hs:(colGt ppSpace selP -- We have applied BI.loeb_wand_intuitionistically let goal := q(iprop(□ (□ ▷ $goal -∗ $goal))) iModIntroCore hyps goal (← `(_)) "iloeb" fun hyps goal => do - iIntroCore hyps goal [(IH, .intro <| .intuitionistic <| .one IH)] "iloeb" k + iIntroCore hyps goal [(IH, .intro <| .intuitionistic IH <| .one IH IH)] "iloeb" k return q($(pf').trans $pf) mvid.assign expr diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean index 8d0a880eb..1c710b2db 100644 --- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean +++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean @@ -29,11 +29,11 @@ def iRevertIntro | {kind := .pure id, ..} => do let name ← Lean.mkIdent <$> id.getUserName let ident ← `(binderIdent| $name:ident) - return (name, .intro <| .pure ident) + return (name, .intro <| .pure ident ident) | {kind := .ipm ivar, ..} => do let name ← Lean.mkIdent <$> (hyps.getUserName? ivar).getM let ident ← `(binderIdent| $name:ident) - return (name, .intro <| (if ivar.persistent? then .intuitionistic else id) <| .one ident) + return (name, .intro <| (if ivar.persistent? then .intuitionistic ident else id) <| .one ident ident) trace[irevertintro] s!"Calling `iRevertIntro` with {names.map (·.1)} on context {←ppExpr <| IrisGoal.toExpr {hyps, goal ..}}" iRevertCore hs hyps goal fun hyps goal => do k hyps goal fun hyps goal => do diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean index e46032fbe..687b8ce8d 100644 --- a/Iris/Iris/ProofMode/Tactics/Specialize.lean +++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean @@ -141,7 +141,7 @@ TODO: This also needs to check that there are no modality addition patterns in ` @[rocq_alias intro_pat_intuitionistic, rocq_alias use_tac_specialize_intuitionistic_helper] def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool := match pat with - | .intuitionistic _ | .pure _ | .rewrite _ => true + | .intuitionistic _ _ | .pure _ _ | .rewrite _ _ => true | _ => false /-- Specialize a proposition `A` by applying a sequence of specialization patterns. From caf2446d797e03f9ca90c7c83955ec19e08a184a Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 12:30:42 +0200 Subject: [PATCH 39/53] Refactor usage of `withRef` in `iCasesCore` --- Iris/Iris/ProofMode/Tactics/Cases.lean | 37 +++++++++++++------------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index f69cf9101..1d37e72c2 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -183,12 +183,12 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) removing `h` from the context afterwards. -/ def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} - (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (direction : Bool) (tacName : String) + (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (forward : Bool) (tacName : String) (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : ProofModeM Q($e ⊢ $goal) := do let target := q($(hyps.tm) ⊢ $goal) let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!) - let ⟨newE, eq, []⟩ ← g.rewrite target h (symm := !direction) + let ⟨newE, eq, []⟩ ← g.rewrite target h !forward | throwError "{tacName}: rewriting should not give additional subgoals" let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails | throwError "{tacName}: unable to parse the Iris entailment {newE}" @@ -221,8 +221,9 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (p : Q(Bool)) (A : Q($prop)) (tacName : String) (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal') := addBIGoal) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := + withRef pat.ref do match pat with - | .one ref name => withRef ref do + | .one _ name => do -- TODO: use Hyps.addWithInfo here? let (name, ref) ← getFreshName name let ivar ← mkFreshIVarId (isTrue p) @@ -231,29 +232,27 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} if let .emp _ := hyps then pure q(of_emp_sep $(← k hyp goal)) else k (.mkSep hyps hyp) goal - | .clear ref => withRef ref do + | .clear _ => let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) tacName pure q($pf $(← k hyps goal)) - | .frame ref => do - withRef ref do + | .frame _ => let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩] res.finish k - | .conjunction ref [arg] | .disjunction ref [arg] => - withRef ref do + | .conjunction _ [arg] | .disjunction _ [arg] => iCasesCore hyps goal arg p A tacName k - | .disjunction ref [] => withRef ref do throwUnsupportedSyntax + | .disjunction _ [] => throwUnsupportedSyntax - | .conjunction ref [] => withRef ref do iCasesEmptyConj bi hyps p A goal tacName + | .conjunction _ [] => iCasesEmptyConj bi hyps p A goal tacName -- pure conjunctions are always handled as existentials. There is `intoExist_and_pure` and -- `intoExist_sep_pure` to make this work as expected for pure assertions that are not explicit existentials. - | .conjunction ref (.pure _ arg :: args) => do + | .conjunction ref (.pure _ arg :: args) => iCasesExists bi arg p P A goal tacName (iCasesCore hyps goal (.conjunction ref args) p · tacName k) - | .conjunction ref (arg :: args) => withRef ref do + | .conjunction ref (arg :: args) => if arg matches .clear _ then if let some pf ← iCasesAndLR bi p P A goal true λ B => iCasesCore hyps goal (.conjunction ref args) p B tacName k then return pf @@ -263,26 +262,26 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} iCasesSep bi hyps p A goal tacName k (iCasesCore · · arg p · tacName ·) (iCasesCore · · (.conjunction ref args) p · tacName ·) - | .disjunction ref (arg :: args) => withRef ref do + | .disjunction ref (arg :: args) => iCasesOr bi p P A goal tacName (iCasesCore hyps goal arg p · tacName k) (iCasesCore hyps goal (.disjunction ref args) p · tacName k) - | .pure ref arg => withRef ref do + | .pure _ arg => iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal - | .intuitionistic ref arg => withRef ref do + | .intuitionistic _ arg => iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) - | .spatial ref arg => withRef ref do + | .spatial _ arg => iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · tacName k) - | .mod ref arg => withRef ref do + | .mod _ arg => iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A tacName k - | .rewrite ref direction => withRef ref do + | .rewrite _ forward => iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) - <| fun _ h => iCasesPureRewrite hyps goal h direction tacName k + <| fun _ h => iCasesPureRewrite hyps goal h forward tacName k /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. From 4afdba461c076cfd35ad90d696d32902ec8d468b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 13:02:01 +0200 Subject: [PATCH 40/53] Add docstrings to `syntax` declarations for pop-up information upon hovering --- Iris/Iris/ProofMode/Patterns/CasesPattern.lean | 13 +++++++++++++ Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 12 ++++++++++++ Iris/Iris/ProofMode/Patterns/SelPattern.lean | 4 ++++ 3 files changed, 29 insertions(+) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index 429c86002..5e159a181 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -15,15 +15,28 @@ open Lean declare_syntax_cat icasesPat syntax icasesPatAlts := sepBy1(icasesPat, " | ") syntax binderIdent : icasesPat +/-- Drop the hypothesis. -/ syntax "-" : icasesPat +/-- Frame the hypothesis and cancel it against the goal. -/ syntax "$" : icasesPat +/-- + Destruct a (separating) conjunction or existential; an existential variable is + bound with `%x` where `x` is the name for it. +-/ syntax "⟨" icasesPatAlts,* "⟩" : icasesPat +/-- Destruct a disjunction, one goal per disjunct. -/ syntax "(" icasesPatAlts ")" : icasesPat +/-- Move the hypothesis to the pure Lean context and give it a name. -/ syntax "%" binderIdent : icasesPat +/-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/ syntax "#" icasesPat : icasesPat +/-- Move the hypothesis to the spatial context and destruct the proposition. -/ syntax "∗" icasesPat : icasesPat +/-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/ syntax ">" icasesPat : icasesPat +/-- Introduce a pure equality and use it for rewriting in the backward direction. -/ syntax "←" : icasesPat +/-- Introduce a pure equality and use it for rewriting in the forward direction. -/ syntax "→" : icasesPat inductive iCasesPat diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index 2f719d310..59f2b99b4 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -20,13 +20,25 @@ syntax ("!" noWs)? selPat : selPatFrame declare_syntax_cat introPat syntax icasesPat : introPat +/-- Introduce a modality, analogous to applying `imodintro`. -/ syntax "!>" : introPat +/-- Try to solve the goal using `itrivial`. -/ syntax "//" : introPat +/-- Apply simplification. -/ syntax "/=" : introPat +/-- Apply simplifcation (`/=`) and try solving the goal (`//`). -/ syntax "//=" : introPat +/-- Introduce all universal quantifiers. -/ syntax "*" : introPat +/-- Introduce all universal quantifiers, pure arrows and wands. -/ syntax "**" : introPat +/-- Introduces a pure proof goal, analogous to applying `ipureintro`. -/ syntax "!%" : introPat +/-- + Given selection patterns `spats`, the introduction pattern `{ spats }` + *clears* the hypotheses chosen by `spats`. Prefix an element in the selection + patterns with `!` to *frame* the hypotheses instead. +-/ syntax "{" (colGt ppSpace selPatFrame)* ppSpace "}" : introPat @[rocq_alias intro_pat] diff --git a/Iris/Iris/ProofMode/Patterns/SelPattern.lean b/Iris/Iris/ProofMode/Patterns/SelPattern.lean index 94c4f2c26..8449df66a 100644 --- a/Iris/Iris/ProofMode/Patterns/SelPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SelPattern.lean @@ -15,9 +15,13 @@ open Lean Meta Std declare_syntax_cat selPat syntax ident : selPat +/-- Choose all hypothesis from the pure context. -/ syntax "%" : selPat +/-- Choose a specific hypothesis from the pure context. -/ syntax "%" noWs ident : selPat +/-- Choose all hypotheses in the intuitionistic context. -/ syntax "#" : selPat +/-- Choose all hypotheses in the spatial context. -/ syntax "∗" : selPat @[rocq_alias sel_pat] From 852a7906f79d260f376a1604589d844e09789df2 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 13:13:31 +0200 Subject: [PATCH 41/53] Update Porting.lean --- Iris/Iris/ProofMode/Porting.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index dad0da8f9..14467db31 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -59,7 +59,7 @@ import Iris.Std.RocqPorting #rocq_concept proofmode "Tactics" "iAccu" missing "" #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial" -#rocq_concept proofmode "Intro Patterns" missing "" +#rocq_concept proofmode "Intro Patterns" ported "" #rocq_concept proofmode "Intro Patterns" "IIdent (pattern: H)" ported "pattern: H" #rocq_concept proofmode "Intro Patterns" "IFresh (pattern: ?)" ported "pattern: _" #rocq_concept proofmode "Intro Patterns" "IDrop (pattern: _)" ported "pattern: -" @@ -70,15 +70,15 @@ import Iris.Std.RocqPorting #rocq_concept proofmode "Intro Patterns" "IIntuitionistic (pattern: #H)" ported "pattern: #H" #rocq_concept proofmode "Intro Patterns" "ISpatial (pattern: -#H)" ported "pattern: ∗H" #rocq_concept proofmode "Intro Patterns" "IModalElim (pattern: >H)" ported "pattern: >H" -#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" missing "" -#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" missing "" +#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" ported "pattern: →/←" +#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" ported "pattern: !%" #rocq_concept proofmode "Intro Patterns" "IModalIntro (pattern: !>)" ported "pattern: !>" -#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" missing "" +#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" ported "pattern: /=" #rocq_concept proofmode "Intro Patterns" "IDone (pattern: //)" ported "pattern: //" -#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" missing "" -#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" missing "" -#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" missing "" -#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" missing "" +#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" ported "pattern: *" +#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" ported "pattern: **" +#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" ported "pattern: { H, ... }" +#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" ported "pattern: { !H, ... }" #rocq_concept proofmode "Specialization Patterns" missing "" #rocq_concept proofmode "Specialization Patterns" "SIdent (pattern: H)" ported "pattern: H" From 761dac6145ee87208c5365013aaaaad8e6ec22f9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 13:25:50 +0200 Subject: [PATCH 42/53] Update tactics.md for the new introduction and case destruction patterns --- Iris/tactics.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Iris/tactics.md b/Iris/tactics.md index f9e465ec0..8031d819b 100644 --- a/Iris/tactics.md +++ b/Iris/tactics.md @@ -77,6 +77,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti - `#`*pat* — Move the hypothesis to the intuitionistic context, then destruct with *pat*. - `∗`*pat* — Move the hypothesis to the spatial context, then destruct with *pat*. - `>`*pat* — Eliminate the modality at the top of the hypothesis, then destruct with *pat*. +- `←`/`→` — Rewrite using a pure Lean equality and then remove the equality from the context. Example: ```lean @@ -91,8 +92,14 @@ Example: - [*casesPat*](#cases-patterns) — Introduce a hypothesis and destruct it with [*casesPat*](#cases-patterns). In particular, `%x` introduces a universally quantified variable or pure premise into the Lean context. - `!>` — Introduce the modality at the top of the goal (like `imodintro`). - `//` — Try to close the goal with `itrivial` (and continue with the remaining patterns if it fails). - -Example: `iintro %x ⟨HP, #HQ⟩ !> //`. +- `*` — Introduce all universal quantifiers. +- `**` — Introduce all universal quantifiers, pure arrows, and wands. +- `!%` — Introduce a pure proof goal and exit the proof mode. +- `/=` — Apply simplification. +- `//=` — Apply simplification and try solving the goal using `itrivial`. This is a shorthand for `/=` and `//`. +- `{` [*selPats*](#selection-patterns) `}` — Clear the selection hypotheses chosen by the selection patterns *selPats*. Each element in *selPats* can be prefixed with `!` so that the chosen hypotheses are framed instead. + +Example: `iintro %x ⟨HP, #HQ⟩ !> {HR !HS #} → //`. ## Selection Patterns From 5c4255ce7626969c7872610870c1f5c0759fb256 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 13:41:49 +0200 Subject: [PATCH 43/53] Add `noWs` to some case destruction patterns --- Iris/Iris/ProofMode/Patterns/CasesPattern.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index 5e159a181..ab28c13c6 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -27,13 +27,13 @@ syntax "⟨" icasesPatAlts,* "⟩" : icasesPat /-- Destruct a disjunction, one goal per disjunct. -/ syntax "(" icasesPatAlts ")" : icasesPat /-- Move the hypothesis to the pure Lean context and give it a name. -/ -syntax "%" binderIdent : icasesPat +syntax "%" noWs binderIdent : icasesPat /-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/ -syntax "#" icasesPat : icasesPat +syntax "#" noWs icasesPat : icasesPat /-- Move the hypothesis to the spatial context and destruct the proposition. -/ -syntax "∗" icasesPat : icasesPat +syntax "∗" noWs icasesPat : icasesPat /-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/ -syntax ">" icasesPat : icasesPat +syntax ">" noWs icasesPat : icasesPat /-- Introduce a pure equality and use it for rewriting in the backward direction. -/ syntax "←" : icasesPat /-- Introduce a pure equality and use it for rewriting in the forward direction. -/ From ea65afd8fdc88316b05c1d156f45b0519bda7e2d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 14:48:16 +0200 Subject: [PATCH 44/53] Support for `rcases` destruction patterns for pure propositions --- .../Iris/ProofMode/Patterns/CasesPattern.lean | 6 ++-- Iris/Iris/ProofMode/Tactics/Cases.lean | 28 ++++++++------- Iris/Iris/ProofMode/Tactics/Intro.lean | 14 ++++++-- Iris/Iris/ProofMode/Tactics/Pure.lean | 35 +++++++++++-------- Iris/Iris/ProofMode/Tactics/RevertIntro.lean | 4 +-- Iris/Iris/Tests/Tactics.lean | 17 ++++++++- 6 files changed, 69 insertions(+), 35 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index ab28c13c6..de86a29c4 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -27,7 +27,7 @@ syntax "⟨" icasesPatAlts,* "⟩" : icasesPat /-- Destruct a disjunction, one goal per disjunct. -/ syntax "(" icasesPatAlts ")" : icasesPat /-- Move the hypothesis to the pure Lean context and give it a name. -/ -syntax "%" noWs binderIdent : icasesPat +syntax "%" noWs rcasesPat : icasesPat /-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/ syntax "#" noWs icasesPat : icasesPat /-- Move the hypothesis to the spatial context and destruct the proposition. -/ @@ -45,7 +45,7 @@ inductive iCasesPat | frame (ref : Syntax) | conjunction (ref : Syntax) (args : List iCasesPat) | disjunction (ref : Syntax) (args : List iCasesPat) - | pure (ref : Syntax) (pat : TSyntax ``binderIdent) + | pure (ref : Syntax) (pat : TSyntax `rcasesPat) | intuitionistic (ref : Syntax) (pat : iCasesPat) | spatial (ref : Syntax) (pat : iCasesPat) | mod (ref : Syntax) (pat : iCasesPat) @@ -68,7 +68,7 @@ where | `(icasesPat| -) => some <| .clear ref | `(icasesPat| $) => some <| .frame ref | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ref ·.toList) - | `(icasesPat| %$pat:binderIdent) => some <| .pure ref pat + | `(icasesPat| %$pat:rcasesPat) => some <| .pure ref pat | `(icasesPat| #$pat) => go pat |>.map <| .intuitionistic ref | `(icasesPat| ∗$pat) => go pat |>.map <| .spatial ref | `(icasesPat| >$pat) => go pat |>.map <| .mod ref diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 1d37e72c2..be44c9b24 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -72,8 +72,7 @@ private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) throwError "{tacName}: cannot destruct {A} as an empty conjunct" /-- Destruct an existential hypothesis [A] by introducing its witness and continuing with the body [B]. -/ -private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) - (name : TSyntax ``binderIdent) +private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (pat : TSyntax `rcasesPat) (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do @@ -82,12 +81,13 @@ private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ) | throwError "{tacName}: {A} is not an existential quantifier" - let (name, ref) ← getFreshName name - withLocalDeclDQ name α fun x => do - addLocalVarInfo ref (← getLCtx) x α - have B : Q($prop) := Expr.headBeta q($Φ $x) - let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← mkLambdaFVars #[x] <|← k B - return q(exists_elim' $pf) + let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← + introWithRcasesPat q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) pat fun g => do + let B : Q($prop) ← mkFreshExprMVarQ q($prop) + let .true ← isDefEq (← g.getType) q($P ∗ □?$p $B ⊢ $goal) + | throwError "{tacName}: unexpected goal {goal} after intro pattern" + k (Expr.headBeta (← instantiateMVars B)) + return q(exists_elim' $pf) /-- Destruct a conjunction hypothesis [A] and continue with only its left or right component. -/ private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) @@ -267,7 +267,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (iCasesCore hyps goal (.disjunction ref args) p · tacName k) | .pure _ arg => - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal + iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) <| k hyps goal | .intuitionistic _ arg => iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) @@ -279,9 +279,13 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A tacName k - | .rewrite _ forward => - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(binderIdent| _)) q(.rfl) - <| fun _ h => iCasesPureRewrite hyps goal h forward tacName k + | .rewrite _ forward => do + let name ← mkFreshUserName .anonymous + let ident := mkIdent name + iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(rcasesPat| $ident:ident)) q(.rfl) do + let some ldecl := (← getLCtx).findFromUserName? name + | throwError "{tacName}: unable to find the introduced pure hypothesis" + iCasesPureRewrite hyps goal ldecl.toExpr forward tacName k /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 63b872e6c..88e393c9f 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -155,8 +155,18 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} | .intro (.rewrite _ direction) => iIntroCoreForallIntro ref none Q tacName none <| fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) - | .intro (.pure _ n) => - iIntroCoreForallIntro ref n Q tacName none (fun _ B => iIntroCore hyps B pats tacName k) + | .intro (.pure _ pat) => + let v ← mkFreshLevelMVar + let α ← mkFreshExprMVarQ q(Sort v) + let Φ ← mkFreshExprMVarQ q($α → $prop) + let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) + | throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" + let pf : Q(∀ x, $P ⊢ $Φ x) ← introWithRcasesPat q(∀ x, $P ⊢ $Φ x) pat fun g => do + let B : Q($prop) ← mkFreshExprMVarQ q($prop) + let .true ← isDefEq (← g.getType) q($P ⊢ $B) + | throwError "{tacName}: internal error: unexpected goal after intro pattern" + iIntroCore hyps (Expr.headBeta (← instantiateMVars B)) pats tacName k + return q(from_forall_intro (Q := $Q) $pf) | .intro pat => let A1 ← mkFreshExprMVarQ q($prop) let A2 ← mkFreshExprMVarQ q($prop) diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index f75e56884..d05c59976 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -40,26 +40,31 @@ theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} public meta section open Lean Elab Tactic Meta Qq +def introWithRcasesPat (ty : Q(Prop)) (pat : TSyntax `rcasesPat) + (k : MVarId → ProofModeM Expr) : ProofModeM Q($ty) := do + let m : Q($ty) ← mkFreshExprSyntheticOpaqueMVar ty + let tac ← withRef pat `(tactic| rintro $pat:rcasesPat) + for g in (← evalTacticAt tac m.mvarId!) do + g.withContext do g.assign (← k g) + instantiateMVars m + def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) - (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) - (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do + (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) + (purePat : TSyntax `rcasesPat) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) + (k : ProofModeM Q($P' ⊢ $Q)) : ProofModeM Q($P ⊢ $Q) := do let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) | throwError "ipure: {A} is not pure" - let (name, ref) ← getFreshName name - withLocalDeclDQ name φ fun h => do - addLocalVarInfo ref (← getLCtx) h φ - let m ← k φ h - let f : Q($φ → $P' ⊢ $Q) ← mkLambdaFVars #[h] m + let f ← introWithRcasesPat q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k - match matchBool p with - | .inl _ => - return (q(pure_elim_intuitionistic $pf $f)) - | .inr _ => - let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q)) - | throwError "ipure: {A} is not affine and the goal not absorbing" - return q(pure_elim_spatial (A:=$A) $pf $f) + match matchBool p with + | .inl _ => + return (q(pure_elim_intuitionistic $pf $f)) + | .inr _ => + let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q)) + | throwError "ipure: {A} is not affine and the goal not absorbing" + return q(pure_elim_spatial (A := $A) $pf $f) def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop)) (e goal : Q($prop)) (tacName : String) : @@ -95,7 +100,7 @@ elab "ipure " colGt hyp:ident : tactic => do let ivar ← hyps.findWithInfo hyp let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar - let pf ← iPureCore bi e e' p out' goal (← `(binderIdent| $hyp:ident)) pf fun _ _ => addBIGoal hyps' goal + let pf ← iPureCore bi e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf <| addBIGoal hyps' goal mvar.assign pf diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean index 1c710b2db..7817dc308 100644 --- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean +++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean @@ -28,8 +28,8 @@ def iRevertIntro let names : List (Syntax × IntroPat) ← hs.mapM fun | {kind := .pure id, ..} => do let name ← Lean.mkIdent <$> id.getUserName - let ident ← `(binderIdent| $name:ident) - return (name, .intro <| .pure ident ident) + let purePat ← `(rcasesPat| $name:ident) + return (name, .intro <| .pure purePat purePat) | {kind := .ipm ivar, ..} => do let name ← Lean.mkIdent <$> (hyps.getUserName? ivar).getM let ident ← `(binderIdent| $name:ident) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index e489b07ad..74620d4f1 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -349,6 +349,13 @@ definition name, but `x✝` is a proof of example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by iintro → +/-- Tests `iintro` with non-trivial `rcases` destruction patterns -/ +example [BI PROP] (a b c1 c2 c3 : Prop) (P : Prop → Prop) : + ⊢@{PROP} □ ⌜((a = b ∧ (b ∨ (c1 ∧ c2 ∧ c3))) ∧ ∃ x, P x)⌝ -∗ ⌜a ∨ c1⌝ ∗ ⌜∃ x, P x⌝ := by + iintro %⟨⟨rfl, ((hb : a) | ⟨hc, _, -⟩)⟩, @⟨d : Prop, hd⟩⟩ !% + · grind + · grind + end intro -- revert @@ -1795,13 +1802,21 @@ example [BI PROP] (m n : Nat) (a b c : Prop) : hypothesis is not a pure equality -/ /-- error: Invalid rewrite argument: Expected an equality or iff proof or -definition name, but `x✝` is a proof of +definition name, but `✝` is a proof of P -/ #guard_msgs in example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by iintro HP icases HP with → +/-- Tests `icases` with non-trivial `rcases` destruction patterns -/ +example [BI PROP] (a b c1 c2 c3 : Prop) (P : Prop → Prop) : + ⊢@{PROP} □ ⌜((a = b ∧ (b ∨ (c1 ∧ c2 ∧ c3))) ∧ ∃ x, P x)⌝ -∗ ⌜a ∨ c1⌝ ∗ ⌜∃ x, P x⌝ := by + iintro Hpure + icases Hpure with %⟨⟨rfl, ((hb : a) | ⟨hc, _, -⟩)⟩, @⟨d : Prop, hd⟩⟩ + · ipureintro <;> grind + · ipureintro <;> grind + end cases section imodintro From 03f876152e77ada299be5017942bfa5ead40dad6 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:13:20 +0200 Subject: [PATCH 45/53] Replace the use of `evalTacticAt` with direct use of built-in function --- Iris/Iris/ProofMode/Tactics/Cases.lean | 2 +- Iris/Iris/ProofMode/Tactics/Intro.lean | 8 ++++---- Iris/Iris/ProofMode/Tactics/Pure.lean | 10 ++++------ 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index be44c9b24..b88b85d7d 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -82,7 +82,7 @@ private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (pat : TSyntax `r let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ) | throwError "{tacName}: {A} is not an existential quantifier" let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← - introWithRcasesPat q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) pat fun g => do + iPureDestruct q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) pat fun g => do let B : Q($prop) ← mkFreshExprMVarQ q($prop) let .true ← isDefEq (← g.getType) q($P ∗ □?$p $B ⊢ $goal) | throwError "{tacName}: unexpected goal {goal} after intro pattern" diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 88e393c9f..26731d02d 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -160,11 +160,11 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} let α ← mkFreshExprMVarQ q(Sort v) let Φ ← mkFreshExprMVarQ q($α → $prop) let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ) - | throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" - let pf : Q(∀ x, $P ⊢ $Φ x) ← introWithRcasesPat q(∀ x, $P ⊢ $Φ x) pat fun g => do + | throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis" + let pf : Q(∀ x, $P ⊢ $Φ x) ← iPureDestruct q(∀ x, $P ⊢ $Φ x) pat fun g => do let B : Q($prop) ← mkFreshExprMVarQ q($prop) - let .true ← isDefEq (← g.getType) q($P ⊢ $B) - | throwError "{tacName}: internal error: unexpected goal after intro pattern" + let eq ← isDefEq (← g.getType) q($P ⊢ $B) + if !eq then throwError "{tacName}: internal error: unexpected goal after intro pattern" iIntroCore hyps (Expr.headBeta (← instantiateMVars B)) pats tacName k return q(from_forall_intro (Q := $Q) $pf) | .intro pat => diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index d05c59976..9bae5a235 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -40,11 +40,11 @@ theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} public meta section open Lean Elab Tactic Meta Qq -def introWithRcasesPat (ty : Q(Prop)) (pat : TSyntax `rcasesPat) +def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat) (k : MVarId → ProofModeM Expr) : ProofModeM Q($ty) := do let m : Q($ty) ← mkFreshExprSyntheticOpaqueMVar ty - let tac ← withRef pat `(tactic| rintro $pat:rcasesPat) - for g in (← evalTacticAt tac m.mvarId!) do + let gs ← withRef pat <| Lean.Elab.Tactic.RCases.rintro #[pat] none m.mvarId! + for g in gs do g.withContext do g.assign (← k g) instantiateMVars m @@ -55,9 +55,7 @@ def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) | throwError "ipure: {A} is not pure" - - let f ← introWithRcasesPat q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k - + let f ← iPureDestruct q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k match matchBool p with | .inl _ => return (q(pure_elim_intuitionistic $pf $f)) From 878b127b59d717c184e513cd3ada0af3a50b5145 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:15:32 +0200 Subject: [PATCH 46/53] Revert the use of `noWs` --- Iris/Iris/ProofMode/Patterns/CasesPattern.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index de86a29c4..f789b258b 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -27,13 +27,13 @@ syntax "⟨" icasesPatAlts,* "⟩" : icasesPat /-- Destruct a disjunction, one goal per disjunct. -/ syntax "(" icasesPatAlts ")" : icasesPat /-- Move the hypothesis to the pure Lean context and give it a name. -/ -syntax "%" noWs rcasesPat : icasesPat +syntax "%" rcasesPat : icasesPat /-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/ -syntax "#" noWs icasesPat : icasesPat +syntax "#" icasesPat : icasesPat /-- Move the hypothesis to the spatial context and destruct the proposition. -/ -syntax "∗" noWs icasesPat : icasesPat +syntax "∗" icasesPat : icasesPat /-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/ -syntax ">" noWs icasesPat : icasesPat +syntax ">" icasesPat : icasesPat /-- Introduce a pure equality and use it for rewriting in the backward direction. -/ syntax "←" : icasesPat /-- Introduce a pure equality and use it for rewriting in the forward direction. -/ From da56fe624ca7fd550e8cd9e17a15eace20fe5079 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:25:09 +0200 Subject: [PATCH 47/53] Minor code formatting --- Iris/Iris/ProofMode/Tactics/Cases.lean | 7 ++++--- Iris/Iris/ProofMode/Tactics/Pure.lean | 4 ++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index b88b85d7d..f6bbca701 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -80,12 +80,13 @@ private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (pat : TSyntax `r let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v) let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ) - | throwError "{tacName}: {A} is not an existential quantifier" + | throwError "{tacName}: {A} is not an existential quantifier" let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← iPureDestruct q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) pat fun g => do let B : Q($prop) ← mkFreshExprMVarQ q($prop) - let .true ← isDefEq (← g.getType) q($P ∗ □?$p $B ⊢ $goal) - | throwError "{tacName}: unexpected goal {goal} after intro pattern" + let eq ← isDefEq (← g.getType) q($P ∗ □?$p $B ⊢ $goal) + if !eq then + throwError "{tacName}: unexpected goal {goal} after intro pattern" k (Expr.headBeta (← instantiateMVars B)) return q(exists_elim' $pf) diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 9bae5a235..9a59a8ee9 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -40,6 +40,10 @@ theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} public meta section open Lean Elab Tactic Meta Qq +/-- + Apply a destruction pattern for pure hypotheses with `k` being a function + to be applied to subgoals generated after the destruction. +-/ def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat) (k : MVarId → ProofModeM Expr) : ProofModeM Q($ty) := do let m : Q($ty) ← mkFreshExprSyntheticOpaqueMVar ty From e9a11b2ba03de124c69969d60f3ea02bd09dea71 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:42:12 +0200 Subject: [PATCH 48/53] Add `ipure ... as ...` tactic syntax --- Iris/Iris/ProofMode/Tactics/Pure.lean | 14 ++++++++++++++ Iris/Iris/Tests/Tactics.lean | 7 +++++++ 2 files changed, 21 insertions(+) diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 9a59a8ee9..8d850fc1f 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -106,6 +106,20 @@ elab "ipure " colGt hyp:ident : tactic => do mvar.assign pf +/-- + `ipure H as pat` moves a pure hypothesis `H` from the Iris context into the + regular Lean context and destructs it using the `rcases` destruction pattern. +-/ +elab "ipure " colGt hyp:ident " as " pat:rcasesPat : tactic => do + ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do + + let ivar ← hyps.findWithInfo hyp + let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar + + let pf ← iPureCore bi e e' p out' goal pat pf <| addBIGoal hyps' goal + + mvar.assign pf + /-- `iempintro` solves an `emp` goal, provided that the spatial context is affine. -/ diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 74620d4f1..b43b6ead0 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -988,6 +988,13 @@ example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ ⌜φ2⌝) ⊢ Q -∗ Q : ipure Hφ iexact HQ +/-- Tests `ipure` with an `rcases` destruction pattern -/ +example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ ⌜φ2⌝) ⊢ Q -∗ Q := by + iintro Hφ + iintro HQ + ipure Hφ as ⟨hφ1, -⟩ + iexact HQ + /-- Tests `ipure` with implication containing pure -/ example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ ⌜φ2⌝ → ⌜φ3⌝) ⊢ Q -∗ Q := by iintro Hφ From c16b5823e7dfce494ac035961be7a3ca49d27227 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:45:17 +0200 Subject: [PATCH 49/53] Update `Porting.lean` and `tactics.md` for the `ipure ... as ...` and case destruction pattern generalisation --- Iris/Iris/ProofMode/Porting.lean | 2 +- Iris/tactics.md | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index 14467db31..3fcdea6d0 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -27,7 +27,7 @@ import Iris.Std.RocqPorting #rocq_concept proofmode "Tactics" "iAssumptionCoq" ignored "weird tactic" #rocq_concept proofmode "Tactics" "iExFalso" ported "iexfalso" #rocq_concept proofmode "Tactics" "iPure (basic)" ported "ipure" -#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" missing "(also for other tactics using ipure)" +#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" ported "ipure ... as ..." #rocq_concept proofmode "Tactics" "iEmpIntro" ported "iempintro" #rocq_concept proofmode "Tactics" "iPureIntro" ported "ipureintro" #rocq_concept proofmode "Tactics" "iFrame (basic)" ported "iframe" diff --git a/Iris/tactics.md b/Iris/tactics.md index 8031d819b..a1c73ae49 100644 --- a/Iris/tactics.md +++ b/Iris/tactics.md @@ -14,6 +14,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti - `iclear` [*selPats*](#selection-patterns) — Discard the hypotheses selected by [*selPats*](#selection-patterns). - `irevert` [*selPats*](#selection-patterns) — Revert the selected hypotheses (proof mode or pure Lean hypotheses) into the goal. - `ipure` *H* — Move the pure hypothesis *H* into the Lean context. +- `ipure` *H* `as` *rcasesPat* — Move the pure hypothesis *H* into the Lean context and destruct it with the `rcases` pattern. - `iintuitionistic` *H* — Move *H* to the intuitionistic context. Equivalent to `icases H with #H`. - `ispatial` *H* — Move *H* to the spatial context. Equivalent to `icases H with ∗H`. @@ -73,7 +74,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti - `$` — Frame the hypothesis: immediately cancel it against the goal (like `iframe`). - `⟨`*pat₁*`,` ... `,` *patₙ*`⟩` — Destruct a (separating) conjunction or existential; an existential variable is bound with `%`*x*, e.g. `⟨%x, H⟩`. - `(`*pat₁* `|` ... `|` *patₙ*`)` — Destruct a disjunction, one goal per disjunct. Parentheses can be omitted when nested inside `⟨⟩`. -- `%`*name* — Move the (pure) hypothesis into the Lean context as *name*. +- `%`*rcasesPat* — Move the (pure) hypothesis into the Lean context and destruct it with the `rcases` pattern *rcasesPat*. - `#`*pat* — Move the hypothesis to the intuitionistic context, then destruct with *pat*. - `∗`*pat* — Move the hypothesis to the spatial context, then destruct with *pat*. - `>`*pat* — Eliminate the modality at the top of the hypothesis, then destruct with *pat*. From 6accdcc5aa0af11c9f3dc938ba0a9c393b7ed44c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:51:32 +0200 Subject: [PATCH 50/53] More minor formatting --- Iris/Iris/ProofMode/Tactics/Clear.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Clear.lean b/Iris/Iris/ProofMode/Tactics/Clear.lean index 8330cea9e..ffa84ac6b 100644 --- a/Iris/Iris/ProofMode/Tactics/Clear.lean +++ b/Iris/Iris/ProofMode/Tactics/Clear.lean @@ -27,7 +27,7 @@ open Lean Elab Tactic Meta Qq def iClearCoreOne {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) (p : Q(Bool)) (out goal : Q($prop)) (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) - (tacName : String := "iclear") : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do + (tacName : String) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do match matchBool p with | .inl _ => return q(clear_intuitionistic (Q := $goal) $pf) | .inr _ => @@ -40,11 +40,11 @@ private structure ClearState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (origE go pf : Q(($e ⊢ $goal) → ($origE ⊢ $goal)) private def ClearState.clearProofModeHyp {u prop bi origE goal} : - @ClearState u prop bi origE goal → IVarId → + @ClearState u prop bi origE goal → String → IVarId → ProofModeM (@ClearState u prop bi origE goal) - | { e, hyps, pf }, ivar => do + | { e, hyps, pf }, tacName, ivar => do let ⟨e', hyps', _, out', p, _, hrem⟩ := hyps.remove true ivar - let step ← iClearCoreOne bi e e' p out' goal hrem + let step ← iClearCoreOne bi e e' p out' goal hrem tacName let pf' : Q(($e' ⊢ $goal) → ($origE ⊢ $goal)) := q(λ h => $pf ($step h)) return { e := e', hyps := hyps', pf := pf' } @@ -59,7 +59,7 @@ def iClearCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} -- Clear the selected Iris hypotheses first, updating the proof-mode context and proof term. let mut st : ClearState e goal := { e, hyps, pf := q(id) } - for ivar in ivars do st ← st.clearProofModeHyp ivar + for ivar in ivars do st ← st.clearProofModeHyp "iclear" ivar -- Lean locals are cleared afterwards; first ensure no remaining hypothesis or goal depends on them. for fvar in fvars do From 137e9cba0277cda29f8c8c7c62eba909da7f7286 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 15:57:49 +0200 Subject: [PATCH 51/53] Generalise `iPureCore` error message --- Iris/Iris/ProofMode/Tactics/Cases.lean | 4 ++-- Iris/Iris/ProofMode/Tactics/Pure.lean | 12 ++++++------ Iris/Iris/Tests/Tactics.lean | 10 +++++++++- 3 files changed, 17 insertions(+), 9 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index f6bbca701..ecff8ae64 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -268,7 +268,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (iCasesCore hyps goal (.disjunction ref args) p · tacName k) | .pure _ arg => - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) <| k hyps goal + iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) tacName <| k hyps goal | .intuitionistic _ arg => iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) @@ -283,7 +283,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} | .rewrite _ forward => do let name ← mkFreshUserName .anonymous let ident := mkIdent name - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(rcasesPat| $ident:ident)) q(.rfl) do + iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(rcasesPat| $ident:ident)) q(.rfl) tacName do let some ldecl := (← getLCtx).findFromUserName? name | throwError "{tacName}: unable to find the introduced pure hypothesis" iCasesPureRewrite hyps goal ldecl.toExpr forward tacName k diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 8d850fc1f..3277a1680 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -53,19 +53,19 @@ def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat) instantiateMVars m def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) - (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) - (purePat : TSyntax `rcasesPat) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) + (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (purePat : TSyntax `rcasesPat) + (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (tacName : String) (k : ProofModeM Q($P' ⊢ $Q)) : ProofModeM Q($P ⊢ $Q) := do let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) - | throwError "ipure: {A} is not pure" + | throwError "{tacName}: {A} is not pure" let f ← iPureDestruct q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k match matchBool p with | .inl _ => return (q(pure_elim_intuitionistic $pf $f)) | .inr _ => let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q)) - | throwError "ipure: {A} is not affine and the goal not absorbing" + | throwError "{tacName}: {A} is not affine and the goal not absorbing" return q(pure_elim_spatial (A := $A) $pf $f) def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop)) @@ -102,7 +102,7 @@ elab "ipure " colGt hyp:ident : tactic => do let ivar ← hyps.findWithInfo hyp let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar - let pf ← iPureCore bi e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf <| addBIGoal hyps' goal + let pf ← iPureCore bi e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf "ipure" <| addBIGoal hyps' goal mvar.assign pf @@ -116,7 +116,7 @@ elab "ipure " colGt hyp:ident " as " pat:rcasesPat : tactic => do let ivar ← hyps.findWithInfo hyp let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar - let pf ← iPureCore bi e e' p out' goal pat pf <| addBIGoal hyps' goal + let pf ← iPureCore bi e e' p out' goal pat pf "ipure" <| addBIGoal hyps' goal mvar.assign pf diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index b43b6ead0..9c3e756bf 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2759,13 +2759,21 @@ example {GF m n} [LcGS .hasLC GF] : icombine H1 H2 H3 H4 as Hnew iexact Hnew -/-- Tests `icombine` for combining two tokens -/ +/-- Tests `icombine` for combining two tokens. -/ example {GF} [TokenG GF] {γ} : ⊢@{IProp GF} token γ -∗ token γ -∗ False := by iintro H1 H2 icombine H1 H2 gives H iexact H +/- Tests `icombine` with an invalid destruction pattern. -/ +/-- error: icombine: cannot destruct iprop( (P ∗ Q)) -/ +#guard_msgs in +example [BI PROP] {P Q R : PROP} [CombineSepGives P Q R] : + ⊢ P -∗ Q -∗ (P ∗ Q) ∗ R := by + iintro HP HQ + icombine HP HQ as ⟨HNew1, _⟩ gives HNew2 + end icombine section iloeb From fe7630c5a76d71c083a1b7373b0003215771e2fa Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 17:12:57 +0200 Subject: [PATCH 52/53] Refactor code to simplify `.rewrite` case in `iCasesCore` --- Iris/Iris/ProofMode/Tactics/Cases.lean | 51 +++++------------ Iris/Iris/ProofMode/Tactics/Intro.lean | 2 +- Iris/Iris/ProofMode/Tactics/Pure.lean | 79 ++++++++++++++++++++------ Iris/Iris/Tests/Tactics.lean | 14 ++++- 4 files changed, 89 insertions(+), 57 deletions(-) diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index ecff8ae64..348a6516d 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -72,7 +72,7 @@ private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) throwError "{tacName}: cannot destruct {A} as an empty conjunct" /-- Destruct an existential hypothesis [A] by introducing its witness and continuing with the body [B]. -/ -private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (pat : TSyntax `rcasesPat) +private def iCasesExists {prop : Q(Type u)} {bi : Q(BI $prop)} (pat : TSyntax `rcasesPat) (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do @@ -103,7 +103,7 @@ private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) else return some q(sep_and_elim_l $(← k A1)) /-- Destruct a conjunction hypothesis [A] into two parts and continue with the left and right subpatterns in sequence. -/ -private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) +private def iCasesSep {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) (tacName : String) (k : ∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal)) (k1 k2 : ∀ {P}, Hyps bi P → (goal B : Q($prop)) → @@ -137,7 +137,7 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) return q(sep_elim_spatial (A := $A) $pf) /-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/ -private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) +private def iCasesOr {prop : Q(Type u)} {bi : Q(BI $prop)} (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k1 k2 : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do @@ -151,7 +151,7 @@ private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) Destruct a persistent hypothesis [A] by turning it into an explicit [□ B] and continuing with the persistent body. -/ -private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) +private def iCasesIntuitionistic {prop : Q(Type u)} {bi : Q(BI $prop)} (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String) (k : (B : Q($prop)) → ProofModeM Q($P ∗ □ $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do @@ -170,7 +170,7 @@ private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) Destruct an affine/spatial hypothesis [A] by removing the affinely wrapper and continuing with the spatial body. -/ -private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) +private def iCasesSpatial {prop : Q(Type u)} {bi : Q(BI $prop)} (p : Q(Bool)) (P A goal : Q($prop)) (k : (B : Q($prop)) → ProofModeM Q($P ∗ $B ⊢ $goal)) : ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do @@ -179,26 +179,6 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A $p) return q(spatial_elim $(← k B)) -/-- - Rewrite an Iris entailment using the pure Lean equality `h`, - removing `h` from the context afterwards. --/ -def iCasesPureRewrite {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} - (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (forward : Bool) (tacName : String) - (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : - ProofModeM Q($e ⊢ $goal) := do - let target := q($(hyps.tm) ⊢ $goal) - let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!) - let ⟨newE, eq, []⟩ ← g.rewrite target h !forward - | throwError "{tacName}: rewriting should not give additional subgoals" - let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails - | throwError "{tacName}: unable to parse the Iris entailment {newE}" - let some ⟨_, hyps'⟩ := parseHyps? bi newTm - | throwError "{tacName}: unable to parse the Iris context {newTm}" - let gNew ← g.replaceTargetEq newE eq - (withoutFVars (u := 0) #[h.fvarId!] <| k hyps' newGoal) >>= (gNew.assign ·) - instantiateMVars (.mvar g) - variable {prop : Q(Type u)} (bi : Q(BI $prop)) in /-- Recursively destruct the current hypothesis `□?p A` in the proof-mode context `hyps` @@ -252,7 +232,7 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} -- pure conjunctions are always handled as existentials. There is `intoExist_and_pure` and -- `intoExist_sep_pure` to make this work as expected for pure assertions that are not explicit existentials. | .conjunction ref (.pure _ arg :: args) => - iCasesExists bi arg p P A goal tacName (iCasesCore hyps goal (.conjunction ref args) p · tacName k) + iCasesExists arg p P A goal tacName (iCasesCore hyps goal (.conjunction ref args) p · tacName k) | .conjunction ref (arg :: args) => if arg matches .clear _ then if let some pf ← iCasesAndLR bi p P A goal true λ B => @@ -260,33 +240,28 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} if args matches [.clear _] then if let some pf ← iCasesAndLR bi p P A goal false λ B => iCasesCore hyps goal arg p B tacName k then return pf - iCasesSep bi hyps p A goal tacName k (iCasesCore · · arg p · tacName ·) + iCasesSep hyps p A goal tacName k (iCasesCore · · arg p · tacName ·) (iCasesCore · · (.conjunction ref args) p · tacName ·) | .disjunction ref (arg :: args) => - iCasesOr bi p P A goal tacName (iCasesCore hyps goal arg p · tacName k) + iCasesOr p P A goal tacName (iCasesCore hyps goal arg p · tacName k) (iCasesCore hyps goal (.disjunction ref args) p · tacName k) | .pure _ arg => - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) tacName <| k hyps goal + iPureCore q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) tacName <| k hyps goal | .intuitionistic _ arg => - iCasesIntuitionistic bi p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) + iCasesIntuitionistic p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k) | .spatial _ arg => - iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · tacName k) + iCasesSpatial p P A goal (iCasesCore hyps goal arg q(false) · tacName k) | .mod _ arg => iModCore bi P goal p A λ p' A goal' => iCasesCore hyps goal' arg p' A tacName k - | .rewrite _ forward => do - let name ← mkFreshUserName .anonymous - let ident := mkIdent name - iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal (← `(rcasesPat| $ident:ident)) q(.rfl) tacName do - let some ldecl := (← getLCtx).findFromUserName? name - | throwError "{tacName}: unable to find the introduced pure hypothesis" - iCasesPureRewrite hyps goal ldecl.toExpr forward tacName k + | .rewrite _ forward => + iPureRewriteCore hyps p A goal tacName forward q(.rfl) k /-- `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`. diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 26731d02d..e2e502742 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -154,7 +154,7 @@ partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k) | .intro (.rewrite _ direction) => iIntroCoreForallIntro ref none Q tacName none <| - fun x B => iCasesPureRewrite hyps B x direction tacName (iIntroCore · · pats tacName k) + fun x B => iPureRewriteCoreAux hyps B x direction tacName (iIntroCore · · pats tacName k) | .intro (.pure _ pat) => let v ← mkFreshLevelMVar let α ← mkFreshExprMVarQ q(Sort v) diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index 3277a1680..ff23b600b 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -41,8 +41,8 @@ public meta section open Lean Elab Tactic Meta Qq /-- - Apply a destruction pattern for pure hypotheses with `k` being a function - to be applied to subgoals generated after the destruction. + Apply a destruction pattern for pure hypotheses. + Then, apply the function `k` to all subgoals generated by the destruction. -/ def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat) (k : MVarId → ProofModeM Expr) : ProofModeM Q($ty) := do @@ -52,21 +52,68 @@ def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat) g.withContext do g.assign (← k g) instantiateMVars m -def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) +/-- + Rewrite an Iris entailment using the pure Lean equality `h`, + removing it from the context afterwards. +-/ +def iPureRewriteCoreAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} + (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (forward : Bool) (tacName : String) + (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : + ProofModeM Q($e ⊢ $goal) := do + let target := q($(hyps.tm) ⊢ $goal) + let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!) + let ⟨newE, eq, []⟩ ← g.rewrite target h !forward + | throwError "{tacName}: rewriting should not give additional subgoals" + let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails + | throwError "{tacName}: unable to parse the Iris entailment {newE}" + let some ⟨_, hyps'⟩ := parseHyps? bi newTm + | throwError "{tacName}: unable to parse the Iris context {newTm}" + let gNew ← g.replaceTargetEq newE eq + -- Apply the continuation function to the new proof goal after rewriting + (withoutFVars (u := 0) #[h.fvarId!] <| k hyps' newGoal) >>= (gNew.assign ·) + instantiateMVars (.mvar g) + +/-- Transform a proof of `φ → (P' ⊢ Q)` into that of `P ⊢ Q`. -/ +def iPureCoreBuildProof {prop : Q(Type u)} {bi : Q(BI $prop)} + {P P' : Q($prop)} {p : Q(Bool)} {A Q : Q($prop)} (φ : Q(Prop)) + (inst : Q(IntoPure $A $φ)) + (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (f : Q($φ → ($P' ⊢ $Q))) (tacName : String) : + ProofModeM Q($P ⊢ $Q) := do + match matchBool p with + | .inl _ => return q(pure_elim_intuitionistic $pf $f) + | .inr _ => + let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q)) + | throwError "{tacName}: {A} is not affine and the goal not absorbing" + return q(pure_elim_spatial (A := $A) $pf $f) + +/-- + Introduce a pure equality into the Lean context, use it for rewriting and + discard the equality hypothesis. +-/ +def iPureRewriteCore {prop : Q(Type u)} {bi : Q(BI $prop)} {P P' : Q($prop)} + (hyps : Hyps bi P') (p : Q(Bool)) (A Q : Q($prop)) (tacName : String) + (forward : Bool) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) + (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) : + ProofModeM Q($P ⊢ $Q) := do + let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) + let .some inst ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) + | throwError "{tacName}: {A} is not pure" + let m : Q($φ → ($P' ⊢ $Q)) ← mkFreshExprSyntheticOpaqueMVar q($φ → ($P' ⊢ $Q)) + let (h, g) ← m.mvarId!.intro1 + let f ← do + g.withContext do g.assign (← iPureRewriteCoreAux hyps Q (.fvar h) forward tacName k) + instantiateMVars m + return ← iPureCoreBuildProof φ inst pf f tacName + +def iPureCore {prop : Q(Type u)} {bi : Q(BI $prop)} (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (purePat : TSyntax `rcasesPat) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (tacName : String) (k : ProofModeM Q($P' ⊢ $Q)) : ProofModeM Q($P ⊢ $Q) := do let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) - | throwError "{tacName}: {A} is not pure" + let some inst ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ) + | throwError "{tacName}: {A} is not pure" let f ← iPureDestruct q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k - match matchBool p with - | .inl _ => - return (q(pure_elim_intuitionistic $pf $f)) - | .inr _ => - let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q)) - | throwError "{tacName}: {A} is not affine and the goal not absorbing" - return q(pure_elim_spatial (A := $A) $pf $f) + return ← iPureCoreBuildProof φ inst pf f tacName def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop)) (e goal : Q($prop)) (tacName : String) : @@ -97,12 +144,12 @@ def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop)) Lean context. -/ elab "ipure " colGt hyp:ident : tactic => do - ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do + ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do let ivar ← hyps.findWithInfo hyp let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar - let pf ← iPureCore bi e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf "ipure" <| addBIGoal hyps' goal + let pf ← iPureCore e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf "ipure" <| addBIGoal hyps' goal mvar.assign pf @@ -111,12 +158,12 @@ elab "ipure " colGt hyp:ident : tactic => do regular Lean context and destructs it using the `rcases` destruction pattern. -/ elab "ipure " colGt hyp:ident " as " pat:rcasesPat : tactic => do - ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do + ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do let ivar ← hyps.findWithInfo hyp let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar - let pf ← iPureCore bi e e' p out' goal pat pf "ipure" <| addBIGoal hyps' goal + let pf ← iPureCore e e' p out' goal pat pf "ipure" <| addBIGoal hyps' goal mvar.assign pf diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 9c3e756bf..92b564eac 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -1806,16 +1806,26 @@ example [BI PROP] (m n : Nat) (a b c : Prop) : /- Tests `icases` with a case destruction pattern for rewriting but the - hypothesis is not a pure equality + hypothesis is not a pure equality. -/ /-- error: Invalid rewrite argument: Expected an equality or iff proof or -definition name, but `✝` is a proof of +definition name, but `a✝` is a proof of P -/ #guard_msgs in example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by iintro HP icases HP with → +/- + Tests `icases` with a case destruction pattern for rewriting but the + hypothesis is not a pure hypothesis. +-/ +/-- error: icases: P is not pure -/ +#guard_msgs in +example [BI PROP] (P : PROP) : ⊢@{PROP} P -∗ True := by + iintro HP + icases HP with → + /-- Tests `icases` with non-trivial `rcases` destruction patterns -/ example [BI PROP] (a b c1 c2 c3 : Prop) (P : Prop → Prop) : ⊢@{PROP} □ ⌜((a = b ∧ (b ∨ (c1 ∧ c2 ∧ c3))) ∧ ∃ x, P x)⌝ -∗ ⌜a ∨ c1⌝ ∗ ⌜∃ x, P x⌝ := by From c59afb610e4dd01967958f1c172eef3ba118508d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 3 Jul 2026 18:09:26 +0200 Subject: [PATCH 53/53] Generalise `Hyps.add` and `Hyps.addWithInfo` to resolve two TODO items --- Iris/Iris/ProofMode/Expr.lean | 15 ++++++++------- Iris/Iris/ProofMode/Tactics/Cases.lean | 15 ++++++--------- Iris/Iris/ProofMode/Tactics/Specialize.lean | 4 ++-- 3 files changed, 16 insertions(+), 18 deletions(-) diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean index c9f86ea0b..8b75781df 100644 --- a/Iris/Iris/ProofMode/Expr.lean +++ b/Iris/Iris/ProofMode/Expr.lean @@ -140,12 +140,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e := .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name ivar ty)) name ivar p ty ⟨⟩ --- TODO: should this ensure that adding a hypothesis to emp creates a --- hyp node instead of a sep node? def Hyps.add {prop : Q(Type u)} (bi : Q(BI $prop)) (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e) - : Hyps bi q(iprop($e ∗ □?$p $ty)) := - Hyps.mkSep h (.mkHyp bi name ivar p ty) + : (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e')) := + match h with + -- Adding a hypothesis to `emp` creates a `.hyp` node instead of a `.sep` node + | .emp _ => ⟨_, .mkHyp bi name ivar p ty, q(emp_sep)⟩ + | _ => ⟨_, .mkSep h (.mkHyp bi name ivar p ty), q(.rfl)⟩ partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) : Option ((s : Q($prop)) × Hyps bi s) := do @@ -533,9 +534,9 @@ def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : Me /-- Hyps.addWithInfo should be used by tactics that introduce a hypothesis based on the name given by the user. -/ def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop)) (name : TSyntax ``binderIdent) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e) - : MetaM (IVarId × Hyps bi q(iprop($e ∗ □?$p $ty))) := do + : MetaM (IVarId × (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e'))) := do let ivar' ← mkFreshIVarId (isTrue p) let (nameTo, nameRef) ← getFreshName name addHypInfo nameRef nameTo ivar' prop ty (isBinder := true) - let hyps := Hyps.add bi nameTo ivar' p ty h - return ⟨ivar', hyps⟩ + let ⟨e', hyps, pf⟩ := Hyps.add bi nameTo ivar' p ty h + return ⟨ivar', e', hyps, pf⟩ diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 348a6516d..519cb2599 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -205,22 +205,19 @@ partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P} withRef pat.ref do match pat with | .one _ name => do - -- TODO: use Hyps.addWithInfo here? - let (name, ref) ← getFreshName name - let ivar ← mkFreshIVarId (isTrue p) - addHypInfo ref name ivar prop A (isBinder := true) - let hyp := .mkHyp bi name ivar p A - if let .emp _ := hyps then pure q(of_emp_sep $(← k hyp goal)) - else k (.mkSep hyps hyp) goal + let ⟨_, _, hyps', pfEq⟩ ← Hyps.addWithInfo bi name p A hyps + let pf ← k hyps' goal + return q($(pfEq).mp.trans $pf) | .clear _ => let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) tacName pure q($pf $(← k hyps goal)) | .frame _ => - let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps + let ⟨ivar, _, hyps', pfEq⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩] - res.finish k + let pf ← res.finish k + return q($(pfEq).mp.trans $pf) | .conjunction _ [arg] | .disjunction _ [arg] => iCasesCore hyps goal arg p A tacName k diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean index 687b8ce8d..6af7ef139 100644 --- a/Iris/Iris/ProofMode/Tactics/Specialize.lean +++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean @@ -194,6 +194,6 @@ elab "ispecialize " colGt pmt:pmTerm : tactic => do | throwError "ispecialize: cannot find argument" let ⟨_, hyps'', pb, B, pf'⟩ ← iSpecializeCore hyps' p out pmt.spats - let hyps''' := Hyps.add bi name ivar pb B hyps'' + let ⟨_, hyps''', pfEq⟩ := Hyps.add bi name ivar pb B hyps'' let pf'' ← addBIGoal hyps''' goal - mvar.assign q(($pf).1.trans <| $(pf').trans <| $pf'') + mvar.assign q(($pf).1.trans <| $(pf').trans <| $(pfEq).mp.trans $pf'')