how to unfold numeric literals

Stream: general

[Asei Inoue]

/-- my own implementation of Nat -/
inductive MyNat where
  | zero
  | succ (n : MyNat)

/-- get a term of `MyNat` from one of `Nat` -/
def MyNat.ofNat (n : Nat) : MyNat :=
  match n with
  | 0 => MyNat.zero
  | n + 1 => MyNat.succ (MyNat.ofNat n)

@[default_instance]
instance (n : Nat) : OfNat MyNat n where
  ofNat := MyNat.ofNat n

/-- one of Peano axiom -/
example (n : MyNat) : MyNat.succ n ≠ MyNat.zero := by
  simp

/-- one of Peano axiom, literal version -/
example : 0 ≠ 1 := by
  simp
  -- unsolved goals...
  -- how to unfold numeric literal automatically?

[Asei Inoue]

-- This works, but is too ad hoc.
-- I want a way that doesn't get me into trouble when the numbers get bigger.
example : 0 ≠ 1 := by
  change MyNat.zero ≠ MyNat.succ .zero
  simp

[Kyle Miller]

intro h; cases h should prove it.

[Kyle Miller]

Or you can do change MyNat.zero ≠ MyNat.succ _ and let Lean handle filling in the _.

[Asei Inoue]

@Kyle Miller

thanks. but why this works?

example : (0 : Nat) ≠ 1 := by
  simp

what is the difference between MyNat and Nat?

[Kyle Miller]

Try simp? to see

[Asei Inoue]

example : (0 : Nat) ≠ 1 := by
  simp only [ne_eq, reduceCtorEq, not_false_eq_true]

what is reduceCtorEq? I see. reduceCtorEq is defined as simproc...

[Kyle Miller]

There is special support for Nat literals in reduceCtorEq as well. It sees 1 as Nat.succ 0.

[Asei Inoue]

Does this mean that a simproc can be defined for MyNat as well, so that a proof can be done with single simp?

[Kyle Miller]

Yes