From fa058ed2286460e6b7b6ab8aebbac76ec7741dc1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 28 Feb 2024 14:14:34 +0100
Subject: [PATCH] fix: include let bindings when determining altParamNums for
 eliminators (#3505)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Else the `case` will now allow introducing all necessary variables.

Induction principles with `let` in the types of the cases will be more
common with #3432.

This implementation no longer reduces the type as it goes, but really
only counts
manifest foralls and lets. I find this more sensible and predictable: If
you have
```
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) …
```
then previously, writing
```
case symm =>
```
would actually bring a fresh `x` and `y` and variable `h : P x y` into
scope and produce a
goal of `P y x`, because `Symmetric P` happens to be
```
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
```

After this change, after `case symm =>` will leave `Symmetric P` as the
goal.

This gives more control to the author of the induction hypothesis about
the actual
goal of the cases. This shows up in mathlib in two places; fixes in
https://github.com/leanprover-community/mathlib4/pull/11023.
I consider these improvements.
---
 src/Lean/Meta/Tactic/ElimInfo.lean | 12 ++++++++++--
 tests/lean/run/indUsingLet.lean    | 14 ++++++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/indUsingLet.lean

diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 9343a7ace2..e1b6ab2590 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -37,6 +37,15 @@ structure ElimInfo where
   altsInfo   : Array ElimAltInfo := #[]
   deriving Repr, Inhabited
 
+
+/-- Given the type `t` of an alternative, determines the number of parameters
+(.forall and .let)-bound, and whether the conclusion is a `motive`-application.  -/
+def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool
+  | .forallE _ _ b _ => altArity motive (n+1) b
+  | .letE _ _ _ b _ => altArity motive (n+1) b
+  | conclusion => (n, conclusion.getAppFn == motive)
+
+
 def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
   let elimType ← inferType elimExpr
   trace[Elab.induction] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}"
@@ -64,8 +73,7 @@ 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, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
-            pure (args.size, concl.getAppFn == motive)
+          let (numFields, provesMotive) := altArity motive 0 xDecl.type
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?
diff --git a/tests/lean/run/indUsingLet.lean b/tests/lean/run/indUsingLet.lean
new file mode 100644
index 0000000000..97056e9ba1
--- /dev/null
+++ b/tests/lean/run/indUsingLet.lean
@@ -0,0 +1,14 @@
+theorem some_induction
+  {motive : Nat → Prop}
+  (zero : motive 0)
+  (succ : forall n, 0 < n → let m := n - 1; motive m → motive n) :
+  ∀ n, motive n
+  | 0 => zero
+  | n+1 => succ (n+1) (Nat.zero_lt_succ n) (some_induction zero succ n)
+
+
+example (n : Nat) : n = n := by
+  induction n using some_induction
+  case zero => rfl
+  case succ n _h _m _IH =>
+    rfl