From ef4ab9c1d15942aed281838de34778cb6a66914d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Mar 2021 16:25:02 -0800
Subject: [PATCH] fix: report error if too many variable names have been
 provided at `induction/cases` alternative

---
 src/Lean/Elab/Tactic/Induction.lean                 | 2 ++
 tests/lean/run/tacticTests.lean                     | 2 +-
 tests/lean/tooManyVarsAtInduction.lean              | 9 +++++++++
 tests/lean/tooManyVarsAtInduction.lean.expected.out | 2 ++
 4 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/tooManyVarsAtInduction.lean
 create mode 100644 tests/lean/tooManyVarsAtInduction.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index b1fb4326af..8fa4e04a35 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -210,6 +210,8 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac :
     | some altStx =>
       subgoals ← withRef altStx do
         let altVarNames := getAltVarNames altStx
+        if altVarNames.size > numFields then
+          throwError! "too many variable names provided at alternative '{altName}', #{altVarNames.size} provided, but #{numFields} expected"
         let mut (_, altMVarId) ← introN altMVarId numFields altVarNames.toList (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
         match (← Cases.unifyEqs numEqs altMVarId {}) with
         | none   => throwError! "alternative '{altName}' is not needed"
diff --git a/tests/lean/run/tacticTests.lean b/tests/lean/run/tacticTests.lean
index be035acb77..196b419aa6 100644
--- a/tests/lean/run/tacticTests.lean
+++ b/tests/lean/run/tacticTests.lean
@@ -10,7 +10,7 @@ theorem ex1 (m : Nat) : Le m 0 → m = 0 := by
 theorem ex2 (m n : Nat) : Le m n → Le m.succ n.succ := by
   intro h
   induction h with
-  | base n => apply Le.base
+  | base => apply Le.base
   | succ n m ih =>
     apply Le.succ
     apply ih
diff --git a/tests/lean/tooManyVarsAtInduction.lean b/tests/lean/tooManyVarsAtInduction.lean
new file mode 100644
index 0000000000..0afd246731
--- /dev/null
+++ b/tests/lean/tooManyVarsAtInduction.lean
@@ -0,0 +1,9 @@
+theorem ex1 (n : Nat) : 0 + n = n := by
+  induction n with
+  | succ x ih₁ ih₂ ih₃ => admit
+  | zero => rfl
+
+theorem ex2 (n : Nat) : 0 + n = n := by
+  cases n with
+  | succ x ih => admit
+  | zero => rfl
diff --git a/tests/lean/tooManyVarsAtInduction.lean.expected.out b/tests/lean/tooManyVarsAtInduction.lean.expected.out
new file mode 100644
index 0000000000..8a67c4411c
--- /dev/null
+++ b/tests/lean/tooManyVarsAtInduction.lean.expected.out
@@ -0,0 +1,2 @@
+tooManyVarsAtInduction.lean:3:2-3:31: error: too many variable names provided at alternative 'succ', #4 provided, but #2 expected
+tooManyVarsAtInduction.lean:8:2-8:22: error: too many variable names provided at alternative 'succ', #2 provided, but #1 expected