feat: iinduction

Iris/Iris/HeapLang/Lib/Quicksort.lean

@@ -282,13 +282,12 @@ theorem quicksort_spec l ls Φ :
 theorem wp_makeList (l : List Int) (Φ : Val → IProp GF) :
     (∀ v, isList v l -∗ Φ v) -∗
     WP hl(&(makeList l)) {{ Φ }} := by
-  induction l generalizing Φ with
+  iintro HΦ
+  iinduction l generalizing %Φ HΦ with
   | nil =>
-    iintro HΦ
     unfold makeList
     iapply nil_spec $$ HΦ
   | cons l ls ih =>
-    iintro HΦ
     rw [makeList]
     wp_pures
     wp_bind &(makeList _)

Iris/Iris/Instances/Lib/FUpd.lean

@@ -170,28 +170,26 @@ theorem lc_fupd_add_later {E1 E2 : CoPset} {P : IProp GF} : ⊢ £ 1 -∗ (▷ |
 @[rocq_alias lc_fupd_add_laterN]
 theorem lc_fupd_add_laterN (n : Nat) {E : CoPset} {P : IProp GF} :
     ⊢ £ n -∗ (▷^[n] |={E}=> P) -∗ |={E}=> P := by
-  induction n generalizing P with
+  iintro Hf Hupd
+  iinduction n with
   | zero =>
-    iintro _ H
     simp [BIBase.laterN]
-    iexact H
+    iexact Hupd
   | succ n IH =>
-    iintro Hf Hupd
     icases Hf with ⟨H1, Hf⟩
     iapply lc_fupd_add_later $$ H1
     inext
     iapply IH $$ [$] [$]
 
-@[rocq_alias lc_fupd_add_step_fupdN ]
+@[rocq_alias lc_fupd_add_step_fupdN]
 theorem lc_fupd_add_step_fupdN (E1 E2 E3: CoPset) (P : IProp GF) (n : Nat) :
-  £ n -∗ (|={E1}[E2]▷=>^[n] |={E1,E3}=> P) -∗ |={E1,E3}=> P := by
-  induction n generalizing P with
+    £ n -∗ (|={E1}[E2]▷=>^[n] |={E1,E3}=> P) -∗ |={E1,E3}=> P := by
+  iintro Hf Hupd
+  iinduction n with
   | zero =>
-    iintro _ H
     simp only [Nat.repeat]
-    iexact H
+    iexact Hupd
   | succ n IH =>
-    iintro Hf Hupd
     simp only [Nat.repeat]
     imod Hupd
     icases Hf with ⟨H1, Hf⟩
@@ -404,12 +402,12 @@ instance elimModal_fupd_fupd_finally p (E1 E2 : CoPset) (P Q : IProp GF) :
 @[rocq_alias step_fupdN_fupd_finally]
 theorem step_fupdN_fupd_finally (E1 E2 : CoPset) (n : Nat) (P : IProp GF) :
     (|={E1}[E2]▷=>^[n] |={E1|}=> P) ⊢ |={E1|}=> ▷^[n] ◇ P := by
-  induction n with
+  iintro HP
+  iinduction n with
   | zero =>
     simp only [Nat.repeat]
     exact fupd_finally_mono except0_intro
   | succ n IH =>
-    iintro HP
     simp only [Nat.repeat]
     imod HP
     iapply fupd_finally_mono (later_laterN n).mpr

Iris/Iris/ProgramLogic/Lifting.lean

@@ -187,10 +187,9 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset)
     [Hexec : PureExec φ n e₁ e₂] (Hφ : φ) :
     (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by
   replace Hexec := Hexec.pureExec Hφ
-  induction Hexec using Relation.Iterate.head_induction_on with
+  iinduction Hexec using Relation.Iterate.head_induction_on with simp only [Nat.repeat]
   | rfl =>
     iintro Hwp
-    simp only [Nat.repeat]
     rw (occs := [2]) [fupd_wp_iff.to_eq]
     icases lc_zero with >Hz
     iapply Hwp $$ Hz
@@ -202,7 +201,6 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset)
       intro σ
       have _ : PrimStep.Reducible (e₁, σ) := by grind only [reducible_of_reducibleNoObs]
       grind [cases Stuckness]
-    simp only [Nat.repeat]
     iapply step_fupd_wand $$ Hwp
     iintro Hwp Hone
     iapply IH

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
 
@@ -224,6 +224,15 @@ 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"

Iris/Iris/ProofMode/Expr.lean

@@ -539,3 +539,21 @@ def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
   addHypInfo nameRef nameTo ivar' prop ty (isBinder := true)
   let hyps := Hyps.add bi nameTo ivar' p ty h
   return ⟨ivar', hyps⟩
+
+/--
+  Given hypothesis `hyps` representing `e` where every hypothesis exist in the
+  intuitionistic context, return the proof of `e ⊢ □ e`. Return `none` if
+  `hyps` contains hypotheses in the spatial context.
+-/
+def Hyps.buildIntuitionisticProof {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : Option Q($e ⊢ □ $e) :=
+  match hyps with
+  | .emp _ => some q(intuitionistically_emp.mpr)
+  | .hyp _ _ _ p _ _ =>
+    match matchBool p with
+    | .inl _ => some q(intuitionistically_idem.mpr)
+    | .inr _ => none
+  | .sep _ _ _ _ lhs rhs => do
+    let pfL ← buildIntuitionisticProof lhs
+    let pfR ← buildIntuitionisticProof rhs
+    some q((sep_mono $pfL $pfR).trans intuitionistically_sep_mpr)

Iris/Iris/ProofMode/Instances.lean

@@ -7,7 +7,9 @@ module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
 public import Iris.ProofMode.ModalityInstances
+public import Iris.ProofMode.Expr
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
 
@@ -918,3 +920,49 @@ 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_mpr.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias into_ih_entails]
+instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (Entails' P Q) P Q where
+  into_ih := λ hpq => intuitionistically_elim.trans hpq
+
+@[rocq_alias into_ih_forall]
+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
+    intro hφ
+    apply forall_intro
+    intro x
+    exact (h x).into_ih (hφ x)
+
+@[rocq_alias into_ih_impl]
+instance (priority := default - 1) 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_right h1.make_affinely.mpr).trans ?_
+    refine persistent_and_affinely_sep_right.2.trans ?_
+    exact pure_elim_right (fun hφ => h2.into_ih (hImp hφ))
+
+#rocq_ignore into_ih_Forall "List.Forall does not exist in the core Lean libraries, and ∀ x ∈ l, p x is used instead"
+
+/-- 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 (priority := default - 2) 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 := 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_intuitionistically ((h _ _).into_ih x)
+      · exact ih

Iris/Iris/ProofMode/Porting.lean

@@ -51,7 +51,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iCombine" ported "icombine"
 #rocq_concept proofmode "Tactics" "iIntros (basic)" ported "iintro"
 #rocq_concept proofmode "Tactics" "iIntros (all intro patterns)" missing ""
-#rocq_concept proofmode "Tactics" "iInduction" missing ""
+#rocq_concept proofmode "Tactics" "iInduction" ported "iinduction"
 #rocq_concept proofmode "Tactics" "iLöb" ported "iloeb"
 #rocq_concept proofmode "Tactics" "iAssert" ported "ihave _ : _"
 #rocq_concept proofmode "Tactics" "iRewrite" ported "irewrite"

Iris/Iris/ProofMode/ProofModeM.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang
+Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -96,6 +96,30 @@ def addMVarGoal (m : MVarId) (name : Name := .anonymous) : ProofModeM Unit := do
     m.setUserName name
   modify ({goals := ·.goals.push m})
 
+/--
+  Creates a new proof goal with the given hypotheses (`hyps`), conclusion
+  (`goal`). Run a sequence of tactics with this proof goal and push all
+  subgoals into the proof state.
+
+  The function returns:
+  1. the metavariable of the initial goal,
+  2. a Boolean value indicating whether the `firstTactic` solves all goals,
+     `false` if `firstTactic` is `none`.
+-/
+def addBIGoalRunTactics {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {e} (hyps : Hyps bi e) (goal : Q($prop)) (name : Name := .anonymous)
+    (firstTactic : Option <| TSyntax `tactic)
+    (tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq) :
+    ProofModeM (Q($e ⊢ $goal) × Bool) := do
+  let m ← mkBIGoal hyps goal name
+  -- Run `firstTactic`, if available
+  let subgoals ← firstTactic.elim (pure [m.mvarId!]) (evalTacticAt · m.mvarId!)
+  -- Run the user tactics on each newly generated goal after running `firstTactic`
+  let mut subgoals' := []
+  for s in subgoals do
+    subgoals' := subgoals'.append <| ← evalTacticAt tacticSeq s
+  pure (m, firstTactic.isSome && subgoals.isEmpty)
+
 /-- Try to synthesize a typeclass instance, adding any created metavariables as proof mode goals. -/
 def ProofModeM.trySynthInstanceQ (α : Q(Sort v)) : ProofModeM (Option Q($α)) := do
   let LOption.some (e, mvars) ← ProofMode.trySynthInstance α | return none

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