feat: add option tactic.customEliminators to be able to turn off custom eliminators for induction and cases

RELEASES.md

@@ -65,6 +65,14 @@ v4.8.0 (development in progress)
   to enable pretty printing function applications using generalized field notation (defaults to true).
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
+* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
+  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
+  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
+  rather than `Nat.zero` and `Nat.succ n`.
+  Added option `tactic.customEliminators` to control whether to use custom eliminators.
+  [#3629](https://github.com/leanprover/lean4/pull/3629) and
+  [#3655](https://github.com/leanprover/lean4/pull/3655).
+
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:

src/Lean/Elab/Tactic/Induction.lean

@@ -533,11 +533,19 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
     else
       return e
 
+register_builtin_option tactic.customEliminators : Bool := {
+  defValue := true
+  group    := "tactic"
+  descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
+    defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
+}
+
 -- `optElimId` is of the form `("using" term)?`
 private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
   if optElimId.isNone then
-    if let some elimName ← getCustomEliminator? targets induction then
-      return ← getElimInfo elimName
+    if tactic.customEliminators.get (← getOptions) then
+      if let some elimName ← getCustomEliminator? targets induction then
+        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]!

tests/lean/run/customEliminators.lean

@@ -0,0 +1,48 @@
+/-!
+# Tests for the custom eliminators feature for `induction` and `cases`
+-/
+
+/-!
+Test the built-in custom `Nat` eliminator.
+-/
+/--
+error: unsolved goals
+case zero
+P : Nat → Prop
+⊢ P 0
+
+case succ
+P : Nat → Prop
+n✝ : Nat
+a✝ : P n✝
+⊢ P (n✝ + 1)
+-/
+#guard_msgs in
+example (P : Nat → Prop) : P n := by
+  induction n
+  done
+
+/-!
+Turn off the built-in custom `Nat` eliminator.
+-/
+section
+set_option tactic.customEliminators false
+
+/--
+error: unsolved goals
+case zero
+P : Nat → Prop
+⊢ P Nat.zero
+
+case succ
+P : Nat → Prop
+n✝ : Nat
+n_ih✝ : P n✝
+⊢ P n✝.succ
+-/
+#guard_msgs in
+example (P : Nat → Prop) : P n := by
+  induction n
+  done
+
+end