feat: explanations for cases applied to non-inductive types

This PR adds an explanation to the error message when `cases` and `induction` are applied to a term whose type is not an inductive type. For `Prop`, these tactics now suggest the `by_cases` tactic.

src/Lean/Elab/Tactic/Induction.lean

@@ -579,12 +579,27 @@ private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Un
           throwErrorAt alt "more than one wildcard alternative '| _ => ...' used"
         found := true
 
-def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
+def getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal :=
   liftMetaMAtMain fun mvarId => do
     let majorType ← inferType major
     let majorType ← whnf majorType
     matchConstInduct majorType.getAppFn
-      (fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
+      (fun _ => do
+        let tacticName := if induction then `induction else `cases
+        let mut hint := m!"\n\nExplanation: the '{tacticName}' tactic is for constructor-based reasoning, \
+          with cases exhausting every way in which a term could have been constructed."
+        if majorType.isProp then
+          hint := m!"{hint} \
+            The 'Prop' universe is not an inductive type however, so '{tacticName}' does not apply. \
+            Consider using the 'by_cases' tactic, which enables true/false reasoning."
+        else if majorType.isType then
+          hint := m!"{hint} \
+            Type universes are not inductive types however, so such case-based reasoning is not possible. \
+            This is a strong limitation. According to Lean's underlying theory, the only distinguishing \
+            feature of types is their cardinalities."
+        else
+          hint := m!"{hint} It can sometimes be helpful defining an equivalent auxiliary inductive type to apply '{tacticName}' to instead."
+        Meta.throwTacticEx tacticName mvarId m!"major premise type is not an inductive type{indentExpr majorType}{hint}")
       (fun val _ => pure val)
 
 /--
@@ -627,7 +642,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
         return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
-    let indVal ← getInductiveValFromMajor targets[0]!
+    let indVal ← getInductiveValFromMajor induction targets[0]!
     if induction && indVal.all.length != 1 then
       throwError "'induction' tactic does not support mutually inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives"
     if induction && indVal.isNested then

tests/lean/run/casesTactic.lean

@@ -0,0 +1,50 @@
+/-!
+# Tests of the 'cases' tactic
+-/
+
+/-!
+Error messages when not an inductive type.
+-/
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Prop
+
+Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
+in which a term could have been constructed. The 'Prop' universe is not an inductive type however,
+so 'cases' does not apply. Consider using the 'by_cases' tactic, which enables true/false reasoning.
+p : Prop
+⊢ True
+-/
+#guard_msgs in
+example (p : Prop) : True := by
+  cases p
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Type
+
+Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
+in which a term could have been constructed. Type universes are not inductive types however, so such
+case-based reasoning is not possible. This is a strong limitation. According to Lean's underlying
+theory, the only distinguishing feature of types is their cardinalities.
+α : Type
+⊢ True
+-/
+#guard_msgs in
+example (α : Type) : True := by
+  cases α
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Bool → Bool
+
+Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
+in which a term could have been constructed. It can sometimes be helpful defining an equivalent
+auxiliary inductive type to apply 'cases' to instead.
+f : Bool → Bool
+⊢ True
+-/
+#guard_msgs in
+example (f : Bool → Bool) : True := by
+  cases f