zero versus 0

Stream: new members

[Shing Tak Lam]

Hello, I'm just getting started using Lean, and I've been looking at the Natural Numbers game. I've copied the definitions over from the Github repository, but the behaviour seems to be different on my local version versus the online version.

So for example for the first exercise in the Addition world, the goal on the online version is 0 + 0 = 0, but on my local version is 0 + zero = zero. I've defined instance : has_zero mynat : ⟨mynat.zero⟩ like in the repository. I could obviously use rw mynat_zero_eq_zero,, but then it would be nice to know why and how to fix this, as a way to learn more about how Lean itself works. So is there a way for Lean to know (or for me to tell Lean) that zero and 0 are the same thing?

Is this something that is defined custom for the Natural Numbers Game, as I see that some of the code in the repo open lean, or am I missing something?

Thank you very much,

[Kevin Buzzard]

Yeah. What actually happens in the natural number game is that it isn't really honest Lean because honest Lean's induction tactic has this problem and i would constantly see this causing problems to students. So in the natural number game I change the induction tactic so that after it's applied, lean rewrites all the zeros to 0s

[Kevin Buzzard]

It will take me a while to remember the details, but here is an example of me defining a new tactic induction' which is "apply induction, and then run the simplifier" and here is where I tag that zero should be rewritten to 0. Finally here is where I tell Lean to use my induction tactic not the inbuilt one. Note that Rob Lewis did most of the technical work here.

[Shing Tak Lam]

Alright, I see. So if I'm just getting started with Lean would you suggest I just stick with zero in all of the proofs (I think the only numbers that come up are 0, 1 and 2, so not too many succs needed)? Or should I try and bodge it so that it reflects the behaviour of the Natural Numbers Game? From what I've seen so far, using 0, 1 and 2 seems to be more of an aesthetic decision, and functionally it (should) be the same. Obviously in the real world, Lean's nat would just be used, so this shouldn't be an issue anyways.

Another difference I noticed is that on my local installation of lean, simp and rw seem to be able to close goals, so a rw h for example can be the last statement in a proof. But in the natural numbers game I'd need to end the proof with refl. Is this also intended as a difference between the two?

[Scott Morrison]

If you have
@[simp] lemma mynat_zero_eq_zero : zero = 0 := rfl
then just calling dsimp should replace all your zeros with 0s.

[Shing Tak Lam]

Alright I see, so @[simp] is an attribute to tell lean that it can use it for simplifying? If so, I've added the @[simp] attribute to add_assoc and add_comm, but the simplifier isn't able to solve a goal that only consists of add_assoc and add_comm. Does it matter that they are in different files? I've imported those files into my working file and they are all in the same namespace.

The goal is

a * t + b * t + (a + b) = a * t + a + (b * t + b)

My manual proof to solve it is:

rw add_assoc, rw <-add_assoc (b*t), rw add_comm (b*t), rw add_assoc (a), rw add_assoc (a*t)

But running simp gives me a new goal, which isn't any simpler than the original.

a + (b * t + (b + a * t)) = a + (a * t + (b + b * t))

In the docs it says simp doesn't recognise <-, however even if I do the parts with the <- manually then use simp

rw add_assoc,rw <-add_assoc (b*t), simp,

It still doesn't solve it, and generates a new goal which it should be able to solve with only add_comm and add_assoc

a * t + b * t + (a + b) = a * t + a + (b * t + b)

Another question, from looking at the docs, it says dsimp is similar to simp, except it uses definitional equalities only. So does that mean that simp uses them as well, or is it only dsimp?

[Mario Carneiro]

you should also simp with add_left_comm

[Shing Tak Lam]

I see, thank you very much. After defining add_left_comm (It wasn't in the list of theorems on the left of the page), simp solved the goal. I guess it's time to go down the rabbit hole and find where that is defined in the Natural Numbers Game repo.

Edit: Interestingly, searching for left_comm in the Natural Numbers Repo does not have any results...

[Mario Carneiro]

you can prove add_left_comm using the other two

[Shing Tak Lam]

I know, it's quite simple to prove using just add_assoc and add_comm. My comment about the Natural numbers game is that simp can solve it in the game, even though I can't seem to find add_left_commdefined in the game (at least not in the repo).

I think what's happening is that there is more behind the scenes 'magic' (for the lack of a better word) in the Natural Numbers game than I thought.

[Mario Carneiro]

There was a recent move to remove the @[simp] attribute from add_comm, add_assoc and add_left_comm. Most likely this is not reflected in NNG

[Mario Carneiro]

I don't think NNG uses simp much

[Shing Tak Lam]

I think it might be namespaces? If I understand this correctly (VSCode go to definition on add_comm isn't very useful), add_comm is defined in by lean, but as all of the theorems are in the same namespace (namespace mynat) for the NNG, there is a mynat.add_comm. So when a theorem uses rw add_comm in the NNG it would use mynat.add_comm and not the one in lean's library. So changes in the library shouldn't change the NNG.

But then none of the theorems are tagged with @[simp] in the repo... So now I'm not sure anymore. I mean I have it working on my end now, so I should probably focus my effort on completing the game before (attempting and failing at) reverse engineering the NNG.

simp is often useful as a final step in the NNG, when the goal just requires commutativity/associativity to solve. It's not strictly required but it's great as a quality of life thing.

[Kevin Buzzard]

The natural number game is a standalone thing. I decided that I wanted users to see 0 and never zero so I made it so that users never see zero. In general the rule is that you should decide on one "canonical form" for things and try and stick to it. In Lean and mathlib they also decided on 0 over zero but you can decide what you want. If you're using mathlib it's probably best to stick with their conventions but I am unclear what you're doing. If you're defining your own natural numbers then you can use whatever conventions you like but it's best to be consistent.

The reason you see zero when using the induction tactic on Lean's naturals in Lean is a technical one, due to the default induction tactic always using the exact constructors used when defining the type, and you can't use 0 when defining the type.

Yes I also changed the behaviour of rewrite because I felt that beginner users were confused by its ability to close refl goals automatically. Again this is a one-off design decision based on my target audience. In general it's much more convenient to have rw closing refl goals once you know what you're doing.

Simp is complicated, it's not merely a matter of "if I tell it all the lemmas then it will figure out how to apply them in exactly the right order". Simp works best with lemmas for which the right hand side of the equality is simpler than the left hand side. Neither associativity nor commutativity have this property. here is where I tag those lemmas with simp -- I don't do it when I define them, I do it all at once when we have all three.

[Donald Sebastian Leung]

Kevin Buzzard said:

The natural number game is a standalone thing. I decided that I wanted users to see 0 and never zero so I made it so that users never see zero. In general the rule is that you should decide on one "canonical form" for things and try and stick to it. In Lean and mathlib they also decided on 0 over zero but you can decide what you want. If you're using mathlib it's probably best to stick with their conventions but I am unclear what you're doing. If you're defining your own natural numbers then you can use whatever conventions you like but it's best to be consistent.

The reason you see zero is a technical one, due to the default induction tactic always using the exact constructors used when defining the type, and you can't use 0 when defining the type.

Yes I also changed the behaviour of rewrite because I felt that beginner users were confused by its ability to close refl goals automatically. Again this is a one-off design decision based on my target audience. In general it's much more convenient to have rw closing refl goals once you know what you're doing.

Simp is complicated, it's not merely a matter of "if I tell it all the lemmas then it will figure out how to apply them in exactly the right order". Simp works best with lemmas for which the right hand side of the equality is simpler than the left hand side. Neither associativity nor commutativity have this property.

Wow, I didn't realize that you tweaked the behavior of certain fundamental tactics like rw and simp even after having gone through TPIL and got the chance to use rw/simp and other things as-is. This is very interesting ...

[Kevin Buzzard]

There is term mode and tactic mode and even something called conv mode. Rob Lewis and Simon Hudon showed me how to write my own "mode". All the begin end blocks in the natural number game are in a slightly hacked tactic mode, that's why if you look at the code they all start begin [nat_num_game]

[Donald Sebastian Leung]

Kevin Buzzard said:

There is term mode and tactic mode and even something called conv mode. Rob Lewis and Simon Hudon showed me how to write my own "mode". All the begin end blocks in the natural number game are in a slightly hacked tactic mode, that's why if you look at the code they all start begin [nat_num_game]

Guess I just learned something new today :smile:

[Patrick Massot]

Technically term mode and nat_num_game mode have not much in common.

[Shing Tak Lam]

Alright I see. Having thought about it a bit more, would it be fair to say that what simp does is (kind of in a hand wavy way) look through lemmas tagged with@[simp], see if the LHS match the goal. If so, then apply it. Then repeat. When nothing can be applied then stop.

If that is the case, then it would make sense for associativity/commutativity to be not very good for this, as it wouldn't have much of a reduction in complexity of the expression. So then using just assoc and comm for simp would be akin to a brute force (depth/breadth first) search with different combinations of assoc and comm?

Then that makes sense with the comment above talking about how the simp attribute was removed for add_comm, add_assoc.

[Kevin Buzzard]

It looks like I change rw, use, induction and cases. The symmetry' tactic (a modified symmetry that also works on hypotheses) is already in mathlib. Here is where I tell Lean to let tactic X in my mode equal the usual tactic X, for X not in those 5 cases, and here is where I insert my modified tactics.

[Kevin Buzzard]

I am not an expert in the simplifier. But most simp lemmas are of the form (thing) = (slightly simpler thing), or (thing) <-> (slightly simpler thing). The simplifier then knows what to do -- try and make stuff simpler. The question is whether you want the simplifier to also be able to solve goals of the form a+b+c+d+e=(d+(b+a)+(c+e)). It can, but there might be some trickery going on behind the scenes to make this happen. I think there's actually a tactic ac_refl whose job it is to specifically solve goals like this. If you're in a ring or a semiring, then ring will also solve these I think.