refl skip add_zero

Stream: new members

[Sailor]

On the level 2 of addition world for exemple refl skip add_zero two times and do refl itself can someone explain me why ? qdqdqdz.PNG

[Kevin Buzzard]

Because although I don't explain this issue in the game, add_zero is true by definition so you can use refl to prove it

[Sailor]

Thanks ;)

[Sailor]

And how do i know what is true by definition ?

[Eric Wieser]

Well, you can try exact rfl and see when it works ;)

[Kyle Miller]

For the NNG, you're not meant to worry about the definitions since there are enough theorems to handle everything, but you can pull back the curtain by looking at the source code: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/mynat/add.lean#L10

[Kyle Miller]

That amounts to the following definition for addition:

m + 0 = m
m + succ(n) = succ(m + n)

(matching the NNG parenthesis convention)

[Sailor]

Ok thanks another question how can i tell lean to use a theorem on a succ d for exemple ?

[Kyle Miller]

In other words, what refl does is automatically apply add_zero and add_succ wherever it is able to, and then it checks they're the same.

[Sailor]

like in this situation
image.png

[Sailor]

because when i want to assoc it assoc the left hand side

[Sailor]

and i want to specify add_assoc a succ d

[Kyle Miller]

put parentheses around succ d

[Kyle Miller]

so rw add_assoc a (succ d)

[Sailor]

Is this in the doc ?

[Sailor]

instead of bothering you

[Kyle Miller]

the "real" parenthesis convention is that (f a b c) means $f(a,b,c)$

[Sailor]

Oh ok i'm a little confused that this is not rigorously defined in the beginning as im just "guessing" from my programming experience

[Kyle Miller]

Also, when there is an operator, like succ a + b + succ d, this means (in normal math notation) $\operatorname{succ}(a) + b + \operatorname{succ}(d)$

[Sailor]

I see right

[Kyle Miller]

I think the NNG walks a fine line between giving you just enough to be able to complete the tasks and giving you an information overload. It's fine coming here for clarification :smile:

[Sailor]

(deleted)

[Kyle Miller]

(re deleted comment, I completely understand, that tends to be my modus operandi, too.)

[Sailor]

But if your fine with it its ok ahah