fix: let induction handle parameters (#3256)

The induction principle used by `induction` may have explicit parameters
that are
not motive, target or “real” alternatives (that have the `motive` as
conclusion), e.g. restrictions on the `motive` or other parameters.

Previously, `induction` would treat them as normal alternatives, and try
to re-introduce the automatically reverted hypotheses. But this only
works when the `motive` is actually the conclusion in the type of that
alternative.

We now pay attention to that, thread that information through, and only
revert when needed.

Fixes #3212.

src/Lean/Elab/Tactic/Induction.lean

@@ -79,11 +79,7 @@ namespace ElimApp
 structure Alt where
   /-- The short name of the alternative, used in `| foo =>` cases -/
   name      : Name
-  /-- A declaration corresponding to the inductive constructor.
-  (For custom recursors, the alternatives correspond to parameter names in the
-  recursor, so we may not have a declaration to point to.)
-  This is used for go-to-definition on the alternative name. -/
-  declName? : Option Name
+  info      : ElimAltInfo
   /-- The subgoal metavariable for the alternative. -/
   mvarId    : MVarId
   deriving Inhabited
@@ -163,8 +159,8 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
           let arg ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
           let x   ← getBindingName
           modify fun s =>
-            let declName? := elimInfo.altsInfo[s.alts.size]!.declName?
-            { s with alts := s.alts.push ⟨x, declName?, arg.mvarId!⟩ }
+            let info := elimInfo.altsInfo[s.alts.size]!
+            { s with alts := s.alts.push ⟨x, info, arg.mvarId!⟩ }
           addNewArg arg
       loop
     | _ =>
@@ -286,7 +282,7 @@ where
     let mut usedWildcard := false
     let mut subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here
     let mut altsSyntax := altsSyntax
-    for { name := altName, declName?, mvarId := altMVarId } in alts do
+    for { name := altName, info, mvarId := altMVarId } in alts do
       let numFields ← getAltNumFields elimInfo altName
       let mut isWildcard := false
       let altStx? ←
@@ -307,7 +303,11 @@ where
         match (← Cases.unifyEqs? numEqs altMVarId {}) with
         | none   => pure () -- alternative is not reachable
         | some (altMVarId', subst) =>
-          (_, altMVarId) ← altMVarId'.introNP numGeneralized
+          altMVarId ← if info.provesMotive then
+            (_, altMVarId) ← altMVarId'.introNP numGeneralized
+            pure altMVarId
+          else
+            pure altMVarId'
           for fvarId in toClear do
             altMVarId ← altMVarId.tryClear fvarId
           altMVarId.withContext do
@@ -333,7 +333,7 @@ where
           -- inside tacticInfo for the current alternative (in `evalAlt`)
           let addInfo : TermElabM Unit := do
             if (← getInfoState).enabled then
-              if let some declName := declName? then
+              if let some declName := info.declName? then
                 addConstInfo (getAltNameStx altStx) declName
               saveAltVarsInfo altMVarId altStx fvarIds
           let unusedAlt := do
@@ -345,7 +345,11 @@ where
           match (← Cases.unifyEqs? numEqs altMVarId {}) with
           | none => unusedAlt
           | some (altMVarId', subst) =>
-            (_, altMVarId) ← altMVarId'.introNP numGeneralized
+            altMVarId ← if info.provesMotive then
+              (_, altMVarId) ← altMVarId'.introNP numGeneralized
+              pure altMVarId
+            else
+              pure altMVarId'
             for fvarId in toClear do
               altMVarId ← altMVarId.tryClear fvarId
             altMVarId.withContext do

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -11,8 +11,15 @@ namespace Lean.Meta
 
 structure ElimAltInfo where
   name      : Name
+  /-- A declaration corresponding to the inductive constructor.
+  (For custom recursors, the alternatives correspond to parameter names in the
+  recursor, so we may not have a declaration to point to.)
+  This is used for go-to-definition on the alternative name. -/
   declName? : Option Name
   numFields : Nat
+  /-- If `provesMotive := true`, then this alternative has `motive` as its conclusion.
+  Only for those alternatives the `induction` tactic should introduce reverted hypotheses.  -/
+  provesMotive : Bool
   deriving Repr, Inhabited
 
 /--
@@ -56,13 +63,14 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
-          let numFields ← forallTelescopeReducing xDecl.type fun args _ => pure args.size
+          let (numFields, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
+            pure (args.size, concl.getAppFn == motive)
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?
             let altDeclName := base ++ name
             if env.contains altDeclName then some altDeclName else none
-          altsInfo := altsInfo.push { name, declName?, numFields }
+          altsInfo := altsInfo.push { name, declName?, numFields, provesMotive }
     pure { elimExpr, elimType,  motivePos, targetsPos, altsInfo }
 
 def getElimInfo (elimName : Name) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do

tests/lean/run/issue3212.lean

@@ -0,0 +1,60 @@
+namespace SillyParam
+
+set_option linter.unusedVariables false in
+theorem nat_rec_with_string (some_param : String) {motive : Nat → Prop}
+  (zero : motive .zero) (succ : ∀ n, motive n → motive (.succ n)) : ∀ n, motive n :=
+  @Nat.rec motive zero succ
+
+example (n m : Nat) (h : n ≠ zero) : Nat.add m n ≠ zero := by
+  induction n using nat_rec_with_string
+  case some_param =>
+    show String
+    exact "heh"
+  case zero => sorry
+  case succ => sorry
+
+end SillyParam
+
+namespace RestrictedMotive
+
+axiom Restriction : (Nat → Prop) → Prop
+
+axiom restricted_induction {motive : Nat → Prop} (h : Restriction motive)
+  (zero : motive .zero) (succ : ∀ n, motive n → motive (.succ n)) : ∀ n, motive n
+
+example (n m : Nat) (h : n ≠ zero) : Nat.add m n ≠ zero := by
+  induction n using restricted_induction
+  case h =>
+    show Restriction _
+    sorry
+  case zero => sorry
+  case succ => sorry
+
+end RestrictedMotive
+
+
+namespace DownInduction
+
+axiom down_induction {motive : Nat → Prop} (u : Nat) (x : Nat)
+  (le_u : x ≤ u) (start : motive u) (step : ∀ x, x < u → motive (x + 1) → motive x) : motive x
+
+example (n m : Nat) (h : m * m < 100) (h2 : n ≤ m) : n * n < 100 := by
+  induction n using down_induction
+  case u => exact m -- (could have used `using down_induction (u := m)` of course)
+  case le_u =>
+    -- This does not work as hoped for yet: `induction` will revert `h2`, because it mentions `n`,
+    -- but we’d like to keep it outside of the motive here.
+    sorry
+  case start => exact h
+  case step x hlt IH =>
+    have IH := IH hlt
+    sorry
+
+-- Unfortunately, this doesn’t work either:
+--  example (n m : Nat) (h : m * m < 100) (h2 : n ≤ m) : n * n < 100 := by
+--    induction n using down_induction (le_u := h2)
+-- because after this, the target `n` is no longer a universally qualified variable
+--
+-- This probably could be made to work with a bit more refactoring.
+
+end DownInduction