feat: better error message for invalid induction alternative name (#5888)

Closes #5887

src/Lean/Elab/Tactic/Induction.lean

@@ -208,15 +208,28 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N
 private def isWildcard (altStx : Syntax) : Bool :=
   getAltName altStx == `_
 
-private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
+private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do
+  let mut seenNames : Array Name := #[]
   for h : i in [:altsSyntax.size] do
     let altStx := altsSyntax[i]
     if getAltName altStx == `_ && i != altsSyntax.size - 1 then
       withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
     let altName := getAltName altStx
     if altName != `_ then
+      if seenNames.contains altName then
+        throwErrorAt altStx s!"duplicate alternative name '{altName}'"
+      seenNames := seenNames.push altName
       unless alts.any (·.name == altName) do
-        throwErrorAt altStx "invalid alternative name '{altName}'"
+        let unhandledAlts := alts.filter fun alt => !seenNames.contains alt.name
+        let msg :=
+          if unhandledAlts.isEmpty then
+            m!"invalid alternative name '{altName}', no unhandled alternatives"
+          else
+            let unhandledAltsMessages := unhandledAlts.map (m!"{·.name}")
+            let unhandledAlts := MessageData.orList unhandledAltsMessages.toList
+            m!"invalid alternative name '{altName}', expected {unhandledAlts}"
+        throwErrorAt altStx msg
+
 
 /-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
     return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can

src/Lean/Message.lean

@@ -279,6 +279,14 @@ def ofList : List MessageData → MessageData
 def ofArray (msgs : Array MessageData) : MessageData :=
   ofList msgs.toList
 
+/-- Puts `MessageData` into a comma-separated list with `"or"` at the back (no Oxford comma).
+Best used on non-empty lists; returns `"– none –"` for an empty list.  -/
+def orList (xs : List MessageData) : MessageData :=
+  match xs with
+  | [] => "– none –"
+  | [x] => "'" ++ x ++ "'"
+  | _ => joinSep (xs.dropLast.map (fun x => "'" ++ x ++ "'")) ", " ++ " or '" ++ xs.getLast! ++ "'"
+
 /-- Puts `MessageData` into a comma-separated list with `"and"` at the back (no Oxford comma).
 Best used on non-empty lists; returns `"– none –"` for an empty list.  -/
 def andList (xs : List MessageData) : MessageData :=

tests/lean/inductionErrors.lean.expected.out

@@ -25,7 +25,7 @@ y : Nat
 ⊢ 0 + (y + 1) = y + 1
 inductionErrors.lean:50:2-50:16: error: alternative 'cons' is not needed
 inductionErrors.lean:55:2-55:16: error: alternative 'cons' is not needed
-inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2'
+inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2', expected 'diag' or 'upper'
 inductionErrors.lean:66:2-66:28: error: invalid occurrence of wildcard alternative, it must be the last alternative
 inductionErrors.lean:74:2-74:34: error: unused alternative '_'
-inductionErrors.lean:80:2-80:56: error: unused alternative 'lower'
+inductionErrors.lean:80:2-80:56: error: duplicate alternative name 'lower'

tests/lean/run/inductionCheckAltNames.lean

@@ -0,0 +1,49 @@
+universe u
+
+axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
+  (diag  : (a : Nat) → motive a a)
+  (upper : (delta a : Nat) → motive a (a + delta.succ))
+  (lower : (delta a : Nat) → motive (a + delta.succ) a)
+  : motive y x
+
+/-- error: invalid alternative name 'lower2', expected 'diag', 'upper' or 'lower' -/
+#guard_msgs in
+theorem invalidAlt (p: Nat) : p ≤ q ∨ p > q := by
+  cases p, q using elimEx with
+  | lower2 /- error -/ d => apply Or.inl; admit
+  | upper d => apply Or.inr
+  | diag    => apply Or.inl; apply Nat.le_refl
+
+/-- error: invalid alternative name 'lower2', expected 'lower' -/
+#guard_msgs in
+theorem oneMissingAlt (p: Nat) : p ≤ q ∨ p > q := by
+  cases p, q using elimEx with
+  | upper d => apply Or.inl; admit
+  | diag    => apply Or.inl; apply Nat.le_refl
+  | lower2  /- error -/ => apply Or.inr
+
+/-- error: duplicate alternative name 'upper' -/
+#guard_msgs in
+theorem doubleAlt (p: Nat) : p ≤ q ∨ p > q := by
+  cases p, q using elimEx with
+  | upper d => apply Or.inl; admit
+  | upper d /- error -/  => apply Or.inr
+  | diag    => apply Or.inl; apply Nat.le_refl
+
+/-- error: invalid occurrence of wildcard alternative, it must be the last alternative -/
+#guard_msgs in
+theorem invalidWildCard (p: Nat) : p ≤ q ∨ p > q := by
+  cases p, q using elimEx with
+  | upper d => apply Or.inl; admit
+  | _ /- error -/  => apply Or.inr
+  | diag    => apply Or.inl; apply Nat.le_refl
+
+
+/-- error: invalid alternative name 'lower2', no unhandled alternatives -/
+#guard_msgs in
+theorem noAlt (p: Nat) : p ≤ q ∨ p > q := by
+  cases p, q using elimEx with
+  | upper d => apply Or.inl; admit
+  | lower  => apply Or.inr
+  | diag    => apply Or.inl; apply Nat.le_refl
+  | lower2  /- error -/ => apply Or.inr