Why can simp prove '0 = Nat.zero', but not '0 = MyNat.zero'?

Stream: lean4

[Adam Dingle]

I'm using Lean 4.5.0-rc1.

simp can prove 0 = Nat.zero, in fact without using any identities at all:

example : 0 = Nat.zero := by simp only []

However now let's try it with my own definition MyNat of natural numbers:

inductive MyNat where
  | zero
  | succ : MyNat → MyNat
deriving Repr

open MyNat (zero succ)

instance : OfNat MyNat 0 where
  ofNat := zero

example : 0 = MyNat.zero := by simp only []

I get

simp made no progress

Why is this?

This may seem like a technicality, but actually it makes proving some theorems less convenient. Consider this example from the chapter "Inductive Types" in "Theorem Proving in Lean 4":

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n <;> simp [*, add_zero, add_succ]

It works with the builtin Nat type, but fails with MyNat, precisely because simp can't resolve the base case which is similar to 0 = Nat.zero.

[Damiano Testa]

Does it work if you add an instance : Zero MyNat instead?

[Adam Dingle]

OK, I just tried that:

instance : Zero MyNat where
  zero := zero

The result is the same: "simp made no progress". (Actually I would have slightly surprised if this made a difference, since Zero is in MathLib and simp is outside it.)

[Matthew Ballard]

set_option trace.Meta.Tactic.simp true in before your declaration will tell what simp is thinking

[Adam Dingle]

Matthew Ballard said:

set_option trace.Meta.Tactic.simp true in before your declaration will tell what simp is thinking

That's a useful hint. I just enabled this option. When simp proves that 0 = Nat.zero, it reports

[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = Nat.zero ==> True

I'm a bit surprised that it's using eq_self, since I thought that the only option tells it to use no identities at all, but perhaps eq_self is special.

When it fails to prove that 0 = MyNat.zero, it reports

[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
      ?a = ?a
    with
      0 = MyNat.zero

[Eric Rodriguez]

I do think Nat has quite a lot of specific support written into the Lean tooling

[Damiano Testa]

Also, simp only really means that you ask simp to only use the simpOnlyBuiltins:

import Lean.Elab.Tactic.Simp

#eval Lean.Elab.Tactic.simpOnlyBuiltins
--  [`eq_self, `iff_self]

[Adam Dingle]

Damiano Testa said:

Also, simp only really means that you ask simp to only use the simpOnlyBuiltins

Aha. Thanks, that's helpful.