Nat term is equal to 0 or _ + 1

Stream: general

[Peter Nelson]

As part of teaching, I'm thinking about the following issue. In the middle of a proof, I have (something complicated) : Nat, and want to divide into cases where the complicated expression is 0 or equal to _ + 1, with minimal fuss. Something like the below is more fuss than I'd like, since it requires typing out the statement that I need fully, as well as a proof, and it includes the word 'induction', which is likely confusing to a mathematically literate novice.

import Mathlib.Tactic

example (f : α → ℕ) (a : α) : False := by
  obtain (h0 | ⟨k,hak⟩ : f a = 0 ∨ ∃ k, f a = k + 1) := by induction f a <;> simp
  · -- solve the case `f a = 0`
    sorry
  -- solve the case `f a = k + 1`
  sorry

So my real question is why the following isn't in mathlib. Is there an approach to the above that I'm missing?

theorem Nat.exists_eq_zero_or_add_one (n : ℕ) : (n = 0) ∨ ∃ m, n = m + 1 := by
  induction n <;> simp

I'm also having an analogous issue splitting an ENat into the infinite and finite cases, where the relevant short proof is a bit longer and more annoying.

[Ruben Van de Velde]

Well, induction n or cases n is exactly this

[Peter Nelson]

So what would that look like applied in the first example?

[Ruben Van de Velde]

import Mathlib.Tactic

example (f : α → ℕ) (a : α) : False := by
  cases h : f a with
  | zero =>
    -- solve the case `f a = 0`
    sorry
  | succ n =>
    -- solve the case `f a = k + 1`
    sorry

[Peter Nelson]

That gives me zero and succ instead of 0 and +1. Can we not do better for the purposes of teaching?

[Peter Nelson]

The approach also does annoying things that need rewriting in the ENat case.

[Ruben Van de Velde]

I think this may be fixed in an upcoming version of lean for Nat. For ENat you can use

import Mathlib

example (a : ENat) (P : ENat → Prop) : P a := by
  cases a using ENat.recTopCoe with
  | top => sorry
  | coe n => sorry

[Peter Nelson]

How would I do this?

example (a : α) (f : α → ℕ∞) (P : ℕ∞ → Prop) (htop : P ⊤)
    (h_coe : ∀ (a : α) (n : ℕ), f a = n → P (f a)) : P (f a) := by
  cases f a using ENat.recTopCoe with
  | top =>
    exact htop
  | coe n =>
    -- Nothing like `f a = ↑n` is in the context here.
    sorry

[Ruben Van de Velde]

cases h : f a using ENat.recTopCoe with

[Peter Nelson]

Right - it's the annotation h : _ in cases that I've been missing. That answers my question - thanks!

[Kyle Miller]

Peter Nelson said:

That gives me zero and succ instead of 0 and +1. Can we not do better for the purposes of teaching?

Just to confirm, we do have this improvement in the next release of Lean. You'll see this for induction/cases/rcases/obtain/rintro

[Mark Fischer]

Would it make sense to let Cases act more like Match when the arms (| _ => ,,,) are present? (Ie, give them full pattern matching and exhaustiveness checking)

[Eric Wieser]

Why not just use match in that case?

[Mark Fischer]

Eric Wieser said:

Why not just use match in that case?

Yeah, that's fair enough. I suppose it avoids switching from tactics to terms? Lessons some cognitive load, but it just pushes it down the line to tactics like inductive.

Probably not a good enough reason though.

[Kim Morrison]

I'd suggest not thinking of match as "switching to terms". Note that when you use match in tactic mode, you are still in tactic mode after the =>.