Zulip Chat Archive

Stream: new members

Topic: why does this work without add_zero


view this post on Zulip 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, -/ /-
rw add_zero (a+b),
refl,

end

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

view this post on Zulip Hanting Zhang (Feb 28 2021 at 01:20):

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

view this post on Zulip 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?

view this post on Zulip Hanting Zhang (Feb 28 2021 at 01:22):

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

view this post on Zulip Hanting Zhang (Feb 28 2021 at 01:23):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 28 2021 at 01:23):

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

view this post on Zulip eax (Feb 28 2021 at 01:25):

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

view this post on Zulip eax (Feb 28 2021 at 01:26):

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

view this post on Zulip 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?

view this post on Zulip eax (Feb 28 2021 at 01:27):

I'm in middle of reading it now.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip eax (Feb 28 2021 at 01:32):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Hanting Zhang (Feb 28 2021 at 01:36):

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

view this post on Zulip 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

view this post on Zulip eax (Feb 28 2021 at 01:37):

yep! that's how I found this chat

view this post on Zulip Hanting Zhang (Feb 28 2021 at 01:38):

Oh yeah, I guess that was obvious :upside_down:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?"

view this post on Zulip 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

view this post on Zulip eax (Feb 28 2021 at 17:02):

couldn't that be solved by enabling tracing?

view this post on Zulip 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

view this post on Zulip eax (Feb 28 2021 at 17:03):

haha fair enough.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip eax (Feb 28 2021 at 17:06):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 17:06):

I was explicitly targetting math people

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 17:06):

because that's the underlying problem

view this post on Zulip 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

view this post on Zulip 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