Custom default recursors?

Stream: lean4

[François G. Dorais]

When declaring an inductive type the recursor generated by Lean doesn't use common notation. Indeed, these always come after the inductive definition. For example, with Nat, the induction tactic does this:

example (n : Nat) : n + 1 - 1 = n := by
  induction n with
  | zero => sorry -- goal: Nat.zero + 1 - 1 = Nat.zero
  | succ n ih => sorry -- goal: Nat.succ n + 1 - 1 = Nat.succ n

In such cases, I add a custom recursor like this:

protected def Nat.recAux.{u} {motive : Nat → Sort u} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n+1)) : (t : Nat) → motive t
| 0 => zero
| n+1 => succ n (Nat.recAux zero succ n)

example (n : Nat) : n + 1 - 1 = n := by
  induction n using Nat.recAux with
  | zero => sorry -- goal: 0 + 1 - 1 = 0
  | succ n ih => sorry -- goal: n + 1 + 1 - 1 = n + 1

Once recAux and friends are available, there is not much further uses for the original rec. It would be nice to be able to customize the default recursor to so we can use recAux without specifying induction ... using .... (The original recursor would still be available by using the original recursor.) The main drawback is that the exact form of rec can be deduced from the inductive definition but this is not true for custom default recursors.

It would also be nice to be able to specify default recursors to use for double induction. For example, I often use this diagonal recursor:

protected def Nat.recDiag.{u} {motive : Nat → Nat → Sort u}
  (zero_zero : motive 0 0)
  (succ_zero : (x : Nat) → motive x 0 → motive (x + 1) 0)
  (zero_succ : (y : Nat) → motive 0 y → motive 0 (y + 1))
  (succ_succ : (x y : Nat) → motive x y → motive (x + 1) (y + 1)) :
  (x y : Nat) → motive x y := sorry

It doesn't necessarily make sense to make this a global default for double induction, but it would be useful as a local default in some cases.

All these examples are about Nat but there are other use cases.

So, I ask:

• Is this something that other people would use?
• Would this be easy or hard to implement?

[Eric Wieser]

Another place this comes up is for cases when a definition is changed to something equivalent but with a different built in recursor (eg consider someone changing int to be the quotient definition that Kevin talks about); it would be nice to be able to provide a custom recursor equivalent to the old one, and make it the default so that downstream inductions don't break