From 46a078995c0e9e91e566225953f60a722ab14484 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 26 May 2026 14:43:44 +0200
Subject: [PATCH 01/54] Start implementing iinduction: move IntoIH from
 Induction.lean to Classes.lean and its type class instances to Instances.lean

---
 Iris/Iris/ProofMode/Classes.lean           | 15 +++-
 Iris/Iris/ProofMode/Instances.lean         | 30 ++++++++
 Iris/Iris/ProofMode/Tactics.lean           |  1 +
 Iris/Iris/ProofMode/Tactics/Induction.lean | 88 +++++++++++-----------
 4 files changed, 85 insertions(+), 49 deletions(-)

diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index fdbe326cb..18868a05a 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.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, Michael Sammler, Alvin Tang
+Authors: Lars König, Michael Sammler, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -208,18 +208,27 @@ class IntoLaterN {PROP} [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : o
 export IntoLaterN (into_laterN)
 
 /-- `CombineSepAs` combines two propositions `P` and `Q` into `R` -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepAs]
 class CombineSepAs [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_as : P ∗ Q ⊢ R
 export CombineSepAs (combine_sep_as)
 
 /-- `CombineSepGives` combines two propositions `P` and `Q` for a proposition
     with the `<pers>` modality -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepGives]
 class CombineSepGives [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_gives : P ∗ Q ⊢ <pers> R
 export CombineSepGives (combine_sep_gives)
 
+/-
+  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
+  hypothesis `Q` under an intuitionistic BI context `□ P`.
+-/
+@[ipm_class, rocq_alias IntoIH]
+class IntoIH [BI PROP] (φ : Prop) (P : PROP) (Q : outParam PROP) where
+  into_ih : φ → □ P ⊢ Q
+export IntoIH (into_ih)
+
 #rocq_ignore elim_inv_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore elim_modal_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore from_and_tc_opaque "No tc_opaque in Lean"
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 53fecb860..ee702a834 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -7,6 +7,7 @@ module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
 public import Iris.ProofMode.ModalityInstances
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
@@ -917,3 +918,32 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     [h : CombineSepGives Q1 Q2 P] :
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_2.trans (persistently_mono h.combine_sep_gives)
+
+-- TODO: two more instances [into_ih_Forall] and [into_ih_Forall2]
+-- have not been implemented
+
+@[rocq_alias into_ih_entails]
+instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
+  into_ih := λ hpq => intuitionistically_elim.trans hpq
+
+@[rocq_alias into_ih_forall]
+instance intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (∀ x, φ x) P (BI.forall Φ) where
+  into_ih := by
+    intro hφ
+    apply forall_intro
+    intro x
+    exact (h x).into_ih (hφ x)
+
+@[rocq_alias into_ih_impl]
+instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
+    [h1 : MakeAffinely iprop(⌜φ⌝) P]
+    [h2 : IntoIH ψ Δ Q] :
+    IntoIH (φ → ψ) Δ iprop(P -∗ Q) where
+  into_ih := by
+    intro hImp
+    apply wand_intro
+    refine (sep_mono_r h1.make_affinely.mpr).trans ?_
+    refine persistent_and_affinely_sep_r.2.trans ?_
+    exact pure_elim_r (fun hφ => h2.into_ih (hImp hφ))
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 361255881..f74191c1c 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -12,6 +12,7 @@ public meta import Iris.ProofMode.Tactics.ExFalso
 public meta import Iris.ProofMode.Tactics.Exists
 public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
+public meta import Iris.ProofMode.Tactics.Induction
 public meta import Iris.ProofMode.Tactics.Intro
 public meta import Iris.ProofMode.Tactics.LeftRight
 public meta import Iris.ProofMode.Tactics.Loeb
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 533818f9f..177106c22 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -1,59 +1,55 @@
 /-
 Copyright (c) 2026 Yunsong Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yunsong Yang
+Authors: Yunsong Yang, Alvin Tang
 -/
 module
 
-public import Iris.ProofMode.ClassesMake
 public meta import Iris.ProofMode.Tactics.Basic
+public meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.ClassesMake
+public meta import Iris.ProofMode.Tactics.RevertIntro
 
 namespace Iris.ProofMode
 
-public section
-open BI Std
+public meta section
+open BI Std Lean Elab Tactic Meta Qq
 
-/-
-  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
-  hypothesis `Q` under an intuitionistic BI context `□ P`.
+private def iInductionCore {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
+    (hyps : Hyps bi e) (goal : Q($prop)) :
+    ProofModeM (Q($e ⊢ $goal)) := sorry
+
+/--
+  Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
+  the subset of hypotheses in `hyps` that contains the `fvar`.
 -/
-@[ipm_class]
-class IntoIH [BI PROP] (φ : Prop) (P : PROP) (Q : outParam PROP) where
-  into_ih : φ → □ P ⊢ Q
-
--- TODO: two more instances [into_ih_Forall] and [into_ih_Forall2]
--- have not been implemented
-instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
-  into_ih := λ hpq => intuitionistically_elim.trans hpq
-instance intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
-    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
-    IntoIH (∀ x, φ x) P (BI.forall Φ) where
-  into_ih := by
-    intro hφ
-    apply forall_intro
-    intro x
-    exact (h x).into_ih (hφ x)
-instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
-    [h1 : MakeAffinely iprop(⌜φ⌝) P]
-    [h2 : IntoIH ψ Δ Q] :
-    IntoIH (φ → ψ) Δ iprop(P -∗ Q) where
-  into_ih := by
-    intro hImp
-    apply wand_intro
-    refine (sep_mono_r h1.make_affinely.mpr).trans ?_
-    refine persistent_and_affinely_sep_r.2.trans ?_
-    exact pure_elim_r (fun hφ => h2.into_ih (hImp hφ))
-
-theorem ih_revert [BI PROP] {Δ P Q : PROP} {φ : Prop} (hφ : φ)
-    [hP : IntoIH φ Δ P]
-    (hΔ : Δ ⊢ □ Δ)
-    (hPQ : Δ ⊢ iprop(<pers> P → Q)) :
-    Δ ⊢ Q := by
-  have hP' : □ Δ ⊢ <pers> P :=
-    (intuitionistically_intro' (hP.into_ih hφ)).trans persistently_of_intuitionistically
-  have hAnd : □ Δ ⊢ iprop(<pers> P ∧ (<pers> P → Q)) :=
-    and_intro hP' <| intuitionistically_elim.trans hPQ
-  exact hΔ.trans <| hAnd.trans (imp_elim_r (P := iprop(<pers> P)) (Q := Q))
+private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
+    (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
+  let ivars := hyps.spatialIVarIds ++ hyps.intuitionisticIVarIds
 
-public meta section
-open Lean Elab Tactic Meta Qq
+  let containing := ivars.filter fun ivar =>
+    match hyps.getDecl? ivar with
+    | some (_, _, _, ty) => ty.containsFVar fvar
+    | none => false
+
+  containing.map (fun ivar => { kind := .ipm ivar, explicit := false })
+
+elab "iinduction" colGt x:ident : tactic => do
+  -- Get the ID of the variable on which induction is being performed
+  let fvar ← getFVarId x
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    -- Find all hypotheses that contain the variable being performed induction on
+    let targets := iHypsContaining hyps fvar
+
+    -- Revert all hypotheses in the list
+    let pf ← iRevertIntro hyps goal targets (
+      fun hyps' goal' k => do
+        -- Use built-in induction in Lean
+        evalTactic (← `(tactic| induction x:id))
+        k hyps' goal'
+    )
+
+    mvar.assign pf

From 5421a78bf21beeb1fc0f11572d12b2b02cf36542 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 14:13:30 +0200
Subject: [PATCH 02/54] Simple iinduction test

---
 Iris/Iris/Tests/Tactics.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index edfb8d86c..538bb0b55 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2715,3 +2715,12 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section iinduction
+
+example [BI PROP] {P Q : PROP} {n : Nat} :
+    ⊢ P -∗ ⌜n = 0⌝ -∗ Q -∗ ⌜n ≠ 1⌝ -∗ P ∗ Q ∗ ⌜n = n⌝ := by
+  iintro H1 H2 H3 #H4
+  iinduction n
+
+end iinduction

From 562fd6478468200912e696cdcd47a021aeca550c Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 14:27:57 +0200
Subject: [PATCH 03/54] Use evalTacticAt for iinduction

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 177106c22..060967509 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -47,8 +47,10 @@ elab "iinduction" colGt x:ident : tactic => do
     -- Revert all hypotheses in the list
     let pf ← iRevertIntro hyps goal targets (
       fun hyps' goal' k => do
-        -- Use built-in induction in Lean
-        evalTactic (← `(tactic| induction x:id))
+        -- Create a new metavariable for the proof goal upon reverting hypotheses
+        let m ← mkBIGoal hyps' goal'
+        -- Use built-in induction in Lean to generate the subgoals for induction
+        let subgoals ← evalTacticAt (← `(tactic| induction $x:ident)) m.mvarId!
         k hyps' goal'
     )
 

From 9af4f6f7e8a7868579575bcb6f093c21838c9f23 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 14:54:13 +0200
Subject: [PATCH 04/54] Try using iRevertCore and iIntroCore separately

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 32 ++++++++++++++++++++--
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 060967509..80bc6b6d6 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -45,13 +45,39 @@ elab "iinduction" colGt x:ident : tactic => do
     let targets := iHypsContaining hyps fvar
 
     -- Revert all hypotheses in the list
-    let pf ← iRevertIntro hyps goal targets (
-      fun hyps' goal' k => do
+    let pf ← iRevertCore targets hyps goal (
+
+      let names : List (Syntax × IntroPat) := ← targets.mapM (fun
+      | {kind := .pure id, ..} => do
+          let name ← Lean.mkIdent <$> id.getUserName
+          let ident ← `(binderIdent| $name:ident)
+          return (name, IntroPat.intro <| .pure ident)
+      | {kind := .ipm ivar, ..} => do
+          let name ← Lean.mkIdent <$> (hyps.getUserName? ivar).getM
+          let ident ← `(binderIdent| $name:ident)
+          return (name, IntroPat.intro <| (if ivar.persistent? then iCasesPat.intuitionistic else id) <| .one ident)
+      )
+
+      -- The function takes the hypotheses and goal after reverting
+      fun hyps' goal' => do
         -- Create a new metavariable for the proof goal upon reverting hypotheses
         let m ← mkBIGoal hyps' goal'
+
         -- Use built-in induction in Lean to generate the subgoals for induction
         let subgoals ← evalTacticAt (← `(tactic| induction $x:ident)) m.mvarId!
-        k hyps' goal'
+
+        for s in subgoals do
+          s.withContext do
+            let sType ← instantiateMVars (← s.getType)
+
+            let some irisGoal := parseIrisGoal? sType
+            -- This should not happen
+            | throwError "iinduction: fail to parse induction subgoal"
+
+            let casePf ← iIntroCore irisGoal.hyps irisGoal.goal names
+            s.assign casePf
+
+        return m
     )
 
     mvar.assign pf

From 72fd7a0be2be9f4c72565c160227b115d541dc2d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 14:55:52 +0200
Subject: [PATCH 05/54] Finish the proof for iinduction

---
 Iris/Iris/Tests/Tactics.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 538bb0b55..5681c1bd3 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2722,5 +2722,8 @@ example [BI PROP] {P Q : PROP} {n : Nat} :
     ⊢ P -∗ ⌜n = 0⌝ -∗ Q -∗ ⌜n ≠ 1⌝ -∗ P ∗ Q ∗ ⌜n = n⌝ := by
   iintro H1 H2 H3 #H4
   iinduction n
+  · iframe
+  · iframe
+    itrivial
 
 end iinduction

From a7aeae1b5b676cef69769c79bd8c33838be538b1 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 16:08:03 +0200
Subject: [PATCH 06/54] Use iRevertIntro instead of iRevertCore and iIntroCore
 separately This also requires generalisation of ProofModeContinuation

---
 Iris/Iris/ProofMode/Tactics/Induction.lean   | 20 ++++----------------
 Iris/Iris/ProofMode/Tactics/RevertIntro.lean |  8 ++++----
 2 files changed, 8 insertions(+), 20 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 80bc6b6d6..e3f640d21 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -45,27 +45,16 @@ elab "iinduction" colGt x:ident : tactic => do
     let targets := iHypsContaining hyps fvar
 
     -- Revert all hypotheses in the list
-    let pf ← iRevertCore targets hyps goal (
-
-      let names : List (Syntax × IntroPat) := ← targets.mapM (fun
-      | {kind := .pure id, ..} => do
-          let name ← Lean.mkIdent <$> id.getUserName
-          let ident ← `(binderIdent| $name:ident)
-          return (name, IntroPat.intro <| .pure ident)
-      | {kind := .ipm ivar, ..} => do
-          let name ← Lean.mkIdent <$> (hyps.getUserName? ivar).getM
-          let ident ← `(binderIdent| $name:ident)
-          return (name, IntroPat.intro <| (if ivar.persistent? then iCasesPat.intuitionistic else id) <| .one ident)
-      )
-
+    let pf ← iRevertIntro hyps goal targets (
       -- The function takes the hypotheses and goal after reverting
-      fun hyps' goal' => do
+      fun hyps' goal' k => do
         -- Create a new metavariable for the proof goal upon reverting hypotheses
         let m ← mkBIGoal hyps' goal'
 
         -- Use built-in induction in Lean to generate the subgoals for induction
         let subgoals ← evalTacticAt (← `(tactic| induction $x:ident)) m.mvarId!
 
+        -- Handle each subgoal
         for s in subgoals do
           s.withContext do
             let sType ← instantiateMVars (← s.getType)
@@ -74,8 +63,7 @@ elab "iinduction" colGt x:ident : tactic => do
             -- This should not happen
             | throwError "iinduction: fail to parse induction subgoal"
 
-            let casePf ← iIntroCore irisGoal.hyps irisGoal.goal names
-            s.assign casePf
+            s.assign <| ← k irisGoal.hyps irisGoal.goal
 
         return m
     )
diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
index 380de3c6d..70d0e2e52 100644
--- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
+++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
@@ -13,16 +13,16 @@ open Lean Meta Elab.Tactic Qq
 
 public meta section
 
-abbrev ProofModeContinuation (u : Level) :=
-  ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
-    (_hyps : Hyps bi e)(goal: 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)
 
 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

From 6203c5f3189c895c46e27cc0efa185968afcd53f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 16:27:17 +0200
Subject: [PATCH 07/54] Remove redundant Iris entailment in Lean context

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index e3f640d21..12e1fc113 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -36,6 +36,16 @@ private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
 
   containing.map (fun ivar => { kind := .ipm ivar, explicit := false })
 
+/-- Clear all local hypotheses whose type parses as an IrisGoal. -/
+private def clearIrisGoalHyps (s : MVarId) : MetaM MVarId :=
+  s.withContext do
+    (← getLCtx).foldlM (fun s' ldecl => do
+      if ldecl.isAuxDecl then return s'
+      if (parseIrisGoal? (← instantiateMVars ldecl.type)).isSome then
+        try s'.clear ldecl.fvarId
+        catch _ => pure s'
+      else pure s') s
+
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -56,6 +66,7 @@ elab "iinduction" colGt x:ident : tactic => do
 
         -- Handle each subgoal
         for s in subgoals do
+          let s ← clearIrisGoalHyps s
           s.withContext do
             let sType ← instantiateMVars (← s.getType)
 

From 7035695bdcd3ce14e6b9a055c87f5e383b1d03d4 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 16:50:00 +0200
Subject: [PATCH 08/54] Avoid unnamed variable in generated induction subgoals

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 7 +++++++
 Iris/Iris/Tests/Tactics.lean               | 8 ++++++++
 2 files changed, 15 insertions(+)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 12e1fc113..1e347890e 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -67,6 +67,13 @@ elab "iinduction" colGt x:ident : tactic => do
         -- Handle each subgoal
         for s in subgoals do
           let s ← clearIrisGoalHyps s
+
+          let s ← (
+            do
+              let [s'] ← evalTacticAt (← `(tactic| rename_i $x:ident)) s | pure s
+              pure s'
+          ) <|> pure s
+
           s.withContext do
             let sType ← instantiateMVars (← s.getType)
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 5681c1bd3..b9b86b40f 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2726,4 +2726,12 @@ example [BI PROP] {P Q : PROP} {n : Nat} :
   · iframe
     itrivial
 
+example [BI PROP] {P Q : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ ⌜n + 0 = n⌝ := by
+  iintro H1 #H2
+  iinduction n
+  · iframe
+  · iframe
+    itrivial
+
 end iinduction

From e963f76210f35ad3f1358edb4230a55a189ddbe8 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 17:50:30 +0200
Subject: [PATCH 09/54] Revert all hypotheses in the intuitionistic context

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 30 +++-------------------
 1 file changed, 4 insertions(+), 26 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 1e347890e..fb8d6dd74 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -17,34 +17,20 @@ namespace Iris.ProofMode
 public meta section
 open BI Std Lean Elab Tactic Meta Qq
 
-private def iInductionCore {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
-    (hyps : Hyps bi e) (goal : Q($prop)) :
-    ProofModeM (Q($e ⊢ $goal)) := sorry
-
 /--
   Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
   the subset of hypotheses in `hyps` that contains the `fvar`.
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
-  let ivars := hyps.spatialIVarIds ++ hyps.intuitionisticIVarIds
-
-  let containing := ivars.filter fun ivar =>
+  let intuitionisticIVarIds := hyps.intuitionisticIVarIds.filter fun ivar =>
     match hyps.getDecl? ivar with
     | some (_, _, _, ty) => ty.containsFVar fvar
     | none => false
 
-  containing.map (fun ivar => { kind := .ipm ivar, explicit := false })
-
-/-- Clear all local hypotheses whose type parses as an IrisGoal. -/
-private def clearIrisGoalHyps (s : MVarId) : MetaM MVarId :=
-  s.withContext do
-    (← getLCtx).foldlM (fun s' ldecl => do
-      if ldecl.isAuxDecl then return s'
-      if (parseIrisGoal? (← instantiateMVars ldecl.type)).isSome then
-        try s'.clear ldecl.fvarId
-        catch _ => pure s'
-      else pure s') s
+  (hyps.spatialIVarIds ++ intuitionisticIVarIds).map (
+    fun ivar => { kind := .ipm ivar, explicit := false }
+  )
 
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
@@ -66,14 +52,6 @@ elab "iinduction" colGt x:ident : tactic => do
 
         -- Handle each subgoal
         for s in subgoals do
-          let s ← clearIrisGoalHyps s
-
-          let s ← (
-            do
-              let [s'] ← evalTacticAt (← `(tactic| rename_i $x:ident)) s | pure s
-              pure s'
-          ) <|> pure s
-
           s.withContext do
             let sType ← instantiateMVars (← s.getType)
 

From d9fa30a0dae158a2b19db9fea3b68c0c0169c3ca Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 28 May 2026 18:27:49 +0200
Subject: [PATCH 10/54] Towards using IntoIH for moving induction hypothesis
 from Lean's context into Iris proof state

---
 Iris/Iris/ProofMode/Expr.lean              |  6 ++++
 Iris/Iris/ProofMode/Tactics/Induction.lean | 34 +++++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index 481b3bcc5..870a0c1bc 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -189,6 +189,12 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
+partial def Hyps.intuitionisticProps {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Q($prop)
+  | _, .emp _ => []
+  | _, .hyp _ _ _ p ty _ => if isTrue p then [ty] else []
+  | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticProps ++ rhs.intuitionisticProps
+
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index fb8d6dd74..b964e1884 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -32,6 +32,32 @@ private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     fun ivar => { kind := .ipm ivar, explicit := false }
   )
 
+private def intuitionisticHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (h : Hyps bi e) : ProofModeM Q($prop) := do
+  let props : List Q($prop) := h.intuitionisticProps
+  if props.isEmpty then
+    return q(emp)
+  else
+    return props.foldl (fun acc ty => q(iprop($acc ∗ $ty))) props[0]!
+
+private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (φ : Q(Prop)) (hFVar : FVarId) :
+    ProofModeM (Hyps bi e) := do
+  let P : Q($prop) ← intuitionisticHyps hyps
+
+  let Q ← mkFreshExprMVarQ q($prop)
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
+  | throwError "iinduction: type class synthesis failed"
+
+  let dummyIdent ← `(binderIdent| _)
+  let ⟨newName, newIdent⟩ ← getFreshName dummyIdent
+
+  let ⟨ivar, newHyps⟩ ← Hyps.addWithInfo bi dummyIdent q(true) Q hyps
+
+  return sorry
+
+private def findIH : ProofModeM FVarId := sorry
+
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -59,7 +85,13 @@ elab "iinduction" colGt x:ident : tactic => do
             -- This should not happen
             | throwError "iinduction: fail to parse induction subgoal"
 
-            s.assign <| ← k irisGoal.hyps irisGoal.goal
+            -- Find the induction hypothesis generated by Lean's `induction` tactic
+            let ihFVar ← findIH
+
+            -- Introduce the induction hypothesis back into the Iris proof state
+            let newHyps ← addIntoIH irisGoal.hyps (← inferType <| mkFVar ihFVar) ihFVar
+
+            s.assign <| ← k newHyps irisGoal.goal
 
         return m
     )

From ffcdbb38c32b1c027623cc3b33bc4efdb5fd0b10 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 10:16:48 +0200
Subject: [PATCH 11/54] Revert only spatial and intuitionistic hypotheses that
 contain x

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index b964e1884..39c7a65dc 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -23,12 +23,12 @@ open BI Std Lean Elab Tactic Meta Qq
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
-  let intuitionisticIVarIds := hyps.intuitionisticIVarIds.filter fun ivar =>
+  let ivars := (hyps.spatialIVarIds ++ hyps.intuitionisticIVarIds).filter fun ivar =>
     match hyps.getDecl? ivar with
     | some (_, _, _, ty) => ty.containsFVar fvar
     | none => false
 
-  (hyps.spatialIVarIds ++ intuitionisticIVarIds).map (
+  ivars.map (
     fun ivar => { kind := .ipm ivar, explicit := false }
   )
 

From e94141bbe37e5230a8a888cba535b7933f2a2cc2 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 10:30:08 +0200
Subject: [PATCH 12/54] Use the result of IntoIH synthesis in addIntoIH

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 39c7a65dc..026a6cf32 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -40,21 +40,25 @@ private def intuitionisticHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   else
     return props.foldl (fun acc ty => q(iprop($acc ∗ $ty))) props[0]!
 
+/--
+  Used for every induction hypothesis generated by Lean upon using the built-in
+  `induction` tactic. The type class `IntoIH` is used for obtaining the
+  corresponding proposition in the Iris proof mode.
+-/
 private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (φ : Q(Prop)) (hFVar : FVarId) :
-    ProofModeM (Hyps bi e) := do
+    ProofModeM ((e' : Q($prop)) × Hyps bi e') := do
   let P : Q($prop) ← intuitionisticHyps hyps
 
   let Q ← mkFreshExprMVarQ q($prop)
-  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
-  | throwError "iinduction: type class synthesis failed"
-
-  let dummyIdent ← `(binderIdent| _)
-  let ⟨newName, newIdent⟩ ← getFreshName dummyIdent
+  let some _ ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
+  | throwError "iinduction: type class synthesis with IntoIH failed"
 
-  let ⟨ivar, newHyps⟩ ← Hyps.addWithInfo bi dummyIdent q(true) Q hyps
+  let nameIdent := mkIdent <| ← hFVar.getUserName
+  let binderIdent ← `(binderIdent| $nameIdent:ident)
+  let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q hyps
 
-  return sorry
+  return ⟨_, newHyps⟩
 
 private def findIH : ProofModeM FVarId := sorry
 
@@ -91,7 +95,7 @@ elab "iinduction" colGt x:ident : tactic => do
             -- Introduce the induction hypothesis back into the Iris proof state
             let newHyps ← addIntoIH irisGoal.hyps (← inferType <| mkFVar ihFVar) ihFVar
 
-            s.assign <| ← k newHyps irisGoal.goal
+            -- s.assign <| ← k newHyps irisGoal.goal
 
         return m
     )

From 8ba460a52638d46179b981a5bdf5c716de7bf2a7 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 10:44:12 +0200
Subject: [PATCH 13/54] Iteratively add induction hypotheses into the Iris
 proof state

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 28 ++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 026a6cf32..59bf3be1f 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -60,7 +60,27 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return ⟨_, newHyps⟩
 
-private def findIH : ProofModeM FVarId := sorry
+/--
+  Search for all induction hypotheses generated by Lean's built-in `induction`
+  tactic and return their `FVarId` values as a list.
+-/
+private def findIHs : ProofModeM (List FVarId) := sorry
+
+/--
+  Introduce a list of induction hypotheses into Iris proof state.
+  The list of `FVarId` values (`ihFVars`) should be the list returned by
+  `findIHs`.
+-/
+private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (ihFVars : List FVarId) :
+    ProofModeM ((e' : Q($prop)) × Hyps bi e') := do
+  let mut current : (e' : Q($prop)) × Hyps bi e' := ⟨_, hyps⟩
+
+  for i in ihFVars do
+    let φ ← inferType (mkFVar i)
+    current ← addIntoIH current.snd φ i
+
+  return current
 
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
@@ -90,12 +110,12 @@ elab "iinduction" colGt x:ident : tactic => do
             | throwError "iinduction: fail to parse induction subgoal"
 
             -- Find the induction hypothesis generated by Lean's `induction` tactic
-            let ihFVar ← findIH
+            let ihFVars ← findIHs
 
             -- Introduce the induction hypothesis back into the Iris proof state
-            let newHyps ← addIntoIH irisGoal.hyps (← inferType <| mkFVar ihFVar) ihFVar
+            let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
 
-            -- s.assign <| ← k newHyps irisGoal.goal
+            s.assign <| ← k newHyps irisGoal.goal
 
         return m
     )

From 8524a82be7686c01af8c7e73ebc04d160982580f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 12:02:13 +0200
Subject: [PATCH 14/54] Towards implementing findIHs

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 59bf3be1f..b5563b04a 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -60,11 +60,26 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return ⟨_, newHyps⟩
 
+private def exprContainsConst (e : Expr) (n : Name) : Bool :=
+  (e.find? fun
+    | .const c _ => c == n
+    | _ => false).isSome
+
 /--
   Search for all induction hypotheses generated by Lean's built-in `induction`
   tactic and return their `FVarId` values as a list.
 -/
-private def findIHs : ProofModeM (List FVarId) := sorry
+private def findIHs : ProofModeM (List FVarId) := do
+  let lctx ← getLCtx
+  return ← lctx.decls.toList.filterMapM fun
+    | none => return none
+    | some ldecl =>
+      if ldecl.isAuxDecl || ldecl.isImplementationDetail
+        then return none
+      else
+        if exprContainsConst ldecl.type ``Entails'
+        then return some ldecl.fvarId
+        else return none
 
 /--
   Introduce a list of induction hypotheses into Iris proof state.

From 998ffb8b07b4d2c6cab8a74d320c39280ee4f42a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 16:02:48 +0200
Subject: [PATCH 15/54] Implement findIHs

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 35 ++++++++--------------
 1 file changed, 13 insertions(+), 22 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index b5563b04a..86f89379b 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -60,26 +60,17 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return ⟨_, newHyps⟩
 
-private def exprContainsConst (e : Expr) (n : Name) : Bool :=
-  (e.find? fun
-    | .const c _ => c == n
-    | _ => false).isSome
-
-/--
-  Search for all induction hypotheses generated by Lean's built-in `induction`
-  tactic and return their `FVarId` values as a list.
--/
-private def findIHs : ProofModeM (List FVarId) := do
-  let lctx ← getLCtx
-  return ← lctx.decls.toList.filterMapM fun
-    | none => return none
-    | some ldecl =>
-      if ldecl.isAuxDecl || ldecl.isImplementationDetail
-        then return none
-      else
-        if exprContainsConst ldecl.type ``Entails'
-        then return some ldecl.fvarId
-        else return none
+/-- Search for hypotheses in the regular Lean context that represent induction
+    hypotheses and return their IDs as a list. -/
+private def findIHs (m : MVarId) : MetaM (List FVarId) :=
+  m.withContext do
+    let lctx ← getLCtx
+    let mut ihs := []
+    for decl in lctx do
+      let type ← instantiateMVars decl.type
+      if isIrisGoal type.consumeMData then
+        ihs := (decl.fvarId) :: ihs
+    return ihs.reverse
 
 /--
   Introduce a list of induction hypotheses into Iris proof state.
@@ -124,8 +115,8 @@ elab "iinduction" colGt x:ident : tactic => do
             -- This should not happen
             | throwError "iinduction: fail to parse induction subgoal"
 
-            -- Find the induction hypothesis generated by Lean's `induction` tactic
-            let ihFVars ← findIHs
+            -- Find the induction hypotheses generated by Lean's `induction` tactic
+            let ihFVars ← findIHs s
 
             -- Introduce the induction hypothesis back into the Iris proof state
             let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars

From 4bc644cd142b2534489d7891fa4e8ebabf6a6fb6 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 16:04:48 +0200
Subject: [PATCH 16/54] Remove induction hypotheses from the regular Lean
 context

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 86f89379b..10fbe0e3a 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -121,7 +121,7 @@ elab "iinduction" colGt x:ident : tactic => do
             -- Introduce the induction hypothesis back into the Iris proof state
             let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
 
-            s.assign <| ← k newHyps irisGoal.goal
+            s.assign <| ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
 
         return m
     )

From 4f6817a6026c0b2f9b2fa260254c278c3ad8cecd Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 16:41:38 +0200
Subject: [PATCH 17/54] Adjust iHypsContaining

---
 Iris/Iris/ProofMode/Expr.lean              |  6 ++++++
 Iris/Iris/ProofMode/Tactics/Induction.lean | 10 ++++++----
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index 870a0c1bc..50c9cfa4a 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -195,6 +195,12 @@ partial def Hyps.intuitionisticProps {u prop bi} :
   | _, .hyp _ _ _ p ty _ => if isTrue p then [ty] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticProps ++ rhs.intuitionisticProps
 
+partial def Hyps.spatialProps {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Q($prop)
+  | _, .emp _ => []
+  | _, .hyp _ _ _ p ty _ => if isTrue p then [] else [ty]
+  | _, .sep _ _ _ _ lhs rhs => lhs.spatialProps ++ rhs.spatialProps
+
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 10fbe0e3a..338a563b5 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -23,12 +23,12 @@ open BI Std Lean Elab Tactic Meta Qq
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
-  let ivars := (hyps.spatialIVarIds ++ hyps.intuitionisticIVarIds).filter fun ivar =>
+  let ivars := hyps.intuitionisticIVarIds.filter fun ivar =>
     match hyps.getDecl? ivar with
     | some (_, _, _, ty) => ty.containsFVar fvar
     | none => false
 
-  ivars.map (
+  (ivars ++ hyps.spatialIVarIds).map (
     fun ivar => { kind := .ipm ivar, explicit := false }
   )
 
@@ -51,6 +51,8 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   let P : Q($prop) ← intuitionisticHyps hyps
 
   let Q ← mkFreshExprMVarQ q($prop)
+  logInfo m!"[DEBUG] φ: {φ}, P: {P}, Q: {Q}"
+
   let some _ ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
 
@@ -68,8 +70,8 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
     let mut ihs := []
     for decl in lctx do
       let type ← instantiateMVars decl.type
-      if isIrisGoal type.consumeMData then
-        ihs := (decl.fvarId) :: ihs
+      if isIrisGoal type then
+        ihs := decl.fvarId :: ihs
     return ihs.reverse
 
 /--

From ff5ea5c357844341d6c9a49da664bab32c50bcc2 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Fri, 29 May 2026 17:33:13 +0200
Subject: [PATCH 18/54] Introducing IHs into the Iris intuitionstic context

To-do:
1. Bug: Some kernel mismatch error when the tactic is used
2. Bug: The variable being performed induction on becomes unnamed
3. Bug: The induction hypotheses are unnamed
4. Feature: Introduction patterns
---
 Iris/Iris/ProofMode/Expr.lean              |  8 +-------
 Iris/Iris/ProofMode/Tactics/Induction.lean | 13 +++++++++----
 Iris/Iris/Tests/Tactics.lean               |  8 ++++----
 3 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index 50c9cfa4a..a45f3e023 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -192,15 +192,9 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
 partial def Hyps.intuitionisticProps {u prop bi} :
     ∀ {s}, @Hyps u prop bi s → List Q($prop)
   | _, .emp _ => []
-  | _, .hyp _ _ _ p ty _ => if isTrue p then [ty] else []
+  | _, .hyp tm _ _ p _ _ => if isTrue p then [tm] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticProps ++ rhs.intuitionisticProps
 
-partial def Hyps.spatialProps {u prop bi} :
-    ∀ {s}, @Hyps u prop bi s → List Q($prop)
-  | _, .emp _ => []
-  | _, .hyp _ _ _ p ty _ => if isTrue p then [] else [ty]
-  | _, .sep _ _ _ _ lhs rhs => lhs.spatialProps ++ rhs.spatialProps
-
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 338a563b5..321cfdf04 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -19,7 +19,8 @@ open BI Std Lean Elab Tactic Meta Qq
 
 /--
   Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
-  the subset of hypotheses in `hyps` that contains the `fvar`.
+  the subset of intuitionistic hypotheses in `hyps` that contains the `fvar`
+  and all spatial hypotheses in the proof state.
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
@@ -32,13 +33,18 @@ private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     fun ivar => { kind := .ipm ivar, explicit := false }
   )
 
+/--
+  Given `h` of type `Hyps bi e`, search for all hypotheses in the intuitionistic
+  context, concatenate them using the separation conjunction and return
+  it as a single proposition.
+-/
 private def intuitionisticHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (h : Hyps bi e) : ProofModeM Q($prop) := do
   let props : List Q($prop) := h.intuitionisticProps
   if props.isEmpty then
     return q(emp)
   else
-    return props.foldl (fun acc ty => q(iprop($acc ∗ $ty))) props[0]!
+    return props.tail.reverse.foldr (fun acc tm => q(iprop($tm ∗ $acc))) props[0]!
 
 /--
   Used for every induction hypothesis generated by Lean upon using the built-in
@@ -51,8 +57,6 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   let P : Q($prop) ← intuitionisticHyps hyps
 
   let Q ← mkFreshExprMVarQ q($prop)
-  logInfo m!"[DEBUG] φ: {φ}, P: {P}, Q: {Q}"
-
   let some _ ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
 
@@ -123,6 +127,7 @@ elab "iinduction" colGt x:ident : tactic => do
             -- Introduce the induction hypothesis back into the Iris proof state
             let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
 
+            -- Remove the IHs from the regular context
             s.assign <| ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
 
         return m
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index b9b86b40f..4d26742e9 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2726,11 +2726,11 @@ example [BI PROP] {P Q : PROP} {n : Nat} :
   · iframe
     itrivial
 
-example [BI PROP] {P Q : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ ⌜n + 0 = n⌝ := by
-  iintro H1 #H2
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
   iinduction n
-  · iframe
+  · itrivial
   · iframe
     itrivial
 

From 2f47ceb6edf1c8cf3db284b9d869d5e9539a8860 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 16:38:46 +0200
Subject: [PATCH 19/54] Use Lean.Meta.Tactic.induction instead of evalTacticAt
 for more flexibility regarding IH naming

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 321cfdf04..e0c817231 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -110,25 +110,26 @@ elab "iinduction" colGt x:ident : tactic => do
         let m ← mkBIGoal hyps' goal'
 
         -- Use built-in induction in Lean to generate the subgoals for induction
-        let subgoals ← evalTacticAt (← `(tactic| induction $x:ident)) m.mvarId!
+        let subgoals ←  m.mvarId!.withContext do
+          m.mvarId!.induction fvar `Nat.recOn #[]
 
         -- Handle each subgoal
         for s in subgoals do
-          s.withContext do
-            let sType ← instantiateMVars (← s.getType)
+          s.mvarId.withContext do
+            let sType ← instantiateMVars (← s.mvarId.getType)
 
             let some irisGoal := parseIrisGoal? sType
             -- This should not happen
             | throwError "iinduction: fail to parse induction subgoal"
 
             -- Find the induction hypotheses generated by Lean's `induction` tactic
-            let ihFVars ← findIHs s
+            let ihFVars ← findIHs s.mvarId
 
             -- Introduce the induction hypothesis back into the Iris proof state
             let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
 
             -- Remove the IHs from the regular context
-            s.assign <| ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
+            s.mvarId.assign <| ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
 
         return m
     )

From a9be948bedaf5ba85bfdf2507a9bcda8afb7288c Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 17:11:56 +0200
Subject: [PATCH 20/54] Generalisation to find recursor name for induction

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index e0c817231..c8546486b 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -102,6 +102,15 @@ elab "iinduction" colGt x:ident : tactic => do
     -- Find all hypotheses that contain the variable being performed induction on
     let targets := iHypsContaining hyps fvar
 
+    -- Find the recursor name for induction
+    let fvarType ← whnf <| ← inferType <| mkFVar fvar
+    let recName : Name ← match fvarType.getAppFn with
+    | Expr.const indName _ =>
+      match (← getEnv).find? indName with
+      | some (ConstantInfo.inductInfo val) => pure (Name.mkStr val.name "recOn")
+      | _ => throwError "iinduction: {indName} is not inductive"
+    | _ => throwError "iinduction: unable to determine inductive type"
+
     -- Revert all hypotheses in the list
     let pf ← iRevertIntro hyps goal targets (
       -- The function takes the hypotheses and goal after reverting
@@ -111,7 +120,7 @@ elab "iinduction" colGt x:ident : tactic => do
 
         -- Use built-in induction in Lean to generate the subgoals for induction
         let subgoals ←  m.mvarId!.withContext do
-          m.mvarId!.induction fvar `Nat.recOn #[]
+          m.mvarId!.induction fvar recName #[]
 
         -- Handle each subgoal
         for s in subgoals do

From c627c24dc93ece749ce084b746fddeb8a0afc777 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 17:26:19 +0200
Subject: [PATCH 21/54] Towards having explicit variable names for induction
 hypotheses

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index c8546486b..927a1d7bb 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -105,12 +105,17 @@ elab "iinduction" colGt x:ident : tactic => do
     -- Find the recursor name for induction
     let fvarType ← whnf <| ← inferType <| mkFVar fvar
     let recName : Name ← match fvarType.getAppFn with
-    | Expr.const indName _ =>
+    | .const indName _ =>
       match (← getEnv).find? indName with
-      | some (ConstantInfo.inductInfo val) => pure (Name.mkStr val.name "recOn")
+      | some (.inductInfo val) => pure <| Name.mkStr val.name "recOn"
       | _ => throwError "iinduction: {indName} is not inductive"
     | _ => throwError "iinduction: unable to determine inductive type"
 
+    let varNames : Array AltVarNames := #[
+        { explicit := true, varNames := [] },
+        { explicit := true, varNames := [x.getId, `IH] }
+      ]
+
     -- Revert all hypotheses in the list
     let pf ← iRevertIntro hyps goal targets (
       -- The function takes the hypotheses and goal after reverting
@@ -120,7 +125,7 @@ elab "iinduction" colGt x:ident : tactic => do
 
         -- Use built-in induction in Lean to generate the subgoals for induction
         let subgoals ←  m.mvarId!.withContext do
-          m.mvarId!.induction fvar recName #[]
+          m.mvarId!.induction fvar recName varNames
 
         -- Handle each subgoal
         for s in subgoals do

From a11f96700cbdcae75b6177329aea883ab3f914e7 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 18:03:21 +0200
Subject: [PATCH 22/54] Solve kernel mismatch, currently using a placeholder
 theorem

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 927a1d7bb..60ba83c1b 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -94,6 +94,16 @@ private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return current
 
+/--
+  The `iinduction` tactic user provides the proof for the induction subgoal,
+  which has hypotheses introduced into the Iris proof state.
+
+  Given this proof, obtain the proof where the hypotheses are not yet
+  introduced into the Iris proof state.
+-/
+@[rocq_alias tac_revert_ih]
+theorem revert_IH [BI PROP] {a b c d : PROP} (h : a ⊢ b) : c ⊢ d := sorry
+
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -142,8 +152,10 @@ elab "iinduction" colGt x:ident : tactic => do
             -- Introduce the induction hypothesis back into the Iris proof state
             let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
 
+            let pf ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
+
             -- Remove the IHs from the regular context
-            s.mvarId.assign <| ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
+            s.mvarId.assign <| (q(revert_IH $pf) : Q($irisGoal.e ⊢ $irisGoal.goal))
 
         return m
     )

From b304c88316b159f8992b96ff083cd0e5f991c706 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 18:36:31 +0200
Subject: [PATCH 23/54] Implement InductionState, towards finishing the
 placeholder theorem

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 92 ++++++++++++++--------
 1 file changed, 57 insertions(+), 35 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 60ba83c1b..bea34528f 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -46,63 +46,85 @@ private def intuitionisticHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   else
     return props.tail.reverse.foldr (fun acc tm => q(iprop($tm ∗ $acc))) props[0]!
 
+/-- Search for hypotheses in the regular Lean context that represent induction
+    hypotheses and return their IDs as a list. -/
+private def findIHs (m : MVarId) : MetaM (List FVarId) :=
+  m.withContext do
+    let lctx ← getLCtx
+    let mut ihs := []
+    for decl in lctx do
+      let type ← instantiateMVars decl.type
+      if isIrisGoal type then
+        ihs := decl.fvarId :: ihs
+    return ihs.reverse
+
+/--
+  The `iinduction` tactic user provides the proof for the induction subgoal,
+  which has hypotheses introduced into the Iris proof state.
+
+  Given this proof, obtain the proof where the hypotheses are not yet
+  introduced into the Iris proof state.
+-/
+@[rocq_alias tac_revert_ih]
+theorem revert_IH [BI PROP] {P Q R goal : PROP}
+  {φ : Prop}
+  (inst : IntoIH φ P Q)
+  (h : R ∗ □ Q ⊢ goal) : R ⊢ goal := sorry
+
+/--
+  Designed to be a mutable state such that `newHyps` contains induction
+  hypotheses generated by Lean's built-in induction.
+-/
+private structure InductionState {u} {prop : Q(Type u)} {bi} (origE goal : Q($prop)) where
+  {newE : Q($prop)}
+  (newHyps : Hyps bi newE)
+  (pf : Q(($newE ⊢ $goal) → $origE ⊢ $goal))
+
 /--
   Used for every induction hypothesis generated by Lean upon using the built-in
   `induction` tactic. The type class `IntoIH` is used for obtaining the
   corresponding proposition in the Iris proof mode.
 -/
-private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
-    (hyps : Hyps bi e) (φ : Q(Prop)) (hFVar : FVarId) :
-    ProofModeM ((e' : Q($prop)) × Hyps bi e') := do
+private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
+    (st : @InductionState u prop bi e goal)
+    (φ : Q(Prop)) (hFVar : FVarId) :
+    ProofModeM (@InductionState u prop bi e goal) := do
+
+  let hyps := st.newHyps
+
   let P : Q($prop) ← intuitionisticHyps hyps
 
   let Q ← mkFreshExprMVarQ q($prop)
-  let some _ ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
 
   let nameIdent := mkIdent <| ← hFVar.getUserName
   let binderIdent ← `(binderIdent| $nameIdent:ident)
   let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q hyps
 
-  return ⟨_, newHyps⟩
-
-/-- Search for hypotheses in the regular Lean context that represent induction
-    hypotheses and return their IDs as a list. -/
-private def findIHs (m : MVarId) : MetaM (List FVarId) :=
-  m.withContext do
-    let lctx ← getLCtx
-    let mut ihs := []
-    for decl in lctx do
-      let type ← instantiateMVars decl.type
-      if isIrisGoal type then
-        ihs := decl.fvarId :: ihs
-    return ihs.reverse
+  return {
+    newHyps,
+    pf := q(fun pf => $st.pf <| revert_IH $inst pf)
+  }
 
 /--
   Introduce a list of induction hypotheses into Iris proof state.
   The list of `FVarId` values (`ihFVars`) should be the list returned by
   `findIHs`.
 -/
-private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal : Q($prop)}
     (hyps : Hyps bi e) (ihFVars : List FVarId) :
-    ProofModeM ((e' : Q($prop)) × Hyps bi e') := do
-  let mut current : (e' : Q($prop)) × Hyps bi e' := ⟨_, hyps⟩
+    ProofModeM (@InductionState u prop bi e goal) := do
+
+  let mut st : InductionState e goal := {
+    newHyps := hyps, pf := q(id)
+  }
 
   for i in ihFVars do
     let φ ← inferType (mkFVar i)
-    current ← addIntoIH current.snd φ i
-
-  return current
-
-/--
-  The `iinduction` tactic user provides the proof for the induction subgoal,
-  which has hypotheses introduced into the Iris proof state.
+    st ← addIntoIH st φ i
 
-  Given this proof, obtain the proof where the hypotheses are not yet
-  introduced into the Iris proof state.
--/
-@[rocq_alias tac_revert_ih]
-theorem revert_IH [BI PROP] {a b c d : PROP} (h : a ⊢ b) : c ⊢ d := sorry
+  return st
 
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
@@ -150,12 +172,12 @@ elab "iinduction" colGt x:ident : tactic => do
             let ihFVars ← findIHs s.mvarId
 
             -- Introduce the induction hypothesis back into the Iris proof state
-            let ⟨_, newHyps⟩ ← addAllIHs irisGoal.hyps ihFVars
+            let st ← addAllIHs irisGoal.hyps ihFVars (goal := irisGoal.goal)
 
-            let pf ← withoutFVars (u := 0) ihFVars.toArray <| k newHyps irisGoal.goal
+            let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
 
             -- Remove the IHs from the regular context
-            s.mvarId.assign <| (q(revert_IH $pf) : Q($irisGoal.e ⊢ $irisGoal.goal))
+            s.mvarId.assign <| q($st.pf $pf')
 
         return m
     )

From 73951390a1a30bee46b5c5e396e767a026a9aa31 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 18:57:13 +0200
Subject: [PATCH 24/54] Finish revert_IH proof, more assumptions required

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 27 ++++++++++++++--------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index bea34528f..bbd0025cf 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -66,10 +66,17 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
   introduced into the Iris proof state.
 -/
 @[rocq_alias tac_revert_ih]
-theorem revert_IH [BI PROP] {P Q R goal : PROP}
-  {φ : Prop}
-  (inst : IntoIH φ P Q)
-  (h : R ∗ □ Q ⊢ goal) : R ⊢ goal := sorry
+theorem revert_IH [BI PROP] {P Q R goal : PROP} {φ}
+    (ih : φ)
+    (inst : IntoIH φ P Q)
+    (h1 : □ P ⊣⊢ R)
+    (h2 : R ∗ □ Q ⊢ goal) : R ⊢ goal := calc
+  R ⊢ □ P         := h1.mpr
+  _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
+  _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
+  _ ⊢ R ∗ □ Q     := sep_mono_l h1.mp
+  _ ⊢ goal        := h2
 
 /--
   Designed to be a mutable state such that `newHyps` contains induction
@@ -89,10 +96,10 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
     (st : @InductionState u prop bi e goal)
     (φ : Q(Prop)) (hFVar : FVarId) :
     ProofModeM (@InductionState u prop bi e goal) := do
+  let oldE := st.newE
+  let oldHyps : Hyps bi oldE := st.newHyps
 
-  let hyps := st.newHyps
-
-  let P : Q($prop) ← intuitionisticHyps hyps
+  let P : Q($prop) ← intuitionisticHyps oldHyps
 
   let Q ← mkFreshExprMVarQ q($prop)
   let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
@@ -100,11 +107,13 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
 
   let nameIdent := mkIdent <| ← hFVar.getUserName
   let binderIdent ← `(binderIdent| $nameIdent:ident)
-  let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q hyps
+  let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
+
+  let a := q(revert_IH sorry $inst (goal := $goal) (R := $oldE) sorry)
 
   return {
     newHyps,
-    pf := q(fun pf => $st.pf <| revert_IH $inst pf)
+    pf := q(fun pf => $st.pf <| $a pf)
   }
 
 /--

From cbdadb66503092964718ba350fd8c9f59838f233 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 19:24:01 +0200
Subject: [PATCH 25/54] Towards completing the use of InductionState

To-do:
1. Prove that the spatial context is empty after reverting hypotheses
2. Remaining tactic syntax
3. Remaining two IntoIH instance
---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 42 +++++++++++++++-------
 1 file changed, 29 insertions(+), 13 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index bbd0025cf..6e0bcfd4d 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -66,25 +66,35 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
   introduced into the Iris proof state.
 -/
 @[rocq_alias tac_revert_ih]
-theorem revert_IH [BI PROP] {P Q R goal : PROP} {φ}
+theorem revert_IH [BI PROP] {P Q goal : PROP} {φ}
     (ih : φ)
     (inst : IntoIH φ P Q)
-    (h1 : □ P ⊣⊢ R)
-    (h2 : R ∗ □ Q ⊢ goal) : R ⊢ goal := calc
-  R ⊢ □ P         := h1.mpr
+    (h1 : P ⊢ □ P)
+    (h2 : P ∗ □ Q ⊢ goal) : P ⊢ goal := calc
+  P ⊢ □ P         := h1
   _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
   _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
   _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
-  _ ⊢ R ∗ □ Q     := sep_mono_l h1.mp
+  _ ⊢ P ∗ □ Q     := sep_mono_l intuitionistically_elim
   _ ⊢ goal        := h2
 
+theorem stay_intuitionistic [BI PROP] {P Q : PROP}
+    (h1 : P ⊢ □ P) :
+    P ∗ □ Q ⊢ □ (P ∗ □ Q) := calc
+  _ ⊢ □ P ∗ □ Q   := sep_mono_l h1
+  _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
+
 /--
   Designed to be a mutable state such that `newHyps` contains induction
   hypotheses generated by Lean's built-in induction.
 -/
 private structure InductionState {u} {prop : Q(Type u)} {bi} (origE goal : Q($prop)) where
+  -- Hypotheses in the latest Iris proof goal
   {newE : Q($prop)}
   (newHyps : Hyps bi newE)
+  -- Proof that the hypotheses is intuitionsitic
+  (pfAux : Q($newE ⊢ □ $newE))
   (pf : Q(($newE ⊢ $goal) → $origE ⊢ $goal))
 
 /--
@@ -94,28 +104,33 @@ private structure InductionState {u} {prop : Q(Type u)} {bi} (origE goal : Q($pr
 -/
 private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
     (st : @InductionState u prop bi e goal)
-    (φ : Q(Prop)) (hFVar : FVarId) :
+    (φ : Q(Prop)) (p : Q($φ)) (hFVar : FVarId) :
     ProofModeM (@InductionState u prop bi e goal) := do
   let oldE := st.newE
   let oldHyps : Hyps bi oldE := st.newHyps
 
-  let P : Q($prop) ← intuitionisticHyps oldHyps
-
   let Q ← mkFreshExprMVarQ q($prop)
-  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $P $Q)
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $oldE $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
 
   let nameIdent := mkIdent <| ← hFVar.getUserName
   let binderIdent ← `(binderIdent| $nameIdent:ident)
   let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
 
-  let a := q(revert_IH sorry $inst (goal := $goal) (R := $oldE) sorry)
+  let a := q(revert_IH $p $inst (goal := $goal) $st.pfAux)
 
   return {
     newHyps,
-    pf := q(fun pf => $st.pf <| $a pf)
+    pf := q(fun pf => $st.pf <| $a pf),
+    pfAux := q(stay_intuitionistic $st.pfAux)
   }
 
+/--
+  This should be true in `addAllIHs` because all spatial hypotheses have
+  been reverted, so the Iris proof state contains no hypothesis in the
+  spatial context. -/
+theorem dummy [BI PROP] {e : PROP} : e ⊢ □ e := sorry
+
 /--
   Introduce a list of induction hypotheses into Iris proof state.
   The list of `FVarId` values (`ihFVars`) should be the list returned by
@@ -126,12 +141,13 @@ private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal : Q($pro
     ProofModeM (@InductionState u prop bi e goal) := do
 
   let mut st : InductionState e goal := {
-    newHyps := hyps, pf := q(id)
+    newHyps := hyps, pf := q(id), pfAux := q(dummy)
   }
 
   for i in ihFVars do
+    let p := mkFVar i
     let φ ← inferType (mkFVar i)
-    st ← addIntoIH st φ i
+    st ← addIntoIH st φ p i
 
   return st
 

From 5a5beaa254c06366981c93768370ded40852c6a6 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 20:39:20 +0200
Subject: [PATCH 26/54] Port type class instances into_ih_Forall and
 into_ih_Forall2

---
 Iris/Iris/ProofMode/Instances.lean | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index ee702a834..b6a8e63a7 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -919,9 +919,6 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_2.trans (persistently_mono h.combine_sep_gives)
 
--- TODO: two more instances [into_ih_Forall] and [into_ih_Forall2]
--- have not been implemented
-
 @[rocq_alias into_ih_entails]
 instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
   into_ih := λ hpq => intuitionistically_elim.trans hpq
@@ -947,3 +944,21 @@ instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
     refine (sep_mono_r h1.make_affinely.mpr).trans ?_
     refine persistent_and_affinely_sep_r.2.trans ?_
     exact pure_elim_r (fun hφ => h2.into_ih (hImp hφ))
+
+/-- Support for induction principles whose IH is guarded by `List.Forall`, e.g.
+    `∀ l, Forall P l → P (Tree l)` arising from nested inductive types like
+    `inductive ntree := Tree : List ntree → ntree`. -/
+@[rocq_alias into_ih_Forall]
+instance intoIH_listForall [BI PROP] (φ : α → Bool) (l : List α) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (l.all φ) P (bigSepL (fun _ a => iprop(□ Φ a)) l) where
+  into_ih := sorry
+
+/-- Support for induction principles whose IH is guarded by `List.Forall₂`, e.g.
+    arising from mutual inductive types relating two lists element-wise. -/
+@[rocq_alias into_ih_Forall2]
+instance intoIH_listForall₂ [BI PROP] (φ : α → β → Prop) (l1 : List α) (l2 : List β)
+    (P : PROP) (Φ : α → β → PROP)
+    [h : ∀ x1 x2, IntoIH (φ x1 x2) P (Φ x1 x2)] :
+    IntoIH (List.Forall₂ φ l1 l2) P (bigSepL2 (fun _ x1 x2 => iprop(□ Φ x1 x2)) l1 l2) where
+  into_ih := sorry

From aa5f430f0706e30bc8fb14b46039ffc7ed4bc475 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 21:42:38 +0200
Subject: [PATCH 27/54] Finish proof for intoIH_listForall

---
 Iris/Iris/ProofMode/Instances.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index b6a8e63a7..e6090b814 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -952,7 +952,20 @@ instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
 instance intoIH_listForall [BI PROP] (φ : α → Bool) (l : List α) (P : PROP) (Φ : α → PROP)
     [h : ∀ x, IntoIH (φ x) P (Φ x)] :
     IntoIH (l.all φ) P (bigSepL (fun _ a => iprop(□ Φ a)) l) where
-  into_ih := sorry
+  into_ih := by
+    intro h1
+    induction l generalizing Φ with
+    | nil =>
+      simp [affine]
+    | cons x xs ih =>
+      simp [List.all, bigSepL] at h1 ⊢
+      rcases h1 with ⟨hx, hxs⟩
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro' ((h x).into_ih hx)
+      · apply ih
+        apply (List.all_eq_true.mpr)
+        apply hxs
 
 /-- Support for induction principles whose IH is guarded by `List.Forall₂`, e.g.
     arising from mutual inductive types relating two lists element-wise. -/

From eab9ccf4d4870008a06e415385dd9d99cce96f36 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 21:46:29 +0200
Subject: [PATCH 28/54] Finish proof for intoIH_listForall2

---
 Iris/Iris/ProofMode/Instances.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index e6090b814..5e309e3d8 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -974,4 +974,13 @@ instance intoIH_listForall₂ [BI PROP] (φ : α → β → Prop) (l1 : List α)
     (P : PROP) (Φ : α → β → PROP)
     [h : ∀ x1 x2, IntoIH (φ x1 x2) P (Φ x1 x2)] :
     IntoIH (List.Forall₂ φ l1 l2) P (bigSepL2 (fun _ x1 x2 => iprop(□ Φ x1 x2)) l1 l2) where
-  into_ih := sorry
+  into_ih := by
+    intro h
+    induction h with
+    | nil => simp [bigSepL2, affine]
+    | cons x xs ih =>
+      simp [bigSepL2] at ⊢
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro' ((h _ _).into_ih x)
+      · exact ih

From b6b03a10f4c03803caffd5572ef977bf887c19da Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 22:36:06 +0200
Subject: [PATCH 29/54] Code refactoring and comments

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 108 +++++++++++++--------
 1 file changed, 66 insertions(+), 42 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 6e0bcfd4d..f57c02677 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -17,6 +17,37 @@ namespace Iris.ProofMode
 public meta section
 open BI Std Lean Elab Tactic Meta Qq
 
+/--
+  The `iinduction` tactic user provides the proof for the induction subgoal,
+  which has hypotheses introduced into the Iris proof state.
+
+  Given this proof, obtain the proof where the hypotheses are not yet
+  introduced into the Iris proof state.
+-/
+@[rocq_alias tac_revert_ih]
+theorem revert_IH [BI PROP] {P Q goal : PROP} {φ}
+    (ih : φ)
+    (inst : IntoIH φ P Q)
+    (h1 : P ⊢ □ P)
+    (h2 : P ∗ □ Q ⊢ goal) : P ⊢ goal := calc
+  P ⊢ □ P         := h1
+  _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
+  _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
+  _ ⊢ P ∗ □ Q     := sep_mono_l intuitionistically_elim
+  _ ⊢ goal        := h2
+
+/--
+  Given two intuitionistic propositions, their combined proposition
+  remains intuitionistic.
+-/
+theorem combine_intuitionistic_props [BI PROP] {P Q : PROP}
+    (h1 : P ⊢ □ P) :
+    P ∗ □ Q ⊢ □ (P ∗ □ Q) := calc
+  _ ⊢ □ P ∗ □ Q   := sep_mono_l h1
+  _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
+
 /--
   Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
   the subset of intuitionistic hypotheses in `hyps` that contains the `fvar`
@@ -58,33 +89,6 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
         ihs := decl.fvarId :: ihs
     return ihs.reverse
 
-/--
-  The `iinduction` tactic user provides the proof for the induction subgoal,
-  which has hypotheses introduced into the Iris proof state.
-
-  Given this proof, obtain the proof where the hypotheses are not yet
-  introduced into the Iris proof state.
--/
-@[rocq_alias tac_revert_ih]
-theorem revert_IH [BI PROP] {P Q goal : PROP} {φ}
-    (ih : φ)
-    (inst : IntoIH φ P Q)
-    (h1 : P ⊢ □ P)
-    (h2 : P ∗ □ Q ⊢ goal) : P ⊢ goal := calc
-  P ⊢ □ P         := h1
-  _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
-  _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
-  _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
-  _ ⊢ P ∗ □ Q     := sep_mono_l intuitionistically_elim
-  _ ⊢ goal        := h2
-
-theorem stay_intuitionistic [BI PROP] {P Q : PROP}
-    (h1 : P ⊢ □ P) :
-    P ∗ □ Q ⊢ □ (P ∗ □ Q) := calc
-  _ ⊢ □ P ∗ □ Q   := sep_mono_l h1
-  _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
-  _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
-
 /--
   Designed to be a mutable state such that `newHyps` contains induction
   hypotheses generated by Lean's built-in induction.
@@ -94,7 +98,7 @@ private structure InductionState {u} {prop : Q(Type u)} {bi} (origE goal : Q($pr
   {newE : Q($prop)}
   (newHyps : Hyps bi newE)
   -- Proof that the hypotheses is intuitionsitic
-  (pfAux : Q($newE ⊢ □ $newE))
+  (pfIntHyps : Q($newE ⊢ □ $newE))
   (pf : Q(($newE ⊢ $goal) → $origE ⊢ $goal))
 
 /--
@@ -113,37 +117,34 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
   let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $oldE $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
 
+  -- Introduce the induction hypothesis into the intuitionistic context
   let nameIdent := mkIdent <| ← hFVar.getUserName
   let binderIdent ← `(binderIdent| $nameIdent:ident)
   let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
 
-  let a := q(revert_IH $p $inst (goal := $goal) $st.pfAux)
+  let a := q(revert_IH $p $inst (goal := $goal) $st.pfIntHyps)
 
   return {
     newHyps,
     pf := q(fun pf => $st.pf <| $a pf),
-    pfAux := q(stay_intuitionistic $st.pfAux)
+    pfIntHyps := q(combine_intuitionistic_props $st.pfIntHyps)
   }
 
-/--
-  This should be true in `addAllIHs` because all spatial hypotheses have
-  been reverted, so the Iris proof state contains no hypothesis in the
-  spatial context. -/
-theorem dummy [BI PROP] {e : PROP} : e ⊢ □ e := sorry
-
 /--
   Introduce a list of induction hypotheses into Iris proof state.
   The list of `FVarId` values (`ihFVars`) should be the list returned by
   `findIHs`.
 -/
 private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal : Q($prop)}
-    (hyps : Hyps bi e) (ihFVars : List FVarId) :
+    (pfIntHyps : Q($e ⊢ □ $e)) (hyps : Hyps bi e) (ihFVars : List FVarId) :
     ProofModeM (@InductionState u prop bi e goal) := do
 
+  -- Initialise the mutable instance of `InductionState`
   let mut st : InductionState e goal := {
-    newHyps := hyps, pf := q(id), pfAux := q(dummy)
+    newHyps := hyps, pf := q(id), pfIntHyps
   }
 
+  -- Iteratively move the induction hypotheses into the intuitionistic context
   for i in ihFVars do
     let p := mkFVar i
     let φ ← inferType (mkFVar i)
@@ -151,6 +152,26 @@ private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal : Q($pro
 
   return st
 
+/--
+  Given hypothesis `hyps` representing `e` where every hypothesis exist in the
+  intuitionistic context, `e ⊢ □ e` must hold.
+-/
+private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : ProofModeM Q($e ⊢ □ $e) :=
+  match hyps with
+  | .emp _ =>
+    pure q(intuitionistically_emp.mpr)
+  | .hyp _ _ _ p _ _ =>
+    match matchBool p with
+    | .inl _ =>
+      pure q(intuitionistically_idem.mpr)
+    | .inr _ =>
+      throwError "iinduction: spatial context is not empty after reverting hypotheses"
+  | .sep _ _ _ _ lhs rhs => do
+    let pfL ← buildPfIntHyps lhs
+    let pfR ← buildPfIntHyps rhs
+    pure q((sep_mono $pfL $pfR).trans intuitionistically_sep_2)
+
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -168,6 +189,7 @@ elab "iinduction" colGt x:ident : tactic => do
       | _ => throwError "iinduction: {indName} is not inductive"
     | _ => throwError "iinduction: unable to determine inductive type"
 
+    -- TODO: generalisation for other inductive data structures
     let varNames : Array AltVarNames := #[
         { explicit := true, varNames := [] },
         { explicit := true, varNames := [x.getId, `IH] }
@@ -184,7 +206,7 @@ elab "iinduction" colGt x:ident : tactic => do
         let subgoals ←  m.mvarId!.withContext do
           m.mvarId!.induction fvar recName varNames
 
-        -- Handle each subgoal
+        -- Handle each subgoal generated by Lean's induction
         for s in subgoals do
           s.mvarId.withContext do
             let sType ← instantiateMVars (← s.mvarId.getType)
@@ -196,12 +218,14 @@ elab "iinduction" colGt x:ident : tactic => do
             -- Find the induction hypotheses generated by Lean's `induction` tactic
             let ihFVars ← findIHs s.mvarId
 
+            -- A proof that all hypotheses in the Iris goal exist in the intuitionistic context
+            let pfIntHyps ← buildPfIntHyps irisGoal.hyps
+
             -- Introduce the induction hypothesis back into the Iris proof state
-            let st ← addAllIHs irisGoal.hyps ihFVars (goal := irisGoal.goal)
+            let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars (goal := irisGoal.goal)
 
+            -- Remove the induction hypotheses from the regular Lean context
             let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
-
-            -- Remove the IHs from the regular context
             s.mvarId.assign <| q($st.pf $pf')
 
         return m

From 783ad437e2d42012ee0179d18cb707b7ed18659b Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sat, 30 May 2026 22:42:47 +0200
Subject: [PATCH 30/54] Remove goal from InductionState, simplifications

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 33 ++++++++++------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index f57c02677..0104acb5a 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -25,17 +25,16 @@ open BI Std Lean Elab Tactic Meta Qq
   introduced into the Iris proof state.
 -/
 @[rocq_alias tac_revert_ih]
-theorem revert_IH [BI PROP] {P Q goal : PROP} {φ}
+theorem revert_IH [BI PROP] {P Q : PROP} {φ}
     (ih : φ)
     (inst : IntoIH φ P Q)
-    (h1 : P ⊢ □ P)
-    (h2 : P ∗ □ Q ⊢ goal) : P ⊢ goal := calc
+    (h1 : P ⊢ □ P) :
+    P ⊢ P ∗ □ Q := calc
   P ⊢ □ P         := h1
   _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
   _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
   _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
   _ ⊢ P ∗ □ Q     := sep_mono_l intuitionistically_elim
-  _ ⊢ goal        := h2
 
 /--
   Given two intuitionistic propositions, their combined proposition
@@ -93,23 +92,23 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
   Designed to be a mutable state such that `newHyps` contains induction
   hypotheses generated by Lean's built-in induction.
 -/
-private structure InductionState {u} {prop : Q(Type u)} {bi} (origE goal : Q($prop)) where
+private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop)) where
   -- Hypotheses in the latest Iris proof goal
   {newE : Q($prop)}
   (newHyps : Hyps bi newE)
   -- Proof that the hypotheses is intuitionsitic
   (pfIntHyps : Q($newE ⊢ □ $newE))
-  (pf : Q(($newE ⊢ $goal) → $origE ⊢ $goal))
+  (pf : Q($origE  ⊢ $newE))
 
 /--
   Used for every induction hypothesis generated by Lean upon using the built-in
   `induction` tactic. The type class `IntoIH` is used for obtaining the
   corresponding proposition in the Iris proof mode.
 -/
-private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
-    (st : @InductionState u prop bi e goal)
+private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (st : @InductionState u prop bi e)
     (φ : Q(Prop)) (p : Q($φ)) (hFVar : FVarId) :
-    ProofModeM (@InductionState u prop bi e goal) := do
+    ProofModeM (@InductionState u prop bi e) := do
   let oldE := st.newE
   let oldHyps : Hyps bi oldE := st.newHyps
 
@@ -122,11 +121,9 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
   let binderIdent ← `(binderIdent| $nameIdent:ident)
   let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
 
-  let a := q(revert_IH $p $inst (goal := $goal) $st.pfIntHyps)
-
   return {
     newHyps,
-    pf := q(fun pf => $st.pf <| $a pf),
+    pf := q($(st.pf).trans <| revert_IH $p $inst $st.pfIntHyps),
     pfIntHyps := q(combine_intuitionistic_props $st.pfIntHyps)
   }
 
@@ -135,13 +132,13 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal}
   The list of `FVarId` values (`ihFVars`) should be the list returned by
   `findIHs`.
 -/
-private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e goal : Q($prop)}
+private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
     (pfIntHyps : Q($e ⊢ □ $e)) (hyps : Hyps bi e) (ihFVars : List FVarId) :
-    ProofModeM (@InductionState u prop bi e goal) := do
+    ProofModeM (@InductionState u prop bi e) := do
 
   -- Initialise the mutable instance of `InductionState`
-  let mut st : InductionState e goal := {
-    newHyps := hyps, pf := q(id), pfIntHyps
+  let mut st : InductionState e := {
+    newHyps := hyps, pf := q(.rfl), pfIntHyps
   }
 
   -- Iteratively move the induction hypotheses into the intuitionistic context
@@ -222,11 +219,11 @@ elab "iinduction" colGt x:ident : tactic => do
             let pfIntHyps ← buildPfIntHyps irisGoal.hyps
 
             -- Introduce the induction hypothesis back into the Iris proof state
-            let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars (goal := irisGoal.goal)
+            let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars
 
             -- Remove the induction hypotheses from the regular Lean context
             let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
-            s.mvarId.assign <| q($st.pf $pf')
+            s.mvarId.assign <| q($(st.pf).trans $pf')
 
         return m
     )

From 31e5633ac1d768f7ede237ad6ef0802596ed6707 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 14:31:27 +0200
Subject: [PATCH 31/54] Add test for iinduction

---
 Iris/Iris/Tests/Tactics.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 4d26742e9..f721334e1 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2718,14 +2718,8 @@ end iloeb
 
 section iinduction
 
-example [BI PROP] {P Q : PROP} {n : Nat} :
-    ⊢ P -∗ ⌜n = 0⌝ -∗ Q -∗ ⌜n ≠ 1⌝ -∗ P ∗ Q ∗ ⌜n = n⌝ := by
-  iintro H1 H2 H3 #H4
-  iinduction n
-  · iframe
-  · iframe
-    itrivial
-
+/-- Tests `iinduction` with induction on natural numbers. Hypotheses in the
+    spatial context become premises of the induction hypothesis. -/
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
@@ -2734,4 +2728,10 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   · iframe
     itrivial
 
+/- Tests `iinduction` with a non-inductive datatype -/
+/-- error: iinduction: unable to determine inductive type -/
+#guard_msgs in
+example [BI PROP] {P : PROP} : ⊢ P := by
+  iinduction P
+
 end iinduction

From bfd3e59b90655828f5fd486e79ac62d9ce6f7b2c Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 15:00:14 +0200
Subject: [PATCH 32/54] Obtain constructor names from inductInfo: towards
 allowing user-given variable and IH names

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 0104acb5a..4878cb04b 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -179,10 +179,10 @@ elab "iinduction" colGt x:ident : tactic => do
 
     -- Find the recursor name for induction
     let fvarType ← whnf <| ← inferType <| mkFVar fvar
-    let recName : Name ← match fvarType.getAppFn with
+    let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
     | .const indName _ =>
       match (← getEnv).find? indName with
-      | some (.inductInfo val) => pure <| Name.mkStr val.name "recOn"
+      | some (.inductInfo val) => pure <| (Name.mkStr val.name "recOn", val.ctors)
       | _ => throwError "iinduction: {indName} is not inductive"
     | _ => throwError "iinduction: unable to determine inductive type"
 

From e5c7a22823df5f23e4a0dac5b56838ce5edbde31 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 15:33:26 +0200
Subject: [PATCH 33/54] Towards implementing the `with` syntax

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 60 +++++++++++++++++++---
 Iris/Iris/Tests/Tactics.lean               | 19 +++++++
 2 files changed, 73 insertions(+), 6 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 4878cb04b..b44df8796 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -169,10 +169,33 @@ private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     let pfR ← buildPfIntHyps rhs
     pure q((sep_mono $pfL $pfR).trans intuitionistically_sep_2)
 
-elab "iinduction" colGt x:ident : tactic => do
+-- One case upon applying the `iinduction` tactic
+syntax iinductionAlt := "| " ident ident* " => " tacticSeq
+
+private def parseIInductionAlt (alt : TSyntax `Iris.ProofMode.iinductionAlt) :
+    TacticM (Name × Array Name × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
+  let `(iinductionAlt| | $ctor:ident $vars:ident* => $tac:tacticSeq) := alt
+  | throwError "iinduction: invalid syntax"
+
+  return (ctor.getId, vars.map (·.getId), tac)
+
+/-- Check whether a fully-qualified constructor name (e.g. `Nat.succ`) matches a
+    user-written short name (e.g. `succ`) or an already-qualified name. -/
+private def matchesCtorName (fullName : Name) (userShort : Name) : Bool :=
+  fullName == userShort || fullName.getString! == userShort.getString!
+
+
+private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
+  throwError "iinduction: case '{ctor.getString!}' is not handled"
+
+
+elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
+  -- Parse the list of cases supplied by the user
+  let parsedAlts ← alts.mapM parseIInductionAlt
+
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     -- Find all hypotheses that contain the variable being performed induction on
     let targets := iHypsContaining hyps fvar
@@ -187,10 +210,14 @@ elab "iinduction" colGt x:ident : tactic => do
     | _ => throwError "iinduction: unable to determine inductive type"
 
     -- TODO: generalisation for other inductive data structures
-    let varNames : Array AltVarNames := #[
-        { explicit := true, varNames := [] },
-        { explicit := true, varNames := [x.getId, `IH] }
-      ]
+    let varNames : Array AltVarNames ← if parsedAlts.isEmpty then
+      pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
+    else do
+      ctors.toArray.mapM fun ctor =>
+      match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+      | some (_, varNms, _) =>
+        pure ({ explicit := true, varNames := varNms.toList } : AltVarNames)
+      | none => throwMissingAlt ctor
 
     -- Revert all hypotheses in the list
     let pf ← iRevertIntro hyps goal targets (
@@ -204,7 +231,10 @@ elab "iinduction" colGt x:ident : tactic => do
           m.mvarId!.induction fvar recName varNames
 
         -- Handle each subgoal generated by Lean's induction
-        for s in subgoals do
+        for (s, ctor) in subgoals.toList.zip ctors do
+          if subgoals.size != ctors.length then
+            throwError "iinduction: expected {ctors.length} subgoals for {ctors.length} constructors, got {subgoals.size}"
+
           s.mvarId.withContext do
             let sType ← instantiateMVars (← s.mvarId.getType)
 
@@ -223,8 +253,26 @@ elab "iinduction" colGt x:ident : tactic => do
 
             -- Remove the induction hypotheses from the regular Lean context
             let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
+
             s.mvarId.assign <| q($(st.pf).trans $pf')
 
+            -- Case applicable for `with` syntax only
+            if !parsedAlts.isEmpty then
+              let biGoalMVar := (← getThe ProofModeM.State).goals.back!
+              modify (fun s => { s with goals := s.goals.pop })
+
+              let some (_, _, userTac) :=
+              parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor)
+              | throwMissingAlt ctor
+
+              -- Run the user tactic on the BI goal
+              let savedGoals ← getGoals
+              setGoals [biGoalMVar]
+              evalTactic userTac
+              let remaining ← getGoals
+              setGoals savedGoals
+              for r in remaining do addMVarGoal r
+
         return m
     )
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index f721334e1..aebe1462a 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2728,10 +2728,29 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   · iframe
     itrivial
 
+/-- Tests `iinduction` with induction on natural numbers with user-supplied
+    names for variables and induction hypotheses. -/
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n
+  | zero      => itrivial
+  | succ n IH => iframe; itrivial
+  | aa => sorry
+
 /- Tests `iinduction` with a non-inductive datatype -/
 /-- error: iinduction: unable to determine inductive type -/
 #guard_msgs in
 example [BI PROP] {P : PROP} : ⊢ P := by
   iinduction P
 
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  induction n with
+  | zero => sorry
+  | succ aa bb => sorry
+
+
+
 end iinduction

From 7d1cb7c168f3c950bc4cfe1ed2b310119ba66d02 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 16:11:25 +0200
Subject: [PATCH 34/54] Pretty variables for cases in the `with` syntax

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 26 +++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index b44df8796..59561174a 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -173,11 +173,11 @@ private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 syntax iinductionAlt := "| " ident ident* " => " tacticSeq
 
 private def parseIInductionAlt (alt : TSyntax `Iris.ProofMode.iinductionAlt) :
-    TacticM (Name × Array Name × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
+    TacticM (Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
   let `(iinductionAlt| | $ctor:ident $vars:ident* => $tac:tacticSeq) := alt
   | throwError "iinduction: invalid syntax"
 
-  return (ctor.getId, vars.map (·.getId), tac)
+  return (ctor.getId, vars, tac)
 
 /-- Check whether a fully-qualified constructor name (e.g. `Nat.succ`) matches a
     user-written short name (e.g. `succ`) or an already-qualified name. -/
@@ -210,13 +210,14 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
     | _ => throwError "iinduction: unable to determine inductive type"
 
     -- TODO: generalisation for other inductive data structures
-    let varNames : Array AltVarNames ← if parsedAlts.isEmpty then
+    let varNames : Array AltVarNames ←
+    if parsedAlts.isEmpty then
       pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
     else do
       ctors.toArray.mapM fun ctor =>
       match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
-      | some (_, varNms, _) =>
-        pure ({ explicit := true, varNames := varNms.toList } : AltVarNames)
+      | some (_, vars, _) =>
+        pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
       | none => throwMissingAlt ctor
 
     -- Revert all hypotheses in the list
@@ -236,6 +237,21 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
             throwError "iinduction: expected {ctors.length} subgoals for {ctors.length} constructors, got {subgoals.size}"
 
           s.mvarId.withContext do
+
+            if !parsedAlts.isEmpty then
+
+
+              match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+              | some (_, vars, _) =>
+                for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
+                let lctx ← getLCtx
+                let fieldType ← inferType fieldFVar
+                addLocalVarInfo varStx lctx fieldFVar (some fieldType) (isBinder := true)
+
+              | none => throwMissingAlt ctor
+
+
+
             let sType ← instantiateMVars (← s.mvarId.getType)
 
             let some irisGoal := parseIrisGoal? sType

From b826e7f21a37e46871a1d52ac977b407d0f57044 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 17:20:01 +0200
Subject: [PATCH 35/54] Check for invalid alternative names and throw pretty
 error

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 25 +++++++++++----------
 Iris/Iris/Tests/Tactics.lean               | 26 ++++++++++++++++------
 2 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 59561174a..60bb0e710 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -184,10 +184,17 @@ private def parseIInductionAlt (alt : TSyntax `Iris.ProofMode.iinductionAlt) :
 private def matchesCtorName (fullName : Name) (userShort : Name) : Bool :=
   fullName == userShort || fullName.getString! == userShort.getString!
 
-
 private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
-  throwError "iinduction: case '{ctor.getString!}' is not handled"
+  throwError "iinduction: alternative `{ctor.getString!}` has not been provided"
+
+private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
+  let invalidAltCtors :=
+    altCtors.filter fun alt =>
+      not <| ctors.any fun ctor => matchesCtorName ctor alt
 
+  if !invalidAltCtors.isEmpty then
+    let invalids := String.intercalate ", " <| invalidAltCtors.map (s!"`{·}`")
+    throwError m!"iinduction: invalid alternative names {invalids}"
 
 elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
@@ -209,7 +216,7 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
       | _ => throwError "iinduction: {indName} is not inductive"
     | _ => throwError "iinduction: unable to determine inductive type"
 
-    -- TODO: generalisation for other inductive data structures
+    -- Define the names for variables and induction hypotheses if supplied by user
     let varNames : Array AltVarNames ←
     if parsedAlts.isEmpty then
       pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
@@ -231,27 +238,21 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
         let subgoals ←  m.mvarId!.withContext do
           m.mvarId!.induction fvar recName varNames
 
+        if !parsedAlts.isEmpty then
+          checkCtors ctors <| parsedAlts.toList.map (fun a => match a with | (aa, _, _) => aa)
+
         -- Handle each subgoal generated by Lean's induction
         for (s, ctor) in subgoals.toList.zip ctors do
-          if subgoals.size != ctors.length then
-            throwError "iinduction: expected {ctors.length} subgoals for {ctors.length} constructors, got {subgoals.size}"
-
           s.mvarId.withContext do
-
             if !parsedAlts.isEmpty then
-
-
               match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
               | some (_, vars, _) =>
                 for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
                 let lctx ← getLCtx
                 let fieldType ← inferType fieldFVar
                 addLocalVarInfo varStx lctx fieldFVar (some fieldType) (isBinder := true)
-
               | none => throwMissingAlt ctor
 
-
-
             let sType ← instantiateMVars (← s.mvarId.getType)
 
             let some irisGoal := parseIrisGoal? sType
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index aebe1462a..b92cd4b1d 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2734,9 +2734,8 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
   iinduction n
-  | zero      => itrivial
-  | succ n IH => iframe; itrivial
-  | aa => sorry
+  | Nat.zero  => itrivial          -- Using the full name of the constructor
+  | succ n IH => iframe; itrivial  -- Using the short name of the constructor
 
 /- Tests `iinduction` with a non-inductive datatype -/
 /-- error: iinduction: unable to determine inductive type -/
@@ -2744,13 +2743,26 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
 example [BI PROP] {P : PROP} : ⊢ P := by
   iinduction P
 
+/- Tests `iinduction` with induction on natural numbers with user-supplied
+    names, missing `succ` case -/
+/-- error: iinduction: alternative `succ` has not been provided -/
+#guard_msgs in
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  induction n with
-  | zero => sorry
-  | succ aa bb => sorry
-
+  iinduction n
+  | zero => itrivial
 
+/- Tests `iinduction` with induction on natural numbers with user-supplied
+    names, missing `succ` case -/
+/-- error: iinduction: invalid alternative names `a` -/
+#guard_msgs in
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n
+  | zero      => itrivial
+  | a         => itrivial
+  | succ n IH => iframe; itrivial
 
 end iinduction

From 43b82159c57b221c53ae3b26047b1bd0fac42dc2 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 17:24:46 +0200
Subject: [PATCH 36/54] Move most of elaboration code into iInductionCore for
 reusability

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 185 +++++++++++----------
 1 file changed, 96 insertions(+), 89 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 60bb0e710..d86603358 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -196,6 +196,101 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
     let invalids := String.intercalate ", " <| invalidAltCtors.map (s!"`{·}`")
     throwError m!"iinduction: invalid alternative names {invalids}"
 
+private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
+    (parsedAlts : Array (Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)) :
+    ProofModeM Q($e ⊢ $goal) := do
+  -- Find all hypotheses that contain the variable being performed induction on
+  let targets := iHypsContaining hyps fvar
+
+  -- Find the recursor name for induction
+  let fvarType ← whnf <| ← inferType <| mkFVar fvar
+  let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
+  | .const indName _ =>
+    match (← getEnv).find? indName with
+    | some (.inductInfo val) => pure <| (Name.mkStr val.name "recOn", val.ctors)
+    | _ => throwError "iinduction: {indName} is not inductive"
+  | _ => throwError "iinduction: unable to determine inductive type"
+
+  -- Define the names for variables and induction hypotheses if supplied by user
+  let varNames : Array AltVarNames ←
+  if parsedAlts.isEmpty then
+    pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
+  else do
+    ctors.toArray.mapM fun ctor =>
+    match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+    | some (_, vars, _) =>
+      pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
+    | none => throwMissingAlt ctor
+
+  -- Revert all hypotheses in the list
+  let pf ← iRevertIntro hyps goal targets (
+    -- The function takes the hypotheses and goal after reverting
+    fun hyps' goal' k => do
+      -- Create a new metavariable for the proof goal upon reverting hypotheses
+      let m ← mkBIGoal hyps' goal'
+
+      -- Use built-in induction in Lean to generate the subgoals for induction
+      let subgoals ←  m.mvarId!.withContext do
+        m.mvarId!.induction fvar recName varNames
+
+      if !parsedAlts.isEmpty then
+        checkCtors ctors <| parsedAlts.toList.map (fun a => match a with | (aa, _, _) => aa)
+
+      -- Handle each subgoal generated by Lean's induction
+      for (s, ctor) in subgoals.toList.zip ctors do
+        s.mvarId.withContext do
+          if !parsedAlts.isEmpty then
+            match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+            | some (_, vars, _) =>
+              for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
+              let lctx ← getLCtx
+              let fieldType ← inferType fieldFVar
+              addLocalVarInfo varStx lctx fieldFVar (some fieldType) (isBinder := true)
+            | none => throwMissingAlt ctor
+
+          let sType ← instantiateMVars (← s.mvarId.getType)
+
+          let some irisGoal := parseIrisGoal? sType
+          -- This should not happen
+          | throwError "iinduction: fail to parse induction subgoal"
+
+          -- Find the induction hypotheses generated by Lean's `induction` tactic
+          let ihFVars ← findIHs s.mvarId
+
+          -- A proof that all hypotheses in the Iris goal exist in the intuitionistic context
+          let pfIntHyps ← buildPfIntHyps irisGoal.hyps
+
+          -- Introduce the induction hypothesis back into the Iris proof state
+          let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars
+
+          -- Remove the induction hypotheses from the regular Lean context
+          let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
+
+          s.mvarId.assign <| q($(st.pf).trans $pf')
+
+          -- Case applicable for `with` syntax only
+          if !parsedAlts.isEmpty then
+            let biGoalMVar := (← getThe ProofModeM.State).goals.back!
+            modify (fun s => { s with goals := s.goals.pop })
+
+            let some (_, _, userTac) :=
+            parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor)
+            | throwMissingAlt ctor
+
+            -- Run the user tactic on the BI goal
+            let savedGoals ← getGoals
+            setGoals [biGoalMVar]
+            evalTactic userTac
+            let remaining ← getGoals
+            setGoals savedGoals
+            for r in remaining do addMVarGoal r
+
+      return m
+  )
+
+  return pf
+
 elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -204,93 +299,5 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
   let parsedAlts ← alts.mapM parseIInductionAlt
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    -- Find all hypotheses that contain the variable being performed induction on
-    let targets := iHypsContaining hyps fvar
-
-    -- Find the recursor name for induction
-    let fvarType ← whnf <| ← inferType <| mkFVar fvar
-    let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
-    | .const indName _ =>
-      match (← getEnv).find? indName with
-      | some (.inductInfo val) => pure <| (Name.mkStr val.name "recOn", val.ctors)
-      | _ => throwError "iinduction: {indName} is not inductive"
-    | _ => throwError "iinduction: unable to determine inductive type"
-
-    -- Define the names for variables and induction hypotheses if supplied by user
-    let varNames : Array AltVarNames ←
-    if parsedAlts.isEmpty then
-      pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
-    else do
-      ctors.toArray.mapM fun ctor =>
-      match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
-      | some (_, vars, _) =>
-        pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
-      | none => throwMissingAlt ctor
-
-    -- Revert all hypotheses in the list
-    let pf ← iRevertIntro hyps goal targets (
-      -- The function takes the hypotheses and goal after reverting
-      fun hyps' goal' k => do
-        -- Create a new metavariable for the proof goal upon reverting hypotheses
-        let m ← mkBIGoal hyps' goal'
-
-        -- Use built-in induction in Lean to generate the subgoals for induction
-        let subgoals ←  m.mvarId!.withContext do
-          m.mvarId!.induction fvar recName varNames
-
-        if !parsedAlts.isEmpty then
-          checkCtors ctors <| parsedAlts.toList.map (fun a => match a with | (aa, _, _) => aa)
-
-        -- Handle each subgoal generated by Lean's induction
-        for (s, ctor) in subgoals.toList.zip ctors do
-          s.mvarId.withContext do
-            if !parsedAlts.isEmpty then
-              match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
-              | some (_, vars, _) =>
-                for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
-                let lctx ← getLCtx
-                let fieldType ← inferType fieldFVar
-                addLocalVarInfo varStx lctx fieldFVar (some fieldType) (isBinder := true)
-              | none => throwMissingAlt ctor
-
-            let sType ← instantiateMVars (← s.mvarId.getType)
-
-            let some irisGoal := parseIrisGoal? sType
-            -- This should not happen
-            | throwError "iinduction: fail to parse induction subgoal"
-
-            -- Find the induction hypotheses generated by Lean's `induction` tactic
-            let ihFVars ← findIHs s.mvarId
-
-            -- A proof that all hypotheses in the Iris goal exist in the intuitionistic context
-            let pfIntHyps ← buildPfIntHyps irisGoal.hyps
-
-            -- Introduce the induction hypothesis back into the Iris proof state
-            let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars
-
-            -- Remove the induction hypotheses from the regular Lean context
-            let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
-
-            s.mvarId.assign <| q($(st.pf).trans $pf')
-
-            -- Case applicable for `with` syntax only
-            if !parsedAlts.isEmpty then
-              let biGoalMVar := (← getThe ProofModeM.State).goals.back!
-              modify (fun s => { s with goals := s.goals.pop })
-
-              let some (_, _, userTac) :=
-              parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor)
-              | throwMissingAlt ctor
-
-              -- Run the user tactic on the BI goal
-              let savedGoals ← getGoals
-              setGoals [biGoalMVar]
-              evalTactic userTac
-              let remaining ← getGoals
-              setGoals savedGoals
-              for r in remaining do addMVarGoal r
-
-        return m
-    )
-
+    let pf ← iInductionCore hyps goal fvar parsedAlts
     mvar.assign pf

From 48945d99755fa07bb4d1bb2f4bdba443f53b1b40 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 17:32:39 +0200
Subject: [PATCH 37/54] iInductionCore: alternative names being optional, use
 pattern matching

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 44 ++++++++++++++--------
 Iris/Iris/Tests/Tactics.lean               |  6 +--
 2 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index d86603358..726894aea 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -198,7 +198,7 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
-    (parsedAlts : Array (Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)) :
+    (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) :
     ProofModeM Q($e ⊢ $goal) := do
   -- Find all hypotheses that contain the variable being performed induction on
   let targets := iHypsContaining hyps fvar
@@ -214,14 +214,15 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   -- Define the names for variables and induction hypotheses if supplied by user
   let varNames : Array AltVarNames ←
-  if parsedAlts.isEmpty then
-    pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
-  else do
-    ctors.toArray.mapM fun ctor =>
-    match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
-    | some (_, vars, _) =>
-      pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
-    | none => throwMissingAlt ctor
+    match parsedAlts with
+    | none =>
+      pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
+    | some parsedAlts => do
+      ctors.toArray.mapM fun ctor =>
+      match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+      | some (_, vars, _) =>
+        pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
+      | none => throwMissingAlt ctor
 
   -- Revert all hypotheses in the list
   let pf ← iRevertIntro hyps goal targets (
@@ -234,13 +235,16 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
       let subgoals ←  m.mvarId!.withContext do
         m.mvarId!.induction fvar recName varNames
 
-      if !parsedAlts.isEmpty then
-        checkCtors ctors <| parsedAlts.toList.map (fun a => match a with | (aa, _, _) => aa)
+      match parsedAlts with
+      | none => pure ()
+      | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
 
       -- Handle each subgoal generated by Lean's induction
       for (s, ctor) in subgoals.toList.zip ctors do
         s.mvarId.withContext do
-          if !parsedAlts.isEmpty then
+          match parsedAlts with
+          | none => pure ()
+          | some parsedAlts =>
             match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
             | some (_, vars, _) =>
               for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
@@ -270,7 +274,9 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           s.mvarId.assign <| q($(st.pf).trans $pf')
 
           -- Case applicable for `with` syntax only
-          if !parsedAlts.isEmpty then
+          match parsedAlts with
+          | none => pure ()
+          | some parsedAlts =>
             let biGoalMVar := (← getThe ProofModeM.State).goals.back!
             modify (fun s => { s with goals := s.goals.pop })
 
@@ -291,7 +297,15 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return pf
 
-elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
+elab "iinduction" colGt x:ident : tactic => do
+  -- Get the ID of the variable on which induction is being performed
+  let fvar ← getFVarId x
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none
+    mvar.assign pf
+
+elab "iinduction" colGt x:ident "with" alts:(colGe iinductionAlt)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
@@ -299,5 +313,5 @@ elab "iinduction" colGt x:ident alts:(colGe iinductionAlt)* : tactic => do
   let parsedAlts ← alts.mapM parseIInductionAlt
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar parsedAlts
+    let pf ← iInductionCore hyps goal fvar (some parsedAlts)
     mvar.assign pf
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index b92cd4b1d..d812dd79e 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2733,7 +2733,7 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n
+  iinduction n with
   | Nat.zero  => itrivial          -- Using the full name of the constructor
   | succ n IH => iframe; itrivial  -- Using the short name of the constructor
 
@@ -2750,7 +2750,7 @@ example [BI PROP] {P : PROP} : ⊢ P := by
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n
+  iinduction n with
   | zero => itrivial
 
 /- Tests `iinduction` with induction on natural numbers with user-supplied
@@ -2760,7 +2760,7 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n
+  iinduction n with
   | zero      => itrivial
   | a         => itrivial
   | succ n IH => iframe; itrivial

From 7378f8d249746628890900634c8d3b66fbbfd1ee Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 17:42:21 +0200
Subject: [PATCH 38/54] Code refactoring

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 47 ++++++++++++++--------
 1 file changed, 30 insertions(+), 17 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 726894aea..33cb85475 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -18,11 +18,17 @@ public meta section
 open BI Std Lean Elab Tactic Meta Qq
 
 /--
-  The `iinduction` tactic user provides the proof for the induction subgoal,
-  which has hypotheses introduced into the Iris proof state.
+  The user of the `iinduction` tactic provides the proof for the induction
+  subgoal. Induction hypotheses are available for the user in the intuitionistic
+  context of the Iris proof state.
 
-  Given this proof, obtain the proof where the hypotheses are not yet
-  introduced into the Iris proof state.
+  Meanwhile, the actual induction subgoal generated by Lean with the `induction`
+  tactic has induction hypotheses in the regular context.
+
+  Given all hypotheses in the Iris proof state (represented by `P`) exist in
+  the intuitionistic context (that is, the spatial context is empty), we can
+  introduce another induction hypothesis generated by Lean into the
+  intuitionistic context.
 -/
 @[rocq_alias tac_revert_ih]
 theorem revert_IH [BI PROP] {P Q : PROP} {φ}
@@ -47,6 +53,18 @@ theorem combine_intuitionistic_props [BI PROP] {P Q : PROP}
   _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
   _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
 
+/--
+  Designed to be a mutable state such that `newHyps` contains induction
+  hypotheses generated by Lean's built-in induction.
+-/
+private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop)) where
+  -- Hypotheses in the Iris proof goal
+  {newE : Q($prop)}
+  (newHyps : Hyps bi newE)
+  -- Proof that the hypotheses is intuitionsitic
+  (pfIntHyps : Q($newE ⊢ □ $newE))
+  (pf : Q($origE ⊢ $newE))
+
 /--
   Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
   the subset of intuitionistic hypotheses in `hyps` that contains the `fvar`
@@ -88,18 +106,6 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
         ihs := decl.fvarId :: ihs
     return ihs.reverse
 
-/--
-  Designed to be a mutable state such that `newHyps` contains induction
-  hypotheses generated by Lean's built-in induction.
--/
-private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop)) where
-  -- Hypotheses in the latest Iris proof goal
-  {newE : Q($prop)}
-  (newHyps : Hyps bi newE)
-  -- Proof that the hypotheses is intuitionsitic
-  (pfIntHyps : Q($newE ⊢ □ $newE))
-  (pf : Q($origE  ⊢ $newE))
-
 /--
   Used for every induction hypothesis generated by Lean upon using the built-in
   `induction` tactic. The type class `IntoIH` is used for obtaining the
@@ -297,6 +303,10 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return pf
 
+/--
+  Simple tactic with inaccessible names of variables and induction hypotheses
+  generated by Lean automatically.
+-/
 elab "iinduction" colGt x:ident : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
@@ -305,11 +315,14 @@ elab "iinduction" colGt x:ident : tactic => do
     let pf ← iInductionCore hyps goal fvar none
     mvar.assign pf
 
+/--
+  Tactic with names of variables and induction hypotheses supplied by the user.
+-/
 elab "iinduction" colGt x:ident "with" alts:(colGe iinductionAlt)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
-  -- Parse the list of cases supplied by the user
+  -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseIInductionAlt
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do

From 3632223103f76a88f7e9c82cbf4bff3af5bc5251 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 17:55:43 +0200
Subject: [PATCH 39/54] More code refactoring

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 57 ++++++----------------
 1 file changed, 15 insertions(+), 42 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 33cb85475..bde7de888 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -33,23 +33,13 @@ open BI Std Lean Elab Tactic Meta Qq
 @[rocq_alias tac_revert_ih]
 theorem revert_IH [BI PROP] {P Q : PROP} {φ}
     (ih : φ)
-    (inst : IntoIH φ P Q)
-    (h1 : P ⊢ □ P) :
-    P ⊢ P ∗ □ Q := calc
-  P ⊢ □ P         := h1
+    (h : R ⊢ □ P)
+    (inst : IntoIH φ P Q) :
+    R ⊢ □ (P ∗ □ Q) := calc
+  _ ⊢ □ P         := h
   _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
   _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
   _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
-  _ ⊢ P ∗ □ Q     := sep_mono_l intuitionistically_elim
-
-/--
-  Given two intuitionistic propositions, their combined proposition
-  remains intuitionistic.
--/
-theorem combine_intuitionistic_props [BI PROP] {P Q : PROP}
-    (h1 : P ⊢ □ P) :
-    P ∗ □ Q ⊢ □ (P ∗ □ Q) := calc
-  _ ⊢ □ P ∗ □ Q   := sep_mono_l h1
   _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
   _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
 
@@ -58,44 +48,31 @@ theorem combine_intuitionistic_props [BI PROP] {P Q : PROP}
   hypotheses generated by Lean's built-in induction.
 -/
 private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop)) where
-  -- Hypotheses in the Iris proof goal
   {newE : Q($prop)}
   (newHyps : Hyps bi newE)
-  -- Proof that the hypotheses is intuitionsitic
-  (pfIntHyps : Q($newE ⊢ □ $newE))
-  (pf : Q($origE ⊢ $newE))
+  (pf : Q($origE ⊢ □ $newE))
 
 /--
   Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
   the subset of intuitionistic hypotheses in `hyps` that contains the `fvar`
   and all spatial hypotheses in the proof state.
+
+  This function is used for identifying the hypotheses in the Iris proof state
+  that must be reverted before applying Lean's built-in `induction` tactic.
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
-  let ivars := hyps.intuitionisticIVarIds.filter fun ivar =>
+  let ivars := hyps.intuitionisticIVarIds.filter <| fun ivar =>
     match hyps.getDecl? ivar with
     | some (_, _, _, ty) => ty.containsFVar fvar
     | none => false
 
-  (ivars ++ hyps.spatialIVarIds).map (
-    fun ivar => { kind := .ipm ivar, explicit := false }
-  )
+  (ivars ++ hyps.spatialIVarIds).map ({ kind := .ipm ·, explicit := false })
 
 /--
-  Given `h` of type `Hyps bi e`, search for all hypotheses in the intuitionistic
-  context, concatenate them using the separation conjunction and return
-  it as a single proposition.
+  Search for hypotheses in the regular Lean context that represent induction
+  hypotheses and return their IDs as a list.
 -/
-private def intuitionisticHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
-    (h : Hyps bi e) : ProofModeM Q($prop) := do
-  let props : List Q($prop) := h.intuitionisticProps
-  if props.isEmpty then
-    return q(emp)
-  else
-    return props.tail.reverse.foldr (fun acc tm => q(iprop($tm ∗ $acc))) props[0]!
-
-/-- Search for hypotheses in the regular Lean context that represent induction
-    hypotheses and return their IDs as a list. -/
 private def findIHs (m : MVarId) : MetaM (List FVarId) :=
   m.withContext do
     let lctx ← getLCtx
@@ -127,11 +104,7 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   let binderIdent ← `(binderIdent| $nameIdent:ident)
   let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
 
-  return {
-    newHyps,
-    pf := q($(st.pf).trans <| revert_IH $p $inst $st.pfIntHyps),
-    pfIntHyps := q(combine_intuitionistic_props $st.pfIntHyps)
-  }
+  return { newHyps, pf := q(revert_IH $p $st.pf $inst) }
 
 /--
   Introduce a list of induction hypotheses into Iris proof state.
@@ -144,7 +117,7 @@ private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
 
   -- Initialise the mutable instance of `InductionState`
   let mut st : InductionState e := {
-    newHyps := hyps, pf := q(.rfl), pfIntHyps
+    newHyps := hyps, pf := q($pfIntHyps)
   }
 
   -- Iteratively move the induction hypotheses into the intuitionistic context
@@ -277,7 +250,7 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           -- Remove the induction hypotheses from the regular Lean context
           let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
 
-          s.mvarId.assign <| q($(st.pf).trans $pf')
+          s.mvarId.assign <| q($(st.pf).trans <| intuitionistically_elim.trans $pf')
 
           -- Case applicable for `with` syntax only
           match parsedAlts with

From 1dbd7ac3b1716eef95d9410cdcf204603b9e1e56 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 18:25:45 +0200
Subject: [PATCH 40/54] More code refactoring 2 and fix tests

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 88 +++++++++++++++-------
 Iris/Iris/Tests/Tactics.lean               | 10 ++-
 2 files changed, 66 insertions(+), 32 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index bde7de888..e21d91d3d 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -85,16 +85,17 @@ private def findIHs (m : MVarId) : MetaM (List FVarId) :=
 
 /--
   Used for every induction hypothesis generated by Lean upon using the built-in
-  `induction` tactic. The type class `IntoIH` is used for obtaining the
-  corresponding proposition in the Iris proof mode.
+  `induction` tactic. This function is called by `addIHs` and returns
+  an instance of `InductionState` after handling one induction hypothesis.
 -/
-private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+private def addIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (st : @InductionState u prop bi e)
     (φ : Q(Prop)) (p : Q($φ)) (hFVar : FVarId) :
     ProofModeM (@InductionState u prop bi e) := do
   let oldE := st.newE
   let oldHyps : Hyps bi oldE := st.newHyps
 
+  -- Obtain the proposition to be introduced into the intuitionistic context
   let Q ← mkFreshExprMVarQ q($prop)
   let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $oldE $Q)
   | throwError "iinduction: type class synthesis with IntoIH failed"
@@ -107,40 +108,41 @@ private def addIntoIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   return { newHyps, pf := q(revert_IH $p $st.pf $inst) }
 
 /--
-  Introduce a list of induction hypotheses into Iris proof state.
-  The list of `FVarId` values (`ihFVars`) should be the list returned by
-  `findIHs`.
+  Introduce a list of induction hypotheses into the intuitionistic context
+  of the Iris proof state. The list of `FVarId` values (`ihFVars`) should be
+  the list returned by `findIHs`. The function returns the final
+  `InductionState` with all induction hypotheses handled.
+
+  The argument `pfIntHyps` holds when the spatial context is empty, which
+  is indeed the case when all hypotheses therein have been reverted.
 -/
-private def addAllIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+private def addIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
     (pfIntHyps : Q($e ⊢ □ $e)) (hyps : Hyps bi e) (ihFVars : List FVarId) :
     ProofModeM (@InductionState u prop bi e) := do
 
   -- Initialise the mutable instance of `InductionState`
-  let mut st : InductionState e := {
-    newHyps := hyps, pf := q($pfIntHyps)
-  }
+  let mut st : InductionState e := { newHyps := hyps, pf := q($pfIntHyps) }
 
   -- Iteratively move the induction hypotheses into the intuitionistic context
   for i in ihFVars do
     let p := mkFVar i
     let φ ← inferType (mkFVar i)
-    st ← addIntoIH st φ p i
+    st ← addIH st φ p i
 
   return st
 
 /--
   Given hypothesis `hyps` representing `e` where every hypothesis exist in the
-  intuitionistic context, `e ⊢ □ e` must hold.
+  intuitionistic context, return the proof of `e ⊢ □ e`. Throw an error if
+  `hyps` contains hypotheses in the spatial context.
 -/
 private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) : ProofModeM Q($e ⊢ □ $e) :=
   match hyps with
-  | .emp _ =>
-    pure q(intuitionistically_emp.mpr)
+  | .emp _ => pure q(intuitionistically_emp.mpr)
   | .hyp _ _ _ p _ _ =>
     match matchBool p with
-    | .inl _ =>
-      pure q(intuitionistically_idem.mpr)
+    | .inl _ => pure q(intuitionistically_idem.mpr)
     | .inr _ =>
       throwError "iinduction: spatial context is not empty after reverting hypotheses"
   | .sep _ _ _ _ lhs rhs => do
@@ -148,24 +150,42 @@ private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     let pfR ← buildPfIntHyps rhs
     pure q((sep_mono $pfL $pfR).trans intuitionistically_sep_2)
 
--- One case upon applying the `iinduction` tactic
-syntax iinductionAlt := "| " ident ident* " => " tacticSeq
+/--
+  Tactic syntax for user-supplied alternative names.
+-/
+syntax inductionAlts := "| " ident+ " => " tacticSeq
+
+/--
+  Parse the tactic syntax for user-supplied alternative names.
 
-private def parseIInductionAlt (alt : TSyntax `Iris.ProofMode.iinductionAlt) :
+  This function returns a triple, which includes:
+  1. the name of the constructor supplied by the user (`ctor.getId`),
+  2. the alternative names for that constructor (`vars`), and
+  3. the tactics for this induction subgoal.
+-/
+private def parseInductionAlts (alt : TSyntax `Iris.ProofMode.inductionAlts) :
     TacticM (Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
-  let `(iinductionAlt| | $ctor:ident $vars:ident* => $tac:tacticSeq) := alt
+  let `(inductionAlts| | $ctor:ident $vars:ident* => $tac:tacticSeq) := alt
   | throwError "iinduction: invalid syntax"
+  return ⟨ctor.getId, vars, tac⟩
 
-  return (ctor.getId, vars, tac)
-
-/-- Check whether a fully-qualified constructor name (e.g. `Nat.succ`) matches a
-    user-written short name (e.g. `succ`) or an already-qualified name. -/
+/--
+  Check whether a fully-qualified constructor name (e.g. `Nat.succ`) matches a
+  user-written short name (e.g. `succ`) or an already-qualified name.
+-/
 private def matchesCtorName (fullName : Name) (userShort : Name) : Bool :=
   fullName == userShort || fullName.getString! == userShort.getString!
 
+/--
+  Throw an error if the user has supplied some but not all alternative names.
+-/
 private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
   throwError "iinduction: alternative `{ctor.getString!}` has not been provided"
 
+/--
+  Checks whether an invalid constructor names have been supplied by the user.
+  Throw an error if this is the case.
+-/
 private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
   let invalidAltCtors :=
     altCtors.filter fun alt =>
@@ -173,8 +193,20 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 
   if !invalidAltCtors.isEmpty then
     let invalids := String.intercalate ", " <| invalidAltCtors.map (s!"`{·}`")
-    throwError m!"iinduction: invalid alternative names {invalids}"
+    throwError m!"iinduction: invalid alternative name(s): {invalids}"
 
+/--
+  The main function handling the steps for the `iinduction` tactic.
+  1. Revert intutionistic hypotheses that include `fvar` on which induction is performed.
+  2. Revert all spatial hypotheses in the Iris proof state.
+  3. Prepare the arguments for `Lean.Meta.Tactic.induction`.
+  4. Apply `Lean.Meta.Tactic.induction` to obtain the induction subgoals.
+  5. For each subgoal, move the induction hypotheses from the regular Lean
+     context into the Iris intuitionistic context.
+  6. Introduce reverted hypotheses back into the Iris proof state.
+
+  Step 1, 2 and 6 are handled by `iRevertIntro`, which is called by this function.
+-/
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
     (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) :
@@ -245,7 +277,7 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           let pfIntHyps ← buildPfIntHyps irisGoal.hyps
 
           -- Introduce the induction hypothesis back into the Iris proof state
-          let st ← addAllIHs pfIntHyps irisGoal.hyps ihFVars
+          let st ← addIHs pfIntHyps irisGoal.hyps ihFVars
 
           -- Remove the induction hypotheses from the regular Lean context
           let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
@@ -291,12 +323,12 @@ elab "iinduction" colGt x:ident : tactic => do
 /--
   Tactic with names of variables and induction hypotheses supplied by the user.
 -/
-elab "iinduction" colGt x:ident "with" alts:(colGe iinductionAlt)* : tactic => do
+elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => do
   -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
   -- Parse the list of alternative names supplied by the user
-  let parsedAlts ← alts.mapM parseIInductionAlt
+  let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let pf ← iInductionCore hyps goal fvar (some parsedAlts)
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index d812dd79e..6dc7bd374 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2753,16 +2753,18 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   iinduction n with
   | zero => itrivial
 
-/- Tests `iinduction` with induction on natural numbers with user-supplied
-    names, missing `succ` case -/
-/-- error: iinduction: invalid alternative names `a` -/
+/- Tests `iinduction` with induction on natural numbers with invalid
+   user-supplied names -/
+/-- error: iinduction: invalid alternative name(s): `invalidA`, `invalidB`, `invalidC` -/
 #guard_msgs in
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
   iinduction n with
+  | invalidA  => done
   | zero      => itrivial
-  | a         => itrivial
+  | invalidB  => done
   | succ n IH => iframe; itrivial
+  | invalidC  => done
 
 end iinduction

From e376e7047db5551add8b0646ed4646fe07aa22fc Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 31 May 2026 18:47:45 +0200
Subject: [PATCH 41/54] More code refactoring and formatting

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 55 ++++++++++++----------
 1 file changed, 30 insertions(+), 25 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index e21d91d3d..e7c853cc1 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -64,7 +64,7 @@ private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
     (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
   let ivars := hyps.intuitionisticIVarIds.filter <| fun ivar =>
     match hyps.getDecl? ivar with
-    | some (_, _, _, ty) => ty.containsFVar fvar
+    | some ⟨_, _, _, ty⟩ => ty.containsFVar fvar
     | none => false
 
   (ivars ++ hyps.spatialIVarIds).map ({ kind := .ipm ·, explicit := false })
@@ -126,7 +126,7 @@ private def addIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
   -- Iteratively move the induction hypotheses into the intuitionistic context
   for i in ihFVars do
     let p := mkFVar i
-    let φ ← inferType (mkFVar i)
+    let φ ← inferType <| mkFVar i
     st ← addIH st φ p i
 
   return st
@@ -219,25 +219,33 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
   | .const indName _ =>
     match (← getEnv).find? indName with
-    | some (.inductInfo val) => pure <| (Name.mkStr val.name "recOn", val.ctors)
+    | some (.inductInfo val) => pure <| (.mkStr val.name "recOn", val.ctors)
     | _ => throwError "iinduction: {indName} is not inductive"
   | _ => throwError "iinduction: unable to determine inductive type"
 
+  let matcher :
+    Name →
+    Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq →
+    Bool := fun ctor ⟨altCtor, _, _⟩ => matchesCtorName ctor altCtor
+
   -- Define the names for variables and induction hypotheses if supplied by user
   let varNames : Array AltVarNames ←
     match parsedAlts with
     | none =>
-      pure <| ctors.toArray.map (fun _ => {explicit := true, varNames := []})
+      pure <| ctors.toArray.map <| fun _ => { explicit := true, varNames := [] }
     | some parsedAlts => do
-      ctors.toArray.mapM fun ctor =>
-      match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
+      ctors.toArray.mapM <| fun ctor =>
+      match parsedAlts.find? <| matcher ctor with
       | some (_, vars, _) =>
-        pure ({ explicit := true, varNames := vars.toList.map (·.getId) } : AltVarNames)
+        pure { explicit := true, varNames := vars.toList.map (·.getId) }
       | none => throwMissingAlt ctor
 
-  -- Revert all hypotheses in the list
-  let pf ← iRevertIntro hyps goal targets (
-    -- The function takes the hypotheses and goal after reverting
+  -- Check that all alternative names supplied by the user are valid
+  match parsedAlts with
+  | none => pure ()
+  | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
+
+  let pf ← iRevertIntro hyps goal targets <|
     fun hyps' goal' k => do
       -- Create a new metavariable for the proof goal upon reverting hypotheses
       let m ← mkBIGoal hyps' goal'
@@ -246,25 +254,23 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
       let subgoals ←  m.mvarId!.withContext do
         m.mvarId!.induction fvar recName varNames
 
-      match parsedAlts with
-      | none => pure ()
-      | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
-
       -- Handle each subgoal generated by Lean's induction
-      for (s, ctor) in subgoals.toList.zip ctors do
+      for ⟨s, ctor⟩ in subgoals.toList.zip ctors do
         s.mvarId.withContext do
+          -- For pretty printing of arguments
           match parsedAlts with
           | none => pure ()
           | some parsedAlts =>
-            match parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor) with
-            | some (_, vars, _) =>
-              for (fieldFVar, varStx) in s.fields.toList.zip vars.toList do
+            match parsedAlts.find? <| matcher ctor with
+            | some ⟨_, vars, _⟩ =>
+              for ⟨fieldFVar, varStx⟩ in s.fields.toList.zip vars.toList do
               let lctx ← getLCtx
               let fieldType ← inferType fieldFVar
-              addLocalVarInfo varStx lctx fieldFVar (some fieldType) (isBinder := true)
+              addLocalVarInfo varStx lctx fieldFVar (some fieldType) true
             | none => throwMissingAlt ctor
 
-          let sType ← instantiateMVars (← s.mvarId.getType)
+          -- Obtain the type of the induction subgoal
+          let sType ← instantiateMVars <| ← s.mvarId.getType
 
           let some irisGoal := parseIrisGoal? sType
           -- This should not happen
@@ -279,9 +285,10 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           -- Introduce the induction hypothesis back into the Iris proof state
           let st ← addIHs pfIntHyps irisGoal.hyps ihFVars
 
-          -- Remove the induction hypotheses from the regular Lean context
+          -- Generate the induction subgoal for the user
           let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
 
+          -- Fill the metavariable for the induction subgoal generated by Lean
           s.mvarId.assign <| q($(st.pf).trans <| intuitionistically_elim.trans $pf')
 
           -- Case applicable for `with` syntax only
@@ -289,10 +296,9 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           | none => pure ()
           | some parsedAlts =>
             let biGoalMVar := (← getThe ProofModeM.State).goals.back!
-            modify (fun s => { s with goals := s.goals.pop })
+            modify <| fun s => { s with goals := s.goals.pop }
 
-            let some (_, _, userTac) :=
-            parsedAlts.find? (fun (altCtor, _, _) => matchesCtorName ctor altCtor)
+            let some ⟨_, _, userTac⟩ := parsedAlts.find? <| matcher ctor
             | throwMissingAlt ctor
 
             -- Run the user tactic on the BI goal
@@ -304,7 +310,6 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
             for r in remaining do addMVarGoal r
 
       return m
-  )
 
   return pf
 

From bff359b3be7e1cfb69247d35c9c290f5a9ebdd57 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 11:14:58 +0200
Subject: [PATCH 42/54] Implement iinduction ... using ... (user-supplied
 recursor name)

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 32 +++++++++++++++++-----
 Iris/Iris/Tests/Tactics.lean               | 17 +++++++++++-
 2 files changed, 41 insertions(+), 8 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index e7c853cc1..4707c7d27 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -209,17 +209,24 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 -/
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
-    (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) :
+    (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (altRecName : Option Name) :
     ProofModeM Q($e ⊢ $goal) := do
   -- Find all hypotheses that contain the variable being performed induction on
   let targets := iHypsContaining hyps fvar
 
-  -- Find the recursor name for induction
+  -- Find the recursor name and constructor names of the inductive datatype
   let fvarType ← whnf <| ← inferType <| mkFVar fvar
   let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
   | .const indName _ =>
     match (← getEnv).find? indName with
-    | some (.inductInfo val) => pure <| (.mkStr val.name "recOn", val.ctors)
+    | some (.inductInfo val) =>
+        -- Use the user-supplied recursor name if available
+        let some recName ← match altRecName with
+          | none => getCustomEliminator? #[mkFVar fvar] true
+          | some altRecName => pure altRecName
+        | throwError "iinduction: unable to determine recursor name"
+        pure (recName, val.ctors)
     | _ => throwError "iinduction: {indName} is not inductive"
   | _ => throwError "iinduction: unable to determine inductive type"
 
@@ -318,23 +325,34 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   generated by Lean automatically.
 -/
 elab "iinduction" colGt x:ident : tactic => do
-  -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar none
+    let pf ← iInductionCore hyps goal fvar none none
     mvar.assign pf
 
 /--
   Tactic with names of variables and induction hypotheses supplied by the user.
 -/
 elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => do
-  -- Get the ID of the variable on which induction is being performed
   let fvar ← getFVarId x
 
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar (some parsedAlts)
+    let pf ← iInductionCore hyps goal fvar (some parsedAlts) none
+    mvar.assign pf
+
+/--
+  Tactic with the recursor name supplied by the user.
+-/
+elab "iinduction" colGt x:ident "using" r:ident : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none recName
     mvar.assign pf
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 6dc7bd374..f8aad4420 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2735,7 +2735,7 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   iintro HP #HQ #HR HS #HT
   iinduction n with
   | Nat.zero  => itrivial          -- Using the full name of the constructor
-  | succ n IH => iframe; itrivial  -- Using the short name of the constructor
+  | succ n ih => iframe; itrivial  -- Using the short name of the constructor
 
 /- Tests `iinduction` with a non-inductive datatype -/
 /-- error: iinduction: unable to determine inductive type -/
@@ -2767,4 +2767,19 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   | succ n IH => iframe; itrivial
   | invalidC  => done
 
+/-- Tests `iinduction` using a custom recursor name. -/
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n using Nat.recOn
+  · itrivial
+  · iframe; itrivial
+
+/-- Tests `iinduction` using a custom recursor name. -/
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n using Nat.strongRecOn  -- TODO: IH with regular hypothesis
+  itrivial
+
 end iinduction

From e87b6078a30d308b31812234d40ad2e0ed6ec4a9 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 11:43:56 +0200
Subject: [PATCH 43/54] Implement iinduction ... using ... with

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 15 +++++++--------
 Iris/Iris/Tests/Tactics.lean               |  8 ++++++++
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 4707c7d27..0dd45796d 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -331,9 +331,7 @@ elab "iinduction" colGt x:ident : tactic => do
     let pf ← iInductionCore hyps goal fvar none none
     mvar.assign pf
 
-/--
-  Tactic with names of variables and induction hypotheses supplied by the user.
--/
+/-- Tactic with names of variables and induction hypotheses supplied by the user. -/
 elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← getFVarId x
 
@@ -344,15 +342,16 @@ elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => d
     let pf ← iInductionCore hyps goal fvar (some parsedAlts) none
     mvar.assign pf
 
-/--
-  Tactic with the recursor name supplied by the user.
--/
-elab "iinduction" colGt x:ident "using" r:ident : tactic => do
+/-- Tactic with the recursor name and alternative names supplied by the user. -/
+elab "iinduction" colGt x:ident "using" r:ident "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← getFVarId x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
 
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar none recName
+    let pf ← iInductionCore hyps goal fvar (some parsedAlts) recName
     mvar.assign pf
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index f8aad4420..81c3847da 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2782,4 +2782,12 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   iinduction n using Nat.strongRecOn  -- TODO: IH with regular hypothesis
   itrivial
 
+/-- Tests `iinduction` using a custom recursor name. -/
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  induction n using Nat.rec with
+  | zero     => sorry
+  | succ _ _ => sorry
+
 end iinduction

From a8daced999fac59fd9576d3b59ec319a095a676b Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 13:45:44 +0200
Subject: [PATCH 44/54] Implement iinduction ... generalizing ...

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 86 ++++++++++++++++++++--
 1 file changed, 78 insertions(+), 8 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 0dd45796d..68a668949 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -61,10 +61,10 @@ private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop))
   that must be reverted before applying Lean's built-in `induction` tactic.
 -/
 private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
-    (hyps : Hyps bi e) (fvar : FVarId) : List SelTarget :=
+    (hyps : Hyps bi e) (fvars : List FVarId) : List SelTarget :=
   let ivars := hyps.intuitionisticIVarIds.filter <| fun ivar =>
     match hyps.getDecl? ivar with
-    | some ⟨_, _, _, ty⟩ => ty.containsFVar fvar
+    | some ⟨_, _, _, ty⟩ => fvars.any ty.containsFVar
     | none => false
 
   (ivars ++ hyps.spatialIVarIds).map ({ kind := .ipm ·, explicit := false })
@@ -210,10 +210,22 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
     (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)
-    (altRecName : Option Name) :
+    (altRecName : Option Name)
+    (genFVars : Option <| List FVarId) :
     ProofModeM Q($e ⊢ $goal) := do
   -- Find all hypotheses that contain the variable being performed induction on
-  let targets := iHypsContaining hyps fvar
+  let targets :=
+    match genFVars with
+    | none => iHypsContaining hyps [fvar]
+    | some genFVars => iHypsContaining hyps <| [fvar] ++ genFVars
+
+  -- User-supplied list of targets for reverting
+  let genTargets : List SelTarget :=
+    match genFVars with
+    | some genFVars => genFVars.map ({ kind := .pure ·, explicit := true })
+    | none => []
+
+  let targets := genTargets ++ targets
 
   -- Find the recursor name and constructor names of the inductive datatype
   let fvarType ← whnf <| ← inferType <| mkFVar fvar
@@ -298,7 +310,7 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           -- Fill the metavariable for the induction subgoal generated by Lean
           s.mvarId.assign <| q($(st.pf).trans <| intuitionistically_elim.trans $pf')
 
-          -- Case applicable for `with` syntax only
+          -- Handle user-supplied tactics for specific constructors
           match parsedAlts with
           | none => pure ()
           | some parsedAlts =>
@@ -328,7 +340,7 @@ elab "iinduction" colGt x:ident : tactic => do
   let fvar ← getFVarId x
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar none none
+    let pf ← iInductionCore hyps goal fvar none none none
     mvar.assign pf
 
 /-- Tactic with names of variables and induction hypotheses supplied by the user. -/
@@ -339,7 +351,18 @@ elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => d
   let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar (some parsedAlts) none
+    let pf ← iInductionCore hyps goal fvar parsedAlts none none
+    mvar.assign pf
+
+/-- Tactic with the recursor name supplied by the user. -/
+elab "iinduction" colGt x:ident "using" r:ident : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none recName none
     mvar.assign pf
 
 /-- Tactic with the recursor name and alternative names supplied by the user. -/
@@ -348,10 +371,57 @@ elab "iinduction" colGt x:ident "using" r:ident "with" alts:(colGe inductionAlts
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar parsedAlts recName none
+    mvar.assign pf
+
+elab "iinduction" colGt x:ident "generalizing" genIds:ident+ : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the user-supplied list of variables to be generalised
+  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none none genFVars
+    mvar.assign pf
 
+elab "iinduction" colGt x:ident "generalizing" genIds:ident+ "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the user-supplied list of variables to be generalised
+  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar parsedAlts none genFVars
+    mvar.assign pf
+
+elab "iinduction" colGt x:ident "using" r:ident "generalizing" genIds:ident+ : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+  -- Parse the user-supplied list of variables to be generalised
+  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none recName genFVars
+    mvar.assign pf
+
+elab "iinduction" colGt x:ident "using" r:ident "generalizing" genIds:ident+ "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← getFVarId x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+  -- Parse the user-supplied list of variables to be generalised
+  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar (some parsedAlts) recName
+    let pf ← iInductionCore hyps goal fvar parsedAlts recName genFVars
     mvar.assign pf

From ab75206e1de2596a2463d0d908b1cf6f4fe7fa25 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 14:35:36 +0200
Subject: [PATCH 45/54] Fix iinduction ... generalizing ... 1. Revert Iris
 hypothesis explcitly specified by the user using `generalizing` syntax 2.
 Revert all spatial hypotheses, relevant intuitionistic hypotheses 3. Revert
 pure Lean variables specified by the user using `generalizing` syntax

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 93 +++++++++++++---------
 1 file changed, 57 insertions(+), 36 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 68a668949..7cc610efe 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -197,35 +197,49 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 
 /--
   The main function handling the steps for the `iinduction` tactic.
-  1. Revert intutionistic hypotheses that include `fvar` on which induction is performed.
-  2. Revert all spatial hypotheses in the Iris proof state.
-  3. Prepare the arguments for `Lean.Meta.Tactic.induction`.
-  4. Apply `Lean.Meta.Tactic.induction` to obtain the induction subgoals.
-  5. For each subgoal, move the induction hypotheses from the regular Lean
+
+  1. Revert Iris hypotheses explicitly specified by the tactic user
+     (applicable when the `generalizing` syntax is used).
+  2. Revert all spatial hypotheses in the Iris proof state as well as the
+     relevant hypotheses in the intuitionistic context.
+  3. Revert pure Lean variables specified by the tactic user
+     (applicable when the `generalizing` syntax is used).
+  4. Prepare the arguments for `Lean.Meta.Tactic.induction`.
+  5. Apply `Lean.Meta.Tactic.induction` to obtain the induction subgoals.
+  6. For each subgoal, move the induction hypotheses from the regular Lean
      context into the Iris intuitionistic context.
-  6. Introduce reverted hypotheses back into the Iris proof state.
+  7. Introduce hypotheses reverted in steps 1 and 2 back into the Iris proof state.
 
-  Step 1, 2 and 6 are handled by `iRevertIntro`, which is called by this function.
+  The relevant intuitionistic hypotheses to which Step 2 refers are those
+  involving `fvar` or pure Lean variables in `genSelTargets`.
 -/
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
     (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)
     (altRecName : Option Name)
-    (genFVars : Option <| List FVarId) :
+    (genSelTargets : Option <| List SelTarget) :
     ProofModeM Q($e ⊢ $goal) := do
-  -- Find all hypotheses that contain the variable being performed induction on
-  let targets :=
-    match genFVars with
-    | none => iHypsContaining hyps [fvar]
-    | some genFVars => iHypsContaining hyps <| [fvar] ++ genFVars
-
-  -- User-supplied list of targets for reverting
-  let genTargets : List SelTarget :=
-    match genFVars with
-    | some genFVars => genFVars.map ({ kind := .pure ·, explicit := true })
+  -- Iris hypotheses to be reverted as specified by the user using the `generalizing` syntax
+  let explicitIrisTargets : List SelTarget :=
+    match genSelTargets with
+    | none => []
+    | some genSelTargets => genSelTargets.filter <| fun t => match t.kind with | .ipm _ => true | _ => false
+
+  -- `FVarID` values of pure hypothesis specified by the user using the `generalizing` syntax
+  let pureFVars : List FVarId :=
+    match genSelTargets with
     | none => []
+    | some genSelTargets =>
+      genSelTargets.filterMap <| fun t => match t.kind with | .pure f => some f | _ => none
+
+  -- Iris hypotheses in the spatial context and relevant intuitionistic context
+  let spatialAndIntuitionisticTargets := iHypsContaining hyps <| pureFVars.concat fvar
+
+  -- Pure hypotheses to be reverted as specified by the user using the `generalizing` syntax
+  let pureTargets : List SelTarget := pureFVars.map ({ kind := .pure ·, explicit := true })
 
-  let targets := genTargets ++ targets
+  -- Those in `explicitIrisTargets` get reverted first, so they are last in the list
+  let targets := pureTargets ++ spatialAndIntuitionisticTargets ++ explicitIrisTargets
 
   -- Find the recursor name and constructor names of the inductive datatype
   let fvarType ← whnf <| ← inferType <| mkFVar fvar
@@ -378,50 +392,57 @@ elab "iinduction" colGt x:ident "using" r:ident "with" alts:(colGe inductionAlts
     let pf ← iInductionCore hyps goal fvar parsedAlts recName none
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "generalizing" genIds:ident+ : tactic => do
+elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
   let fvar ← getFVarId x
 
-  -- Parse the user-supplied list of variables to be generalised
-  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
-
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar none none genFVars
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar none none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "generalizing" genIds:ident+ "with" alts:(colGe inductionAlts)* : tactic => do
+elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← getFVarId x
 
-  -- Parse the user-supplied list of variables to be generalised
-  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar parsedAlts none genFVars
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar parsedAlts none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "using" r:ident "generalizing" genIds:ident+ : tactic => do
+elab "iinduction" colGt x:ident "using" r:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
   let fvar ← getFVarId x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
-  -- Parse the user-supplied list of variables to be generalised
-  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar none recName genFVars
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar none recName genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "using" r:ident "generalizing" genIds:ident+ "with" alts:(colGe inductionAlts)* : tactic => do
+elab "iinduction" colGt x:ident "using" r:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← getFVarId x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
-  -- Parse the user-supplied list of variables to be generalised
-  let genFVars ← genIds.toList.mapM <| fun id => getFVarId id.raw
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iInductionCore hyps goal fvar parsedAlts recName genFVars
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar parsedAlts recName genSelTargets
     mvar.assign pf

From 34fece6270b126fa329cf1353200b15ce0961598 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 15:14:15 +0200
Subject: [PATCH 46/54] Use binderIdent instead of ident for `with` syntax to
 support underscores for inaccessible names

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 23 +++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 7cc610efe..3ef6eec31 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -153,7 +153,7 @@ private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 /--
   Tactic syntax for user-supplied alternative names.
 -/
-syntax inductionAlts := "| " ident+ " => " tacticSeq
+syntax inductionAlts := "| " binderIdent+ " => " tacticSeq
 
 /--
   Parse the tactic syntax for user-supplied alternative names.
@@ -164,8 +164,8 @@ syntax inductionAlts := "| " ident+ " => " tacticSeq
   3. the tactics for this induction subgoal.
 -/
 private def parseInductionAlts (alt : TSyntax `Iris.ProofMode.inductionAlts) :
-    TacticM (Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
-  let `(inductionAlts| | $ctor:ident $vars:ident* => $tac:tacticSeq) := alt
+    TacticM (Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
+  let `(inductionAlts| | $ctor:ident $vars:binderIdent* => $tac:tacticSeq) := alt
   | throwError "iinduction: invalid syntax"
   return ⟨ctor.getId, vars, tac⟩
 
@@ -215,7 +215,7 @@ private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
 -/
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
-    (parsedAlts : Option <| Array <| Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (parsedAlts : Option <| Array <| Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq)
     (altRecName : Option Name)
     (genSelTargets : Option <| List SelTarget) :
     ProofModeM Q($e ⊢ $goal) := do
@@ -258,7 +258,7 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   let matcher :
     Name →
-    Name × Array (TSyntax `ident) × TSyntax `Lean.Parser.Tactic.tacticSeq →
+    Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq →
     Bool := fun ctor ⟨altCtor, _, _⟩ => matchesCtorName ctor altCtor
 
   -- Define the names for variables and induction hypotheses if supplied by user
@@ -270,7 +270,11 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
       ctors.toArray.mapM <| fun ctor =>
       match parsedAlts.find? <| matcher ctor with
       | some (_, vars, _) =>
-        pure { explicit := true, varNames := vars.toList.map (·.getId) }
+        pure { explicit := true, varNames := vars.toList.map <|
+          fun v =>
+            match v.raw with
+            | `(binderIdent| $id:ident) => id.getId
+            | _ => Name.mkSimple "_" }
       | none => throwMissingAlt ctor
 
   -- Check that all alternative names supplied by the user are valid
@@ -297,9 +301,10 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
             match parsedAlts.find? <| matcher ctor with
             | some ⟨_, vars, _⟩ =>
               for ⟨fieldFVar, varStx⟩ in s.fields.toList.zip vars.toList do
-              let lctx ← getLCtx
-              let fieldType ← inferType fieldFVar
-              addLocalVarInfo varStx lctx fieldFVar (some fieldType) true
+                if let `(binderIdent| $id:ident) := varStx then
+                  let lctx ← getLCtx
+                  let fieldType ← inferType fieldFVar
+                  addLocalVarInfo id lctx fieldFVar (some fieldType) true
             | none => throwMissingAlt ctor
 
           -- Obtain the type of the induction subgoal

From cc8136808d336476c6ae04829c0346ca773531d5 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 16:01:28 +0200
Subject: [PATCH 47/54] Catch invalid, missing and duplicate constructor names
 when `with` syntax is used

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 44 +++++++++++++++-------
 1 file changed, 31 insertions(+), 13 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 3ef6eec31..abd5cd121 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -73,7 +73,7 @@ private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
   Search for hypotheses in the regular Lean context that represent induction
   hypotheses and return their IDs as a list.
 -/
-private def findIHs (m : MVarId) : MetaM (List FVarId) :=
+private def findIHs (m : MVarId) : ProofModeM (List FVarId) :=
   m.withContext do
     let lctx ← getLCtx
     let mut ihs := []
@@ -183,17 +183,35 @@ private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
   throwError "iinduction: alternative `{ctor.getString!}` has not been provided"
 
 /--
-  Checks whether an invalid constructor names have been supplied by the user.
-  Throw an error if this is the case.
+  Checks whether an invalid, missing and/or duplicate constructor names have
+  been supplied by the user. Throw an error if this is the case.
 -/
-private def checkCtors (ctors altCtors : List Name) : MetaM Unit := do
+private def checkCtors (ctors altCtors : List Name) : ProofModeM Unit := do
+  let mut errors : List String := []
+
+  -- Check for missing constructor names
+  let missingAltCtors :=
+    ctors.filter (not <| altCtors.any <| fun altCtor => matchesCtorName · altCtor)
+
+  -- Check for invalid constructor names
   let invalidAltCtors :=
-    altCtors.filter fun alt =>
-      not <| ctors.any fun ctor => matchesCtorName ctor alt
+    altCtors.filter (not <| ctors.any <| fun ctor => matchesCtorName ctor ·)
 
+  -- Check for duplicate constructor names
+  let dupAltCtors := (altCtors.filter (fun alt => altCtors.countP (fun alt' => matchesCtorName alt alt') > 1)).eraseDupsBy matchesCtorName
+
+  if !missingAltCtors.isEmpty then
+    let missing := ", ".intercalate  <| missingAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: missing alternative name(s): {missing}"
+  if !dupAltCtors.isEmpty then
+    let dups := ", ".intercalate  <| dupAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: duplicate alternative name(s): {dups}"
   if !invalidAltCtors.isEmpty then
-    let invalids := String.intercalate ", " <| invalidAltCtors.map (s!"`{·}`")
-    throwError m!"iinduction: invalid alternative name(s): {invalids}"
+    let invalids := ", ".intercalate <| invalidAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: invalid alternative name(s): {invalids}"
+
+  if !errors.isEmpty then
+    throwError m!"{"\n".intercalate errors}"
 
 /--
   The main function handling the steps for the `iinduction` tactic.
@@ -261,6 +279,11 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq →
     Bool := fun ctor ⟨altCtor, _, _⟩ => matchesCtorName ctor altCtor
 
+  -- Check that all alternative names supplied by the user are valid
+  match parsedAlts with
+  | none => pure ()
+  | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
+
   -- Define the names for variables and induction hypotheses if supplied by user
   let varNames : Array AltVarNames ←
     match parsedAlts with
@@ -277,11 +300,6 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
             | _ => Name.mkSimple "_" }
       | none => throwMissingAlt ctor
 
-  -- Check that all alternative names supplied by the user are valid
-  match parsedAlts with
-  | none => pure ()
-  | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
-
   let pf ← iRevertIntro hyps goal targets <|
     fun hyps' goal' k => do
       -- Create a new metavariable for the proof goal upon reverting hypotheses

From 1525cd2402601ab3a6d86ce5bd6e5160f14a868b Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 16:30:42 +0200
Subject: [PATCH 48/54] Hypotheses explicitly reverted by the user using the
 `generalized` syntax do not require reverting again when other spatial and
 intuitionistic hypotheses are reverted

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index abd5cd121..5490873c2 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -253,6 +253,9 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
   -- Iris hypotheses in the spatial context and relevant intuitionistic context
   let spatialAndIntuitionisticTargets := iHypsContaining hyps <| pureFVars.concat fvar
 
+  let spatialAndIntuitionisticTargets :=
+    spatialAndIntuitionisticTargets.filter (not <| (explicitIrisTargets.map (·.kind)).contains ·.kind)
+
   -- Pure hypotheses to be reverted as specified by the user using the `generalizing` syntax
   let pureTargets : List SelTarget := pureFVars.map ({ kind := .pure ·, explicit := true })
 

From 559ba5ac37283ead19b92df7f03eb095ad95337b Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 16:38:23 +0200
Subject: [PATCH 49/54] Consolidate tests for iinduction

---
 Iris/Iris/Tests/Tactics.lean | 76 +++++++++++++++---------------------
 1 file changed, 32 insertions(+), 44 deletions(-)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 81c3847da..56526d4e9 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2718,24 +2718,37 @@ end iloeb
 
 section iinduction
 
-/-- Tests `iinduction` with induction on natural numbers. Hypotheses in the
-    spatial context become premises of the induction hypothesis. -/
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
-  iintro HP #HQ #HR HS #HT
-  iinduction n
-  · itrivial
-  · iframe
-    itrivial
+/--
+  Tests `iinduction` with induction on natural numbers.
+
+  For natural numbers, `Nat.recAux` is used as the default recursor name. Hence,
+  the tactic is equivalent to `iinduction n using Nat.recAux generalizing %P HQ %R`.
+
+  Hypotheses in the spatial context necessarily become premises of the
+  induction hypothesis.
+
+  With the `generalizing` syntax, `P` and `R` are universally quantified
+  in the induction hypothesis. Given they occur in `HP` and `HR`, respectively,
+  the two propositions are included as premises of the induction hypothesis.
 
-/-- Tests `iinduction` with induction on natural numbers with user-supplied
-    names for variables and induction hypotheses. -/
+  Meanwhile, `HQ` is included as a premise of the induction hypothesis without
+  `Q` being universally quantified.
+
+  Note that the following variants of the tactic all produce equivalent subgoals:
+  - `induction n generalizing %P HP HQ %R`
+  - `induction n generalizing %P HQ %R HR`
+  - `induction n generalizing %P HP HQ %R HR`
+  - the tactics above with any permutations of `generalizing` arguments.
+-/
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n with
-  | Nat.zero  => itrivial          -- Using the full name of the constructor
-  | succ n ih => iframe; itrivial  -- Using the short name of the constructor
+  iinduction n generalizing %P HQ %R with
+  -- Using the full name of the constructor (`Nat.zero`)
+  | Nat.zero  => itrivial
+  /- Using the short name of the constructor (`succ`), naming the induction
+     hypothesis as `ih`, but leaving the variable `n` inaccessible by using `_` -/
+  | succ _ ih => iframe; itrivial
 
 /- Tests `iinduction` with a non-inductive datatype -/
 /-- error: iinduction: unable to determine inductive type -/
@@ -2743,19 +2756,10 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
 example [BI PROP] {P : PROP} : ⊢ P := by
   iinduction P
 
-/- Tests `iinduction` with induction on natural numbers with user-supplied
-    names, missing `succ` case -/
-/-- error: iinduction: alternative `succ` has not been provided -/
-#guard_msgs in
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
-  iintro HP #HQ #HR HS #HT
-  iinduction n with
-  | zero => itrivial
-
-/- Tests `iinduction` with induction on natural numbers with invalid
-   user-supplied names -/
-/-- error: iinduction: invalid alternative name(s): `invalidA`, `invalidB`, `invalidC` -/
+/- Tests `iinduction` with induction on natural numbers with invalid user-supplied names -/
+/-- error: iinduction: missing alternative name(s): `Nat.succ`
+iinduction: duplicate alternative name(s): `zero`
+iinduction: invalid alternative name(s): `invalidA`, `invalidB`, `invalidC` -/
 #guard_msgs in
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
@@ -2764,17 +2768,9 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   | invalidA  => done
   | zero      => itrivial
   | invalidB  => done
-  | succ n IH => iframe; itrivial
+  | Nat.zero  => itrivial
   | invalidC  => done
 
-/-- Tests `iinduction` using a custom recursor name. -/
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
-  iintro HP #HQ #HR HS #HT
-  iinduction n using Nat.recOn
-  · itrivial
-  · iframe; itrivial
-
 /-- Tests `iinduction` using a custom recursor name. -/
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
@@ -2782,12 +2778,4 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   iinduction n using Nat.strongRecOn  -- TODO: IH with regular hypothesis
   itrivial
 
-/-- Tests `iinduction` using a custom recursor name. -/
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
-  iintro HP #HQ #HR HS #HT
-  induction n using Nat.rec with
-  | zero     => sorry
-  | succ _ _ => sorry
-
 end iinduction

From 10589a5e2b66bb0e9db7ae11197f3737f2adc24d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 17:17:00 +0200
Subject: [PATCH 50/54] Define new function isIrisGoalWithForalls for findIHs:
 search for Iris goals with leading universal quantifiers

---
 Iris/Iris/ProofMode/Expr.lean              | 5 +++++
 Iris/Iris/ProofMode/Tactics/Induction.lean | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index a45f3e023..8c74c91fc 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -490,6 +490,11 @@ structure IrisGoal where
 
 def isIrisGoal (expr : Expr) : Bool := isAppOfArity expr ``Entails' 4
 
+partial def isIrisGoalWithForalls (expr : Expr) : Bool :=
+  match expr.consumeMData with
+  | .forallE _ _ e _ => isIrisGoalWithForalls e
+  | e => isIrisGoal e
+
 def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
   -- remove top-level metadata when matching on the goal
   let expr := expr.consumeMData
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 5490873c2..a848f2101 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -79,7 +79,7 @@ private def findIHs (m : MVarId) : ProofModeM (List FVarId) :=
     let mut ihs := []
     for decl in lctx do
       let type ← instantiateMVars decl.type
-      if isIrisGoal type then
+      if isIrisGoalWithForalls type then
         ihs := decl.fvarId :: ihs
     return ihs.reverse
 

From 58efe2c804163d1e5024d6f8f36830246dd0a9c5 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 17:17:29 +0200
Subject: [PATCH 51/54] Fix priority of IntoIH instances

---
 Iris/Iris/ProofMode/Instances.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 5e309e3d8..762aca43c 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -924,7 +924,7 @@ instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
   into_ih := λ hpq => intuitionistically_elim.trans hpq
 
 @[rocq_alias into_ih_forall]
-instance intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
+instance (priority := default - 2) intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
     [h : ∀ x, IntoIH (φ x) P (Φ x)] :
     IntoIH (∀ x, φ x) P (BI.forall Φ) where
   into_ih := by
@@ -934,7 +934,7 @@ instance intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP
     exact (h x).into_ih (hφ x)
 
 @[rocq_alias into_ih_impl]
-instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
+instance (priority := default - 1) intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
     [h1 : MakeAffinely iprop(⌜φ⌝) P]
     [h2 : IntoIH ψ Δ Q] :
     IntoIH (φ → ψ) Δ iprop(P -∗ Q) where

From 062ec019541d84cff34147ab5766c0c61f6b5d96 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 17:18:03 +0200
Subject: [PATCH 52/54] More iinduction tests

---
 Iris/Iris/Tests/Tactics.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 56526d4e9..309138311 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2725,7 +2725,8 @@ section iinduction
   the tactic is equivalent to `iinduction n using Nat.recAux generalizing %P HQ %R`.
 
   Hypotheses in the spatial context necessarily become premises of the
-  induction hypothesis.
+  induction hypothesis. The intuitionistic hypothesis `T n` is reverted
+  because it depends on `n`.
 
   With the `generalizing` syntax, `P` and `R` are universally quantified
   in the induction hypothesis. Given they occur in `HP` and `HR`, respectively,
@@ -2740,8 +2741,8 @@ section iinduction
   - `induction n generalizing %P HP HQ %R HR`
   - the tactics above with any permutations of `generalizing` arguments.
 -/
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+example [BI PROP] {P Q R S : PROP} {T : Nat → PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T n -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
   iinduction n generalizing %P HQ %R with
   -- Using the full name of the constructor (`Nat.zero`)
@@ -2775,7 +2776,7 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
 example [BI PROP] {P Q R S T : PROP} {n : Nat} :
     ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n using Nat.strongRecOn  -- TODO: IH with regular hypothesis
+  iinduction n using Nat.strongRecOn
   itrivial
 
 end iinduction

From 9a17cbaf1e4a8abfc47f150876db086a42549b62 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 17:50:39 +0200
Subject: [PATCH 53/54] Generalisation to provide support for expressions, not
 just idents

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 50 +++++++++++++++-------
 Iris/Iris/Tests/Tactics.lean               |  8 ++--
 2 files changed, 38 insertions(+), 20 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index a848f2101..97cf03a58 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -372,20 +372,38 @@ private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
   return pf
 
+/--
+  Given a term expression, check whether it is a `FVarId` value. If so,
+  return it directly. Otherwise, generalise the term expressions before
+  returning its `FVarId`.
+-/
+private def termToFVar (x : TSyntax `term) : TacticM FVarId := do
+  let e ← withMainContext <| elabTerm x none
+  let e ← instantiateMVars e
+
+  if e.isFVar then
+    return e.fvarId!
+
+  let mvarId ← getMainGoal
+  let (fvars, newMVarId) ← mvarId.generalize #[{ expr := e }]
+  replaceMainGoal [newMVarId]
+
+  return fvars[0]!
+
 /--
   Simple tactic with inaccessible names of variables and induction hypotheses
   generated by Lean automatically.
 -/
-elab "iinduction" colGt x:ident : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term : tactic => do
+  let fvar ← termToFVar x
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let pf ← iInductionCore hyps goal fvar none none none
     mvar.assign pf
 
 /-- Tactic with names of variables and induction hypotheses supplied by the user. -/
-elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
@@ -395,8 +413,8 @@ elab "iinduction" colGt x:ident "with" alts:(colGe inductionAlts)* : tactic => d
     mvar.assign pf
 
 /-- Tactic with the recursor name supplied by the user. -/
-elab "iinduction" colGt x:ident "using" r:ident : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "using" r:ident : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
@@ -406,8 +424,8 @@ elab "iinduction" colGt x:ident "using" r:ident : tactic => do
     mvar.assign pf
 
 /-- Tactic with the recursor name and alternative names supplied by the user. -/
-elab "iinduction" colGt x:ident "using" r:ident "with" alts:(colGe inductionAlts)* : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "using" r:ident "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
@@ -418,8 +436,8 @@ elab "iinduction" colGt x:ident "using" r:ident "with" alts:(colGe inductionAlts
     let pf ← iInductionCore hyps goal fvar parsedAlts recName none
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ : tactic => do
+  let fvar ← termToFVar x
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     -- Parse the user-supplied list of variables to be generalised
@@ -429,8 +447,8 @@ elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ : tact
     let pf ← iInductionCore hyps goal fvar none none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the list of alternative names supplied by the user
   let parsedAlts ← alts.mapM parseInductionAlts
@@ -443,8 +461,8 @@ elab "iinduction" colGt x:ident "generalizing" genSelPats:(colGt selPat)+ "with"
     let pf ← iInductionCore hyps goal fvar parsedAlts none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "using" r:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "using" r:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
@@ -457,8 +475,8 @@ elab "iinduction" colGt x:ident "using" r:ident "generalizing" genSelPats:(colGt
     let pf ← iInductionCore hyps goal fvar none recName genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:ident "using" r:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
-  let fvar ← getFVarId x
+elab "iinduction" colGt x:term "using" r:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
   let recName := r.getId
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 309138311..754884e4c 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2772,11 +2772,11 @@ example [BI PROP] {P Q R S T : PROP} {n : Nat} :
   | Nat.zero  => itrivial
   | invalidC  => done
 
-/-- Tests `iinduction` using a custom recursor name. -/
-example [BI PROP] {P Q R S T : PROP} {n : Nat} :
-    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+/-- Tests `iinduction` using a custom recursor name and expression -/
+example [BI PROP] {P R S : PROP} {Q T : Nat → PROP} {n : Nat} :
+    ⊢ P -∗ □ Q m -∗ □ R -∗ S -∗ □ T n -∗ ⌜n + m + 0 = n + m⌝ := by
   iintro HP #HQ #HR HS #HT
-  iinduction n using Nat.strongRecOn
+  iinduction n + m using Nat.strongRecOn
   itrivial
 
 end iinduction

From 18a9e311dd9f9820f30702ecff8f571ee6310b13 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Mon, 1 Jun 2026 18:06:53 +0200
Subject: [PATCH 54/54] Code formatting

---
 Iris/Iris/ProofMode/Tactics/Induction.lean | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 97cf03a58..0426e7b84 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -198,7 +198,8 @@ private def checkCtors (ctors altCtors : List Name) : ProofModeM Unit := do
     altCtors.filter (not <| ctors.any <| fun ctor => matchesCtorName ctor ·)
 
   -- Check for duplicate constructor names
-  let dupAltCtors := (altCtors.filter (fun alt => altCtors.countP (fun alt' => matchesCtorName alt alt') > 1)).eraseDupsBy matchesCtorName
+  let dupAltCtors := (altCtors.filter <|
+    fun alt => altCtors.countP (matchesCtorName alt ·) > 1).eraseDupsBy matchesCtorName
 
   if !missingAltCtors.isEmpty then
     let missing := ", ".intercalate  <| missingAltCtors.map (s!"`{·}`")
@@ -233,7 +234,8 @@ private def checkCtors (ctors altCtors : List Name) : ProofModeM Unit := do
 -/
 private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
-    (parsedAlts : Option <| Array <| Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (parsedAlts : Option <| Array <|
+      Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq)
     (altRecName : Option Name)
     (genSelTargets : Option <| List SelTarget) :
     ProofModeM Q($e ⊢ $goal) := do
@@ -424,7 +426,8 @@ elab "iinduction" colGt x:term "using" r:ident : tactic => do
     mvar.assign pf
 
 /-- Tactic with the recursor name and alternative names supplied by the user. -/
-elab "iinduction" colGt x:term "using" r:ident "with" alts:(colGe inductionAlts)* : tactic => do
+elab "iinduction" colGt x:term "using" r:ident
+    "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
@@ -447,7 +450,8 @@ elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ : tacti
     let pf ← iInductionCore hyps goal fvar none none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
+elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+
+    "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← termToFVar x
 
   -- Parse the list of alternative names supplied by the user
@@ -461,7 +465,8 @@ elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ "with"
     let pf ← iInductionCore hyps goal fvar parsedAlts none genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:term "using" r:ident "generalizing" genSelPats:(colGt selPat)+ : tactic => do
+elab "iinduction" colGt x:term "using" r:ident
+    "generalizing" genSelPats:(colGt selPat)+ : tactic => do
   let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user
@@ -475,7 +480,8 @@ elab "iinduction" colGt x:term "using" r:ident "generalizing" genSelPats:(colGt
     let pf ← iInductionCore hyps goal fvar none recName genSelTargets
     mvar.assign pf
 
-elab "iinduction" colGt x:term "using" r:ident "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
+elab "iinduction" colGt x:term "using" r:ident
+    "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
   let fvar ← termToFVar x
 
   -- Parse the recursor name provided by the user