Why is `2+2=4 := rfl`?

Stream: new members

[Michael Rothgang]

This question came up during yesterday's Lean workshop in Berlin: it's easy to understand that rfl proves 2=2 --- but it confused the participants that 2+2=4 also holds by rfl, see MWE:

example : 2000 + 2000 = 4000 := rfl

example :
  let n : Nat := 1;
  let m : Nat := 37;
  n + m = 38 := rfl

Can you help me understand why? Some wild guesses are

• Does it matter that 2 and 4 are natural number literals? It seems not...
• So, this means the kernel would also check 1000+1000=2000 by rfl, just slower?

[Riccardo Brasca]

In principle yes, rfl just unfolds the various definitions, of 2, of + and so on, and at the end it gets to two things that equal by definition. (In Lean4 it is possible that it uses some clever algorithm to compute the sum, I am not completely sure.)

[Johan Commelin]

When the kernel checks that two terms are defeq, it will do a bunch of unfolding. In particular, it will unfold the definition of + a bunch of times, and eventually see that the LHS is 4 by definition.

[Johan Commelin]

As Riccardo says, for Nat's there is more magic. But the "unfold until LHS = RHS" is the basic algorithm / mental model that helps understanding why rfl works on goals that aren't syntactic equalities.

[Michael Rothgang]

Thanks for the elaboration (no pun intended)!

[Michael Rothgang]

Two more examples, for my future self: to some extend, having specific numbers 2 and 4 is useful, so Lean can unfold the definition far enough to obtain an actual defeq.

-- Addition is defined this way.
example (n : Nat) : n + 0 = n := rfl
-- This is a theorem to show: as n is not a concrete number, Lean cannot show this.
-- example (n : Nat) : 0 + n = n := rfl -- fails

[Riccardo Brasca]

This is because addition is defined by recursion on the second variable