Deprecation and Replacement of `induction'`?

Stream: mathlib4

[Pietro Monticone]

I'd like to start a discussion about the possible deprecation of the tactic induction' and its replacement with induction in Mathlib.

Recently, I submitted a few PRs to replace usages of the tactic induction' with induction (with the plan of automating it via lake exe refactor in the medium term). The motivation behind this change was based on information I received from a few maintainers who suggested that induction' is soon to be deprecated and that induction should be used in all cases going forward (but of course I might have misunderstood completely). Moreover, in my experience with several PRs, reviewers have consistently recommended using induction over induction', leading me to believe that this was the preferred practice and possibly the direction Mathlib was heading.

However, during the review process of my latest PR, it was pointed out by @Yaël Dillies that there might not be a consensus or a concrete plan to deprecate induction'.

This raises a few questions in my opinion:

1. Is there an official plan or ongoing discussion to deprecate induction' in favour of induction?
2. Are there specific situations or cases where induction' is to be preferred or necessary over induction?
3. More basically, what are the key differences between induction and induction', and why might one be favoured over the other in practice?

[Heather Macbeth]

Controversial opinion: if we require induction in Mathlib, we should also change the standard recursor so that the case names are math-idiomatic:

import Mathlib

/-- Alternative recursor for `Nat` with idiomatic case names. -/
@[elab_as_elim, induction_eliminator]
abbrev Nat.recPretty {motive : Nat → Sort*} (baseCase : motive 0)
    (inductiveStep : (n : Nat) → motive n → motive (n + 1)) (t : Nat) : motive t :=
  Nat.rec baseCase inductiveStep t

example (n : ℕ) : (3:ℤ) ∣ 4 ^ n - 1 := by
  induction n with
  | baseCase => decide
  | inductiveStep k IH =>
    obtain ⟨a, ha⟩ := IH
    use 4 * a + 1
    linear_combination 4 * ha

[Heather Macbeth]

(But more seriously, I think there is probably no consensus on this, and no harm in allowing for author preference.)

[Patrick Massot]

I would understand this request if we were stuck with n.succ, but this is no longer true. So I don’t quite understand. In a teaching context I would understand.

[Patrick Massot]

I think we should switch to induction. As far as I know, the natural number case is the only one were induction' is not clearly worse, and consistency is nice.

[Ruben Van de Velde]

I prefer induction, certainly for new code, less strongly for large-scale refactors (because those are fairly disruptive)

[Jeremy Tan]

In #16198 I replace induction' and cases' in files that directly import Tactic.Cases so that that import may be removed. (Thus a file in the main folder, if it imports Tactic.Cases, now does so transitively by Tactic.Common)

[Matthew Ballard]

Is core willing to absorb induction'? My worry is something breaks it at some point and creates a significant burden on whomever has to fix it. The ergonomics seems within tolerance now.

[Mario Carneiro]

I would love it if we could get induction' to support a more rcases-like syntax, with | and possibly \<\>. I think that's the prinicpal readability issue with it, and making that modification wouldn't block its usage in NNG et al.

[Jeremy Tan]

There are 3672 uses of induction' and cases' throughout the repository. It is feasible that we can replace them all with induction/cases/rcases/obtain

[Jeremy Tan]

Jeremy Tan said:

There are 3672 uses of induction' and cases' throughout the repository

Regarding these uses: 60 are in my PR #16198, 75 are in my PR #16189 and 41 are in Pietro's PR #16182. I have more removals stashed locally

[Ruben Van de Velde]

I'm surprised that we seem to be replacing induction' in dozens of files at a time without reaching a conclusion in this thread

[Kim Morrison]

Here's my attempt at summarising

• it would be nice to have a variant of induction' that supports rcases-like syntax, but no one is actively working on this.
• there is some concern about the maintainability of induction'
• there doesn't seem to be an urgent need to get rid of induction' or cases'
• but there is little to no downside if someone wants to go to the effort of replacing them locally

[Jeremy Tan]

image.png
:idea:

[Kyle Miller]

(Just joining this thread) One feature I noticed that induction' has that induction doesn't is induction' h : x syntax, which is useful if x isn't just a local variable. I think induction could support this syntax, so if refactoring is continuing, please be sure not to eliminate induction' h : x.

[Jeremy Tan]

My open PRs relating to this: #16451, #16250, #16470