default induction

Stream: mathlib4

[Yury G. Kudryashov]

Can we teach Lean 4 to do induction on Nat (in induction tactic) using 0 and n + 1 instead of Nat.zero and Nat.succ?

[Kevin Buzzard]

Isn't a custom induction lemma the way to do this (and then induction using lemma)?

[Eric Wieser]

I think there is a way to set a default induction principle now too?

[Kevin Buzzard]

That would be really nice. In NNG I had to hack Lean's induction tactic to make it use the right zero (mynat.zero v has_zero.zero)

[Reid Barton]

Is there any update on this? It would be very nice for WithTop as well.
As a bonus: The "Generate a recursive function..." code action should also generate the correct pattern match syntax for the type...

[Mario Carneiro]

I was thinking about using the registered delaborators in the code action, which will fix pattern matches on [] / x :: xs, but not 0 / n + 1

[Eric Wieser]

Unless I was imagining things, I think it turns out that in Lean 3 we had this all along by just naming the recursor rec; though that only worked for type aliases.

[Kyle Miller]

@Reid Barton There's an @[eliminator] attribute: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructor.20is.20the.20new.20split/near/346658539

I tried experimenting with it again recently and thought I ran into some error with some hypotheses not being generalized correctly when using this feature, but I don't think I have the example anymore.

[Reid Barton]

By the way, is the intention for rcases also to use the default induction tactic for the type it's analyzing?

[Reid Barton]

rcases/rintro

[Yury G. Kudryashov]

Should I try to add

@[eliminator]
def Nat.rec' {α : ℕ → Sort _} (zero : α 0) (step : ∀ n, α n → α (n + 1)) (n : ℕ) : α n :=
  Nat.rec zero step n

and see how it works?

[Yury G. Kudryashov]

If yes, how should I name the assumptions? zero/step, zero/succ, base/step?

[Mario Carneiro]

I'm pretty skeptical of custom eliminators, they were pretty buggy in lean 3

[Mario Carneiro]

zero/succ

[Mario Carneiro]

otherwise lots of things will break

[Yury G. Kudryashov]

We can't know if they work in Lean 4 unless we try.

[Mario Carneiro]

I'm sure lots of things will still break if you put this in an early file, since the proofs will be assuming to see succ and not n+1

[Mario Carneiro]

I'm expecting to see >200 files touched by this refactor

[Yury G. Kudryashov]

At least, I'll need to remove lots of rw [Nat.zero_eq]

[Mario Carneiro]

Mario Carneiro said:

zero/succ

Another reason for this naming is that you won't get hovers on the cases otherwise

[Eric Wieser]

Mario Carneiro said:

I'm pretty skeptical of custom eliminators, they were pretty buggy in lean 3

They work reliably in lean 4 via induction using

[Mario Carneiro]

in particular I am concerned about (1) the eliminator not looking sufficiently eliminator-like for some code path, (2) the type being eliminated not actually being an inductive or not having the same constructors and code assuming that it is basically the same as the eliminator

[Mario Carneiro]

there is still quite a lot baked into the language regarding handling of inductive types

[Mario Carneiro]

we are a long way from "view patterns"

[Mario Carneiro]

re: rcases, I don't know. rcases just calls the internal cases method so you should be able to see whether it does anything with default eliminators

[Yury G. Kudryashov]

I just want to call induction n and see 0 (not Nat.zero) and n + 1.

[Yury G. Kudryashov]

Or it can break other tactics?

[Mario Carneiro]

Yury G. Kudryashov said:

Or it can break other tactics?

That is what I'm saying. Even if cases and induction themselves work, a lot of things assume that they work in a particular way, and generally only think about inductive types

[Mario Carneiro]

but like you said, the only way to be sure is to try it and find out

[Kyle Miller]

It looks like @[eliminator] might only really affect induction and cases directly

[Mario Carneiro]

at the very least, linters and code actions have to be aware of it

[Kyle Miller]

rcases/rintro use the Lean.MVarId.cases function, which appears not to look at @[eliminator] unless it's not obviously an inductive type

[Kyle Miller]

@Mario Carneiro Everything you're saying seems like an argument to try this out, since anything that breaks is something that should be fixed, and now we have a better shot at fixing these things in Lean 4

[Mario Carneiro]

heck, you can even use @[eliminator] also to do multi-target inductions. I have no idea how this is supposed to be used in practice and I'm sure everything will break

[Mario Carneiro]

match is, as far as I am aware, completely ignorant of @[eliminator]

[Mario Carneiro]

which is unfortunate since that's really where you want to do view-pattern-like things

[Mario Carneiro]

the difficulty level there is higher since you have to do exhaustiveness checking too

[Eric Wieser]

What's languages do have "view patterns"?

[Mario Carneiro]

haskell and scala come to mind

[Sebastian Ullrich]

A lovely paper by my former colleague on how complicated things get in Haskell: https://pp.ipd.kit.edu/uploads/publikationen/graf20lyg.pdf (also has a Lean 3 formalization)

[Eric Wieser]

I had naively assumed that Lean would have prepared me for Haskell's type theory, but then saw

The inhabitants of the type Maybe Void are ⊥, Nothing, and (Just ⊥)

which is two more elements than Option Empty has in Lean!

[Jireh Loreaux]

Yeah, in Haskell every type is inhabited by \bot, which is ... special:joy:

[François G. Dorais]

Mario's suspicions are partly right: the eliminator works fine for induction but it doesn't work perfectly well with cases. For example:

@[eliminator] 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) : 0 + n = n := by
  induction n with
  | zero =>
    -- ⊢ 0 + 0 = 0
    rfl
  | succ n ih =>
    -- n: Nat
    -- ih: 0 + n = n
    -- ⊢ 0 + (n + 1) = n + 1
    rw [←Nat.add_assoc, ih]

example (n : Nat) : 1 - n ≤ 1 := by
  cases n with
  | zero =>
    -- ⊢ 1 - 0 = 0
    exact Nat.le_refl ..
  | succ n =>
    -- n: Nat
    -- a✝: n + 1 = n → 1 - (n + 1) ≤ 1 -- what!?
    -- ⊢ 1 + (n + 1) ≤ 1
    rw [Nat.succ_sub_succ, Nat.zero_sub]
    exact Nat.zero_le ..

Personally, I still use the eliminator attribute. However, mostly locally. One use case that I find convenient is 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
  | x, 0 => left x
  | 0, y => right y
  | x + 1, y + 1 => succ_succ x y <| Nat.recDiag zero_zero succ_zero zero_succ succ_succ x y
where
  left
  | 0 => zero_zero
  | x+1 => succ_zero x (left x)
  right
  | 0 => zero_zero
  | y+1 => zero_succ y (right y)

For example:

attribute [local eliminator] Nat.recDiag

example (x y : Nat) : y ≤ (y - x) + x := by
  induction x, y with
  | zero_zero => exact Nat.zero_le ..
  | succ_zero x => exact Nat.zero_le ..
  | zero_succ y => exact Nat.le_refl ..
  | succ_succ x y ih =>
    rw [Nat.succ_sub_succ]
    apply Nat.succ_le_succ
    exact ih

Admittedly, for just one or two proofs, it's better to use induction x, y using Nat.recDiag with...

[Scott Morrison]

Just cross-referencing everthing: this will need modification in core to get anywhere, but there is a mathlib4 branch where you can see this in action at #5562.

[Patrick Massot]

Are there any news about this? I'm teaching induction today and I realized too late that it is still a mess. It would be really really nice to fix this.