## Stream: new members

### Topic: why does this work without add_zero

#### eax (Feb 28 2021 at 00:45):

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=
begin
induction c,
/- rw add_zero b, -/ /-
refl,

end


before the refl line it wants to prove ⊢ a + b + 0 = a + (b + 0) which assumes associativity ?

#### Hanting Zhang (Feb 28 2021 at 01:20):

(a + b) + 0 = a + b = a + (b + 0) you don't need associativity.

#### eax (Feb 28 2021 at 01:21):

right, but isn't that what I'm doing with the first add_zero ? How is lean proving this without it?

#### Hanting Zhang (Feb 28 2021 at 01:22):

n + 0 is defeq to n. Where are you using associativity?

#### Hanting Zhang (Feb 28 2021 at 01:23):

You've defined n + 0 = n when defining addition

#### eax (Feb 28 2021 at 01:25):

I think I'm more confused about what lean is doing than about the proof itself.

#### eax (Feb 28 2021 at 01:26):

is refl going farther than "the things on both sides of the = are identical?

#### Bryan Gin-ge Chen (Feb 28 2021 at 01:27):

Yes, it's able to unfold definitions to a certain extent. Did you take a look at the blog post I linked yet?

#### eax (Feb 28 2021 at 01:27):

I'm in middle of reading it now.

#### eax (Feb 28 2021 at 01:30):

this blog post makes a lot more sense. (I'm brand new to lean so somewhat clueless about what its all doing)

#### eax (Feb 28 2021 at 01:31):

it also explains that for e.g., lemma one_mul (m : mynat) : 1 * m = m := I could write

induction m,
refl,


instead of  rw mul_zero, refl,
since the former is true by definition

#### Hanting Zhang (Feb 28 2021 at 01:31):

Ah, I see what you were asking now. refl can close the goal without rw because it unfolds all of the a + b + 0 and a + (b + 0) to a + b. oops.

#### eax (Feb 28 2021 at 01:32):

yeah. I was expecting to need to be a lot more explicit.

#### Bryan Gin-ge Chen (Feb 28 2021 at 01:34):

Lean does a lot behind the scenes! Fortunately we usually don't need to worry too much about it. If you're curious, you can use the following options to have Lean log some output while it checks whether things are definitionally equal:

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true


#### eax (Feb 28 2021 at 01:35):

I'm playing this "game" https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game but good to know for when/if I get this installed locally

#### Hanting Zhang (Feb 28 2021 at 01:37):

You should also get familiar with the sidebar on https://leanprover-community.github.io/, all of the communities' resources are there

#### eax (Feb 28 2021 at 01:37):

yep! that's how I found this chat

#### Hanting Zhang (Feb 28 2021 at 01:38):

Oh yeah, I guess that was obvious :upside_down:

#### Kevin Buzzard (Feb 28 2021 at 09:10):

I don't talk about definitional equality at all in the natural number game because preliminary experiments with students showed that if the system randomly proved goals of the form X+0=X then the students would get confused, so I actually weakened the system somewhat and added add_zero without ever saying what its proof was -- I just claimed that it was an "axiom". The truth is that it's true by definition so you can prove it with refl. What I do not explain in NNG is that refl will prove definitional equalities, not just syntactic ones. For me as a mathematician, 0+X=X and X+0=X look pretty symmetric and I thought it was confusing if one proof was zero_add but the other was refl.

#### eax (Feb 28 2021 at 17:00):

The tradeoff is that the game hides what refl is actually doing. In fact, I was confused about why it was needed at all "once lean gets to X=X why should i have to add the syntactic noise of refl?" that it's actually doing work that the game makes you do explicitly is useful to know
As a computer scientist that understands (the basics of) term rewriting, 0+X=X and X+0=X actually look very different to me and it doesn't shock me you'd have to solve them separately.

#### Kevin Buzzard (Feb 28 2021 at 17:01):

In real Lean rw tries refl when it's done, so if you do the levels in real Lean then some of them finish much earlier than you would expect. If you're a programmer this is good, if you're a mathematician playing NNG this is apparently confusing.

#### Kevin Buzzard (Feb 28 2021 at 17:02):

This is what students were telling me, at least. "I hadn't finished the proof, how come it says I'm done?"

#### Kevin Buzzard (Feb 28 2021 at 17:02):

"well, if you think about it, a * 1 = 0 + a is definitional" isn't a good answer

#### eax (Feb 28 2021 at 17:02):

couldn't that be solved by enabling tracing?

#### Kevin Buzzard (Feb 28 2021 at 17:03):

I'm talking about mathematicians here. They don't use braces, thy don't use traces, they don't even look at the error box

#### eax (Feb 28 2021 at 17:03):

haha fair enough.

#### Kevin Buzzard (Feb 28 2021 at 17:04):

A goal of a * 1 = 0 + a magically disappearing will not be explained by traces, this assertion is as trivial to a mathematician as 1 * a = 0 + a and 1 * a = a + 0` etc

#### Kevin Buzzard (Feb 28 2021 at 17:04):

the fact that one of these is definitional and the others aren't is not actually mathematics, it is an implementation detail.

#### eax (Feb 28 2021 at 17:06):

there is certainly a tradeoff between making this conceptually simple to either CS and Math people

#### Kevin Buzzard (Feb 28 2021 at 17:06):

I was explicitly targetting math people

#### Kevin Buzzard (Feb 28 2021 at 17:06):

because that's the underlying problem

#### Kevin Buzzard (Feb 28 2021 at 17:06):

They teach this stuff in the CS department at Imperial, but nobody has heard of it in the maths department

#### eax (Feb 28 2021 at 17:07):

fair enough and understand the goal; my CS undergrad didn't go near this stuff so its been fun to learn/play the game.

Last updated: May 08 2021 at 04:14 UTC