why does this work without add_zero

Stream: new members

[eax]

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

end

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

[Hanting Zhang]

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

[eax]

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

[Hanting Zhang]

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

[Hanting Zhang]

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

[Bryan Gin-ge Chen]

You might find this blog post about definitional equality helpful: https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

[eax]

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

[eax]

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

[Bryan Gin-ge Chen]

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

[eax]

I'm in middle of reading it now.

[eax]

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

[eax]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

the download guide is here: https://leanprover-community.github.io/get_started.html

[Hanting Zhang]

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

[eax]

yep! that's how I found this chat

[Hanting Zhang]

Oh yeah, I guess that was obvious :upside_down:

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[eax]

couldn't that be solved by enabling tracing?

[Kevin Buzzard]

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]

haha fair enough.

[Kevin Buzzard]

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]

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

[eax]

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

[Kevin Buzzard]

I was explicitly targetting math people

[Kevin Buzzard]

because that's the underlying problem

[Kevin Buzzard]

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

[eax]

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