induction with 0 instead of Nat.zero

Stream: general

[Johan Commelin]

Can someone remind me: what do we need to do so that induction n will use 0 and ?n + 1 instead of Nat.zero and Nat.succ ?n by default in mathlib?
This has been discussed several times, but I fail to find the discussions.
The current behaviour is a really annoying booby trap to land in when you are in the middle of a demo in front of innocent unsuspecting mathematicians.

[Eric Wieser]

import Mathlib.LinearAlgebra.Basic

/-- `Nat.rec` but with `0` and `+1` instead of `.zero` and `.succ` -/
@[eliminator]
def Nat.recWithTheRealZero.{u} {motive : ℕ → Sort u} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1)) (t : ℕ) :
  motive t := @Nat.rec.{u} motive zero succ t

example (m n : Nat) : n + m = m + n := by
  induction n

[Johan Commelin]

Is there a reason why we shouldn't have this eliminator somewhere in the bottom of our import hierarchy?

[Johan Commelin]

PR'd as #8769. But expect lots of breakage in induction proofs, so it'll take some time before this is ready for review.

[Eric Wieser]

You could shortcut the breakage for now with induction n using Nat.rec

[Patrick Massot]

The issue is that it breaks cases.

[Eric Wieser]

Does it? Can you give an example?

[Eric Wieser]

cases n using Nat.rec works too

[Johan Commelin]

Thanks Eric Wieser! I'll use that strategy. At a later point, people can decide to rewrite proofs using the new recursor.

[Patrick Massot]

Most recent previous discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ring.20tactic.20on.20.60.28n.2B1.29.5E2.3Dn.5E2.2B2n.2B1.60/near/398346446 with links to older ones.

[Johan Commelin]

Well, I hope this thread will the last one to discuss this issue

[Eric Wieser]

This message seems to contain the failing example

[Eric Wieser]

Note that the same problem can be obtained without a custom induction principle:

example (m n : Nat) : n + m = m + n := by
  cases n using Nat.rec
  /-
  case zero
  m : Nat
  ⊢ Nat.zero + m = m + Nat.zero
  -/
  · sorry
  /-
  case succ
  m n✝ : Nat
  n_ih✝ : Nat.succ n✝ = n✝ → Nat.succ n✝ + m = m + Nat.succ n✝  -- what?
  ⊢ Nat.succ n✝ + m = m + Nat.succ n✝
  -/
  · sorry

[Eric Wieser]

So I don't think it's fair to say this "breaks cases", I think cases is just broken itself

[Eric Wieser]

Ah, cases n using Nat.casesOn solve that issue

[Eric Wieser]

So I think the answer is we need both @[eliminator] and a new @[cases_eliminator]

[Johan Commelin]

Would you mind writing that one as well?

[Eric Wieser]

That's a core change

[Eric Wieser]

docs#Lean.Meta.getCustomEliminator? would need to learn a "rec := false" argument

[Eric Wieser]

Then I think these lines would pass in the existing induction : Bool into getCustomEliminator

[Kyle Miller]

I've been in the process of preparing a core change to fix this for Nat (making induction on Nat beautiful for everyone is an FRO priority :smile:)

[Kyle Miller]

I haven't made the PR yet (it's only a local branch), but, yes, part of the solution is to split @[eliminator] into two for cases and induction.

[Kyle Miller]

(@Adam Topaz already figured out most of it here, but I'm looking into seeing whether it's feasible to get equation lemmas to use 0 and n + 1 as well for Nat. A side effect would be that rcases would also use the right eliminator -- rcases does not use code that cares about @[eliminator].)

[Johan Commelin]

@Kyle Miller Shall I continue with my PR, or do you think that will actually make your work more difficult?

[Kyle Miller]

If you can stand to wait, that recursor should appear in core. It wouldn't hurt if you do decide to include it in mathlib in the meantime, but make sure not to add @[eliminator] since it will break either induction or cases (your choice).

[François G. Dorais]

The alternate recursors are in Std.

[Kyle Miller]

Oh, right, thanks for the reminder: docs#Nat.recAux and docs#Nat.casesAuxOn

[Johan Commelin]

@Kyle Miller how about I do add @[eliminator] and fix a whole bunch of proofs in mathlib. Because those proofs will need fixing anyway, right?

[Eric Wieser]

To be clear, it doesn't actually break cases, right? It just introduces some unused garbage?

[Kyle Miller]

In testing I did before, it actually put cases into unsalveagable states. I don't have those tests anymore though (this was months ago).

[Eric Wieser]

Does cases using Nat.casesAuxOn avoid the issue?

[Kyle Miller]

Yes, because it's using the correct kind of eliminator.

[Eric Wieser]

It sounds like Johan's plan is safe as long as that (and removing zero = 0 rewrites) is the only fix that gets made, since then when the real fix lands we can just delete the using clause

[Kyle Miller]

Another plan is to wait for the Lean PR and then do this all in the mathlib fixup branch. That would save needing to add using clauses and then removing them again.

[Kyle Miller]

I'm planning on making the PR within the next week (and if it all goes well, I'll have the PR today)

[Kyle Miller]

(But feel free to go and use using clauses everywhere. It won't cause any conflicts with what I'm doing, so long as you do it soon, before I start making that mathlib fixup branch. Otherwise we'll have to be careful synchronizing what we're doing.)

[Johan Commelin]

Ok, I think I'll wait for the fixup branch, because this weekend is full of family visits, and it sounds like you are making good progress doing it "the right way (TM)" :happy: