Why shouldn't I use induction'?

Stream: CSLib

[Ching-Tsun Chou]

After rebasing on the current main of cslib (commt 4c176f), Lean is now telling me:

The induction' tactic is discouraged: please strongly consider using induction instead.
Note: This linter can be disabled with set_option linter.style.induction false

Why? Is this specific to cslib, or generally applicable to mathlib as well?

[Shreyas Srinivas]

induction’ uses lean 3 syntax and probably won’t get any new features that the induction tactic will.

[Shreyas Srinivas]

It already comes with a code action

[Shreyas Srinivas]

Technically a deprecation notice could mean that the respective maintainers may choose to remove it in future releases

[Ching-Tsun Chou]

It is used in #mil!

[Ching-Tsun Chou]

Also, I didn't get this warning yesterday (or ever, for that matter). What changed in cslib or mathlib since yesterday?

[Chris Henson]

This is a linter from mathlibStandardSet. You are seeing it now because we just moved to the new Lean release. This is a recent linter that has been added after the last uses of induction' were removed from Mathlib. I would expect MIL to eventually follow suit.

[Ching-Tsun Chou]

I see. Thanks!

[Ching-Tsun Chou]

I really don't like the syntax of induction.

[Eric Wieser]

Is induction n with | foo x | bar y z really worse than induction' n with x y z?

[Eric Wieser]

Remember that there is more than one syntax you can use for induction, you don't have to use the one with =>s

[Ching-Tsun Chou]

Can you point me to an example of that syntax in mathlib or somewhere else? All I have is #tpil, which doesn't seem to have an example.

[Malvin Gattinger]

Maybe Eric has better explanations, but I thought induction _ using blabla is only for using specific induction principles and with should be used to write | foo x | bar y z afterwards? :thinking:
Anyway, running rg "induction n using" or rg "induction n with" in mathlib brings up many examples. Here is for example

private theorem abs_geomSum_le [IsOrderedRing α] : |geomSum a b n| ≤ (n + 1) * max |a| |b| ^ n := by
  induction n with | zero => simp [geomSum] | succ n ih => ?_
  ...

And here is this example:

theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0 := by
  induction n using Nat.binaryRec with | zero => rfl | bit b n hn => ?_
  ...

[Ching-Tsun Chou]

The fact that you have to write zero and succ and => is precisely what I don't like about the syntax of induction.

[Shreyas Srinivas]

I prefer this syntax precisely for this reason. You get properly named cases usually corresponding to the constructors of the type

[Ching-Tsun Chou]

This may make sense for user-defined inductive types. But does everyone really care about the fact that the natural numbers are inductively defined in Lean using constructors named "zero" and "succ" (rather than some other names)? With induction' you can do inductive proofs on Nat without ever noticing that.

[Shreyas Srinivas]

To answer your question, unironically yes. Tracking induction arms is very useful when we are dealing with induction proofs on larger inductive types. It also makes the proof script readable. And fwiw, this debate appears to have reached a settlement sometime ago. The new syntax is here to stay.