How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?

Question

I want to do the proof of n + 0 = n in Lean 4 using mathlib 4, my attempt:

-- Prove that n + 0 = n
theorem n_plus_zero : ∀ n : ℕ, n + 0 = n := by
  intro n
  -- use Nat.add to rewrite n + 0 to n
  rw [Nat.add]

but I get it fails to progress with error:

basic_nats_using_mathlib_nats.lean:14:13
Tactic state
1 goal
n : ℕ
⊢ n + 0 = n
Expected type
n : ℕ
⊢ ℕ → ℕ → ℕ
Messages (1)
basic_nats_using_mathlib_nats.lean:14:6
failed to rewrite using equation theorems for 'Nat.add'
All Messages (8)

but the definition of Nat.add from mathlib 4 looks right to me, so I'm not sure why it's failing:

set_option bootstrap.genMatcherCode false in
/--
Addition of natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently
evaluate using the "bignum" representation (see `Nat`). The definition provided
here is the logical model (and it is soundness-critical that they coincide).
-/
@[extern "lean_nat_add"]
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

but the rewrite tactic did work when I manually did the proof with my definition of add (using add left, which seemed to be the opposite side of what mathlib 4 has). How do I fix my proof using the definition of addition in mathlib 4. Note, I know it works with the Nat.add_zero theorem:

Nat.add_zero (n : ℕ) : n + 0 = n
import Init.Core

which is not what I am puzzled/trying to learn about.

Thanks!

Answer 1

The + notation is used for the general typeclass that represents addition. If you set the pretty printer to be maximally verbose set_option pp.all true you can see that the goal doesn't (directly) use Nat.add, it's stated as:

@Eq.{1} Nat
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) n

If you unfold the more general addition typeclasses used, you do get to Nat.add and you can (but you shouldn't) prove this by rewriting with Nat.add.

theorem n_plus_zero : ∀ n : Nat, n + 0 = n := by
  intro n
  simp only [HAdd.hAdd, Add.add]
  -- Now the goal is Nat.add n 0
  rw [Nat.add]
  done

These kind of direct references to an implementation on a specific type (like the rewrite lemmas for Nat.add) usually just serve as stepping stones a developer can use to prove that Nat.add has some more generic structure (for example, that it's an additive monoid), then that implementation of the more generic structure becomes the "public API". In this case, there's a generic add_zero theorem in Mathlib (admittedly I'm not sure what the idiomatic way is to discover the relationship between something a user might think to find, like AddMonoid and something like AddZeroClass, maybe someone can fill me in).

In an isolated example like this, the whole exercise may feel like noisy indirection, but the direct approach does not scale well for developments like Mathlib.

Answer 2

I'm not sure the broader goal you are asking about, but just to make sure it is clear (in addition to Chris Bailey's good answer), these sort of "follow the definition" simplifications are definitionally equal and can be proved with rfl:

theorem n_plus_zero : ∀ n : Nat, n + 0 = n := by
  intro n
  rfl

Of course, in practice, you are usually looking to prove a theorem with (n + 0) in it, but not where it is the goal. Nonetheless, you have a number of options to use this definitional equality.

-- make a lemma
theorem foo0 (n : Nat) : 2 * (n + 0) = n + n := by
  have h : n + 0 = n := rfl 
  rw [h]
  sorry

-- make an inline lemma
theorem foo1 (n : Nat) : 2 * (n + 0) = n + n := by
  rw [(by rfl : n + 0 = n)]
  sorry

-- break up steps using calc
theorem foo2 (n : Nat) : 2 * (n + 0) = n + n := by
  calc
    2 * (n + 0) = 2 * n := rfl
    _           = n + n := sorry