Does refl implicitly call other tactics?

Stream: new members

[Rishi Mehta]

Hello everyone,
I'm doing level 3 in the Addition World in the natural numbers game (https://cbirkbeck.github.io/natural_number_game/?world=2&level=3). I notice that

  induction b with d hd,
  {
    refl
  },

closes the first goal (the base case for the induction. However, the first goal before applying refl is ⊢ succ a + 0 = succ (a + 0). I would've assumed this would first require a rw add_zero, before refl, would close it. How did refl work on its own?

[Patrick Johnson]

Is definitional equality explained in NNG?

[Patrick Johnson]

succ a + 0 and succ (a + 0) are definitionally equal because x + 0 is definitionally equal to x for any x

[Kyle Miller]

In Lean, certain things are considered to be true by definition (this is known as "definitional equality", or that they're "defeq" for short).

The definition of addition is, essentially, add_zero and add_succ, so you can imagine that refl operates by applying these two lemmas wherever possible to try to make both sides the same.

[Rishi Mehta]

I see - thank you!

[Kevin Buzzard]

Yeah I explicitly avoided explaining definitional equality and indeed did the opposite -- I disabled rw so that it would not attempt to close defeq goals after application, because it confused new users. So now we only get confusion when people spot that refl is in fact stronger than I claim it to be. I peddle the lie that a+0=a is "true by axiom" rather than "true by definition" and tell the user to apply the "axiom" without telling them that the axiom is proved with refl internally.