feat: induction tactic to err on extra targets (#7224)

This PR make `induction … using` and `cases … using` complain if more
targets were given than expected by that eliminator.

src/Lean/Elab/Tactic/Induction.lean

@@ -173,6 +173,10 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
           addNewArg arg
       loop
     | _ =>
+      let s ← get
+      let ctx ← read
+      unless s.targetPos = ctx.targets.size do
+        throwError "unexpected number of targets for '{elimInfo.elimExpr}'"
       pure ()
   let (_, s) ← (loop).run { elimInfo := elimInfo, targets := targets }
     |>.run { f := elimInfo.elimExpr, fType := elimInfo.elimType, motive := none }

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -120,6 +120,8 @@ where
       else
         collect (b.instantiate1 (← mkFreshExprMVar d)) (argIdx+1) targetIdx implicits targets'
     | _ =>
+      unless targetIdx = targets.size do
+        throwError "extra targets for '{elimInfo.elimExpr}'"
       return (implicits, targets')
 
 structure CustomEliminator where

src/Std/Data/DTreeMap/Internal/Balancing.lean

@@ -763,13 +763,13 @@ theorem balance_eq_inner [Ord α] {sz k v} {l r : Impl α β}
     balance k v l r hl.left hl.right h = inner sz k v l r := by
   rw [balance_eq_balance!, balance!_eq_balanceₘ hl.left hl.right h, balanceₘ]
   have hl' := balanced_inner_iff.mp hl
-  cases k, v, l, r, hl.left, hl.right, h using balanceₘ.fun_cases <;> tree_tac
+  fun_cases balanceₘ k v l r <;> tree_tac
 
 theorem balance!_desc {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     (balance! k v l r).size = l.size + 1 + r.size ∧ (balance! k v l r).Balanced := by
   rw [balance!_eq_balanceₘ hlb hrb hlr, balanceₘ]
-  cases k, v, l, r, hlb, hrb, hlr using balanceₘ.fun_cases
+  fun_cases balanceₘ k v l r
   · rw [if_pos ‹_›, bin, balanced_inner_iff]
     exact ⟨rfl, hlb, hrb, Or.inl ‹_›, rfl⟩
   · rw [if_neg ‹_›, dif_pos ‹_›]

tests/lean/run/casesUsing.lean

@@ -17,6 +17,16 @@ theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
   | lower d => apply Or.inl; show p ≤ p + d.succ; admit
   | upper d => apply Or.inr; show q + d.succ > q; admit
 
+/-- error: insufficient number of targets for 'elimEx' -/
+#guard_msgs in
+theorem ex1' (p q : Nat) : p ≤ q ∨ p > q := by
+  cases p using elimEx
+
+/-- error: extra targets for 'elimEx' -/
+#guard_msgs in
+theorem ex1'' (p q : Nat) : p ≤ q ∨ p > q := by
+  cases p, q, p using elimEx
+
 theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx
   case lower => admit

tests/lean/run/grind_constProp.lean

@@ -211,7 +211,7 @@ example (e : Expr) : e.simplify.eval σ = e.eval σ := by
   try? (max := 1)
 
 @[simp, grind =] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by
-  induction e, σ using Expr.simplify.induct <;> grind
+  induction e using Expr.simplify.induct <;> grind
 
 @[simp, grind =] def Stmt.simplify : Stmt → Stmt
   | skip => skip