Natural Numbers Game

Stream: new members

[Patrick Stevens]

Two questions:

I've defined the following helper because it turned out to be necessary. My first question will end up being "why was this necessary?".

lemma add_comm' (a b : mynat) : add a b = add b a :=
begin [nat_num_game]
  exact (add_comm a b)
end

Then I'm trying to prove:

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin [nat_num_game]
  intro f,
  cases a,
  rw (zero_add b) at f,
  exact f, -- done the case a=0
  rw (add_comm (succ a) b) at f,
  injection f,
  rw (add_comm' b a) at h_1,
  exact (eq_zero_of_add_right_eq_self h_1)
end

1. Why did I have to define add_comm' to get the rw (add_comm' b a) at h_1 to stick? I couldn't simply rewrite by add_comm b a.
2. How can I make the recursive call to eq_zero_of_add_right_eq_self h1? I'm getting "unknown identifier" at the moment.

[Patrick Massot]

I don't think playing the natural number game off-line is so well supported. Your first issue is probably a conflict between mathlib's add_comm and the one Kevin crafted for the game. The second issue is simply not what proofs by induction look like in Lean. This should be all explained if you play the game online;

[Kevin Buzzard]

Can you post code which compiles? i.e. let's assume I have got a local copy of the game. Can you give me something I can cut and paste, with the imports and opens you're using? You shouldn't need to define add_comm' and if I can't easily reproduce your errors it's hard to help (I've just spent a few minutes trying and I've failed)

[Patrick Stevens]

The code which demonstrates "I have to use add_comm'" is as follows:

import mynat.definition -- Imports the natural numbers.
import mynat.add -- definition of addition

namespace mynat

lemma zero_add (n : mynat) : 0 + n = n :=
begin [nat_num_game]
  induction n,
  refl,
  rw (add_succ 0 n_n),
  rw n_ih,
  refl
end

lemma succ_add (a b : mynat) : succ a + b = succ (a + b) :=
begin [nat_num_game]
  induction b,
  rw (add_zero a),
  rw (add_zero (succ a)),
  refl,
  rw (add_succ a b_n),
  rw (add_succ (succ a) b_n),
  rw b_ih,
  refl
end

lemma add_comm (a b : mynat) : a + b = b + a :=
begin [nat_num_game]
  induction a,
  rw (zero_add b),
  refl,
  rw (succ_add a_n b),
  rw a_ih,
  rw (add_succ b a_n),
  refl
end

lemma add_comm' (a b : mynat) : add a b = add b a :=
begin [nat_num_game]
  exact (add_comm a b)
end

-- this is used for antisymmetry of ≤
lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin [nat_num_game]
  intro f,
  cases a,
  rw (zero_add b) at f,
  exact f,
  rw (add_comm (succ a) b) at f,
  injection f,
  rw (add_comm' b a) at h_1,
  sorry
end

[Kevin Buzzard]

The natural number game tries very hard to stop notation leaking through, this looks like your problem. The natural number game was written precisely because Lean's induction tactic was very poor with regards to leaking notation. You are seeing precisely the problems which I saw my users see when they were trying to write the game themselves. injection f is not a natural-number-game-sanctioned tactic and it looks like you have managed to create a hypothesis h_1 which mentions add a b. You should change <write what h_1 should actually say, i.e. change add to +> at h_1. Notation leakage is a big problem if you try to do things yourself, and I don't explain this sort of thing at all in NNG.

[Patrick Stevens]

OK, thanks very much

[Kevin Buzzard]

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin [nat_num_game]
  intro f,
  cases a,
  rw (zero_add b) at f,
  exact f,
  rw (add_comm (succ a) b) at f,
  injection f, -- leakage
  change b + a = a at h_1, -- fixed
  rw add_comm at h_1, -- works
  sorry
end

[Kevin Buzzard]

See how much easier it is if you post fully working code?

[Kevin Buzzard]

I would have been able to solve it in 1 minute not 10 ;-)

[Kevin Buzzard]

The underlying issue going on here is that there is something called definitional equality, which means "two things are equal because they have the same definition", and there is something called syntactic equality, which means "two things are equal if they are literally exactly the same string of symbols".

[Patrick Stevens]

Kevin Buzzard said:

I would have been able to solve it in 1 minute not 10 ;-)

Sorry, yes - this is true

[Kevin Buzzard]

rw only works with syntactic equality. add a b is definitionally equal to a + b but not syntactically equal to it.

[Patrick Stevens]

Ah, OK - I was misled by Agda's rewrite, which doesn't care

[Kevin Buzzard]

The change tactic can be used to change anything to something definitionally equal. It works on hypotheses and goals.

[Patrick Stevens]

(both my problems in this thread appear to be that Agda has given me in-built assumptions about how Lean works)

[Kevin Buzzard]

Oh that's interesting about Agda. The whole [nat_num_game] stuff is my attempt to stop notation being leaked like this, but as you can see it's a pretty difficult task. Because basically I'm trying to teach mathematicians to rewrite, leakage is a killer. Lean's inbuilt induction tactic always returns the exact constructors used to define the type, and when mynat is defined, we don't have access to notation.

[Kevin Buzzard]

Hence induction by default will give mynat.zero and mynat.succ, and already mynat.zero is enough to stop zero_add working, because 0 is notation, but it's notation for has_zero.zero, which is defeq to mynat.zero. rw can see through notation, but it's the mynat.zero not being has_zero.zero which causes no end of confusion to maths undergrads.

[Kevin Buzzard]

The [nat_num_game] monad modifies certain core tactics by basically doing all of those changes to get things back to the canonical notation needed for the rws to work and look good, but it's not a "whatever the user does, fix stuff up" thing, it's literally just explicitly modifying the behaviour of certain core tactics like induction and cases.

[Kevin Buzzard]

Maybe I should write up some notes for experts (sorry for not realising earlier that you had a lot of background knowledge, there are so many people around nowadays asking questions about the game and I forget who knows what).

[Patrick Stevens]

I broke several of the cardinal rules about how to ask for help, it's hardly your fault :P

[Patrick Stevens]

Thanks very much

[Kevin Buzzard]

I think one thing that's interesting about the community here was that I am a mathematician and I had the idea about the game when trying to get undergrads to just write Lean files to prove stuff like this about a home-rolled nat, and then when I realised there was this notational leakage issue I asked for help and the community stepped in fixed it by showing me how to make my own tactic monad, and then when I realised that mathematicians weren't going to be downloading lean I asked for help and the community stepped in again with all this web framework stuff, there are all these people in the background without whom it would never have got off the ground. This is why this chatroom is such a cool place to be.

[Daniel Keys]

The online NNG is a great learning tool, but there are a number of things that work in a different way than in a local Lean installation. Even rw for example; it does not close a goal in NNG, but otherwise it does so. It might be a good idea to collect such changes in a "disclaimer" list for this and other such games that are bound to spring up, although with Lean 4 in the works this may not be the best time.

[Shing Tak Lam]

@Daniel Keys

There was this thread not too long ago when I was trying to do the same thing and found quite a few differences between NNG and my local Lean installation.

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/zero.20versus.200/near/188937541

[Shing Tak Lam]

Also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/zero.20versus.200/near/189001740 later in the thread.

The list of changes is https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/zero.20versus.200/near/189002663

Basically just Kevin's answers to my questions :)

[Daniel Keys]

@Shing Tak Lam Sure, these are good in their own right. What I meant, though, was that the online game pages could themselves host an additional summary page, more or less formal, of changes made to the usual tactics. Given the work that the game designer logs in anyway, it is a little unfair to ask them for any extra bit. It would save us (the players) from some later surprises though, although figuring stuff out is eventually part of the bigger game.

[Kevin Buzzard]

The game designer is going to make it to the end of term (one week away) and then hopefully sit down and deal with the many issues which have arisen with the natural number game since Christmas, so any suggestions about how to improve it are welcome :-)

[Daniel Keys]

@Kevin Buzzard Many will probably agree that a cool way this designer could use some of their time would be having the real number gem (sorry, I literally had a typing mistake...I meant game) up and running. Sure enough they know how to take the good decisions by themselves though!-:)

[Kevin Buzzard]

real number game, group theory game, integer game, rational number game, logic game. They're all on my todo list :-)

[Patrick Stevens]

I, for one, am hoping to write the representation theory game, and then do it :P

[Filip Szczepański]

mul_left_cancel is the first proof I'm kinda getting stuck on. Gonna keep trying though.

[Johan Commelin]

It seems to be the one everyone gets stuck on.

[Filip Szczepański]

It's hard to know if I'm on the right track or not

[Johan Commelin]

I don't know if it helps, but most people say that once they are on the right track they are done immediately...

[Filip Szczepański]

Here's what goals I end up with:

case mynat.succ
a c b_n : mynat,
b_ih : a ≠ 0 → a * b_n = a * c → b_n = c
⊢ a ≠ 0 → a * succ b_n = a * c → succ b_n = c

[Filip Szczepański]

And I'm not sure if there's somehow a straightforward way to go from b_ih to the goal

[Donald Sebastian Leung]

Nope, there isn't, at least with your current proof state. Consider the hint given at that level to try revert b before induction :wink:

[Filip Szczepański]

Oh, to get the forall?

[Filip Szczepański]

I should have taken that advice more literally

[Filip Szczepański]

What's the general strategy if I'm given a goal that I know is false?

[Kenny Lau]

backtrack

[Kevin Buzzard]

Unless your hypothesis are contradictory

[Mario Carneiro]

then your goal isn't false, is it

[Kevin Buzzard]

Depends how literally you interpret the statement

[undef]

Hi, I'm having trouble in the natural number game, to be precise advanced multiplication world.
For example I proved the first level like this:

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=

cases b with n,
intro h,
cc,
intros ha hn,
cases a with a,
cc,
apply succ_ne_zero _,

So I "understand" most of my proof (and by that I mean I expected cc to be able to close the goals when I used it, even though I can't inspect what exactly it did).
But I'm puzzled about the last line - I didn't expect the proof to be complete after this (for lean).
Could someone explain why?

[Kevin Buzzard]

To understand what happened here you need to know something about definitional equality, which is not something I emphasize in NNG

[undef]

Is there a way to inspect the state of lean with more granularity?

[undef]

I expected that I would have to tell lean to use ha and hn to finish the proof.

[Kevin Buzzard]

Sorry, real life intervened

[Kevin Buzzard]

When you tried to apply succ_ne_zero Lean tried to convince itself that your goal was of the form succ X ne 0 by definition

[Kevin Buzzard]

And to see through this you have to know what is true by definition and what is true because of a theorem

[Kevin Buzzard]

For example add_succ is true by definition and succ_add is not

[undef]

Thank you, I will investigate that!

[Moses Schönfinkel]

ha and hn are equivalent to true, they are not very useful hypotheses - it holds vacuously that succ n \neq 0 - your conclusion in your current goals is similar (1 + k) * (1 + n) cannot possibly be 0 for k n \in mathbb{N}, no matter what the context contains; what Kevin alluded to with definitional equality is something like this:

cases b with n,
intro h,
cc,
intros ha hn,
cases a with a,
cc,
change succ a * succ n       with (a + 1) * (n + 1),
change (a + 1) * (n + 1)     with (a + 1) * n + (a + 1),
change (a + 1) * n + (a + 1) with ((a + 1) * n + a) + 1,
change (a + 1) * n + (a + 1) with succ ((a + 1) * n + a),
apply succ_ne_zero _,

Note that change X with Y only works when X is defeq with Y - so I just make some explicit rewrites, rather than leave Lean compute these from definitions.

[Moses Schönfinkel]

Maybe I should add that the last conclusion before apply succ_ne_zero _ is now succ ((a + 1) * n + a), which fits the lemma "more obviously".

[undef]

I didn't know the change command, but I like it as it is much more explicit!
Thank you very much.

[Kevin Buzzard]

I don't think that mathematicians are interested in the difference between definitional equality and "normal equality", whatever that means, but what is going on here is that a + 1 is by definition a + succ 0 which is by definition succ (a + 0) which is by definition succ a. It is not a coincidence that you have to prove zero_add in NNG and you don't have to prove add_zero -- in fact add_zero can be thought of as an axiom, defined when addition is defined. But zero_add needs to be proved by induction. This way of thinking about + is extremely asymmetric and very counter-intuitive to a mathematician's model of addition, so I don't stress this at all. The change tactic changes a goal to a definitionally equal goal so it is in some sense a very unmathematical tactic -- it will change a + 0 to a but it won't change 0 + a to a.

[Patrick Massot]

There is still some mathematical content in saying that a + 0 = a by definition while 0 + a = a is a theorem (if you define addition by induction on the second argument).

[Patrick Massot]

It's so basic that your mind blurs the distinction, but this game is about setting up the foundations of natural numbers, so you can't say this is unmathematical.

[Kevin Buzzard]

To Gauss, the naturals were a commutative semiring and this did not need to be questioned.

[Patrick Massot]

This distinction becomes unmathematical once the foundations are done, because you don't want to care about the foundational details after they have been taken care of.

[Patrick Massot]

But NNG is all about foundations.

[Patrick Massot]

That's why I initially thought people would not like it. But clearly I was wrong.

[Kevin Buzzard]

I was in some sense surprised too, but this is what bubbled to the top when I started showing undergraduates this stuff.

[Filip Szczepański]

I somehow got the web version of Lean stuck without using repeat now, on le_succ_of_le. I just copy-pasted the code from the end and changed the ??? to (succ c)

[Nam]

why does a ≤ b ∧ ¬b ≤ a accept a hypothesis of a < b?

[Mario Carneiro]

those two are defeq

[Kenny Lau]

the connective is “and”.

[Nam]

oh, they are defeq. i see.

[Mario Carneiro]

well, they don't have to be defeq but I would guess that they are for nat

[Kenny Lau]

I thought a <= b is defeq with succ a < b

[Mario Carneiro]

actually they aren't for nat

[Mario Carneiro]

but maybe they are for mynat or whatever NNG uses?

[Nam]

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/mynat/lt_not_used.lean#L5
the file is called "not used" though.

[Kevin Buzzard]

They're defeq in nng

[Sam Raleigh]

Hello there,

I was making my way through level 6 of inequality when I stumbled on something that has me a bit confused. I was able to finish the level, but the following code that I used to do so bothers me.

  cases hab with c uhab,
  cases hba with d uhba,
  rw uhab at uhba,
  symmetry at uhba,
  rw add_assoc at uhba,
  have h := eq_zero_of_add_right_eq_self a (c + d),
  have h1 := h uhba,
  have h2 := add_right_eq_zero h1, --why does this work???
  rw h2 at uhab,
  rw uhab,
  ring,

I apologize in advance for my uninformative variable names. Why is it that have h := eq_zero_of_add_right_eq_self expects an expression of the form (a b : mynat), but have h2 := add_right_eq_zero expects a proposition? More specifically, why can't I write have h := eq_zero_of_add_right_eq_self uhba without lean whining like I did with have h2 := add_right_eq_zero h1?

[Kevin Buzzard]

What is the statement of the theorem you're proving?

[Sam Raleigh]

theorem le_antisymm (a b : mynat) (hab : a ≤ b) (hba : b ≤ a) : a = b :=

[Sam Raleigh]

If my understanding of what I learned in proposition world is correct, lean treats implications like eq_zero_of_add_right_eq_self as functions from proofs to proofs, so why can't I write have h := eq_zero_of_add_right_eq_self uhba and obtain h := c + d = 0 as a result?

[Kevin Buzzard]

mynat.eq_zero_of_add_right_eq_self : ∀ (a b : mynat), a + b = a → b = 0

[Kevin Buzzard]

so

h : a + (c + d) = a → c + d = 0

[Kevin Buzzard]

Aah! But

mynat.add_right_eq_zero : ∀ {a b : mynat}, a + b = 0 → a = 0

[Sam Raleigh]

exactly!

[Kevin Buzzard]

The brackets are different. Does this answer your question? I guess the difference between the () and {} brackets aren't explained in the game.

[Sam Raleigh]

Ah I see! I don't recall the difference ever being explained in game, and I've completed everything except what's left of inequality world and power world

[Kevin Buzzard]

It's because the idiot who designed this stupid game decided to make the numeral inputs explicit in the definition of eq_zero_of_add_right_eq_self

[Sam Raleigh]

what is the difference between {} and () then?

[Kevin Buzzard]

With () brackets, Lean expects you to tell it the input. With {} brackets Lean decides it will guess from the context.

[Kevin Buzzard]

It seems to me that in my model solutions, I never use eq_zero_of_add_right_eq_self at all, so I could just change the brackets and it wouldn't break anything.

[Sam Raleigh]

Ah thanks, this clarifies a lot of confusion I've had throughout the game so far. I couldn't figure out why different theorems were so inconsistent in what they expected as input.

[Kevin Buzzard]

I tried to make it so that the inputs were always "the things which the user would guess" because I wanted to avoid having to explain the different kinds of brackets.

[Kevin Buzzard]

I was going to take a look at the natural number game tomorrow, there are some other issues which people pointed out recently. Probably tomorrow evening there will be a new version where this issue works better.

[Kevin Buzzard]

Thanks for the comment :-)

[Sam Raleigh]

Thanks! Also thanks in general for creating this game. I've learned more about lean in the two days I've been playing it than in the two weeks I spent trying to decipher the resources on the github. You've created something really neat

[Kevin Buzzard]

We're working on a sequel: https://github.com/ImperialCollegeLondon/real-number-game

[Sam Raleigh]

: O

[Kevin Buzzard]

I was going to take a good look at that tomorrow too -- my co-author has been doing everything

[Sam Raleigh]

Level 15 of inequality world says, "By default, the definition of a < b in Lean, once ≤ is defined, is this: a < b := a ≤ b ∧ ¬ (b ≤ a)". Why doesn't lean simply define a < b as a < b := ¬ (b ≤ a)? Is it for the convenience of easily obtaining a ≤ b from a < b?

[orlando]

I think it is because all relation ≤ are not total ! For example, the relation ⊆ on subset of a set X . If we take X = { 0,1} and the relation ⊆ on the subset of X we have ¬ {1} ≤ {0} and you don't want to tell that {0} < {1} ! It's ok for the relation where all element are comparable.

[Aniruddh Agarwal]

Kevin Buzzard said:

We're working on a sequel: https://github.com/ImperialCollegeLondon/real-number-game

Do you know when this will be ready? Using Lean to gamify undergrad math is a fantastic idea

[Sam Raleigh]

Level 7 of inequality world says "Note that you can do things like have h2 := add_right_eq_zero _ _ h1 if h1 : a + c = 0." What exactly do the underscores do here? The level doesn't give any more details beyond that note, and this is my first time seeing them in the game.

[Alex J. Best]

The underscores mean that Lean should try and infer those arguments, in this case add_right_eq_zero has type

lemma add_right_eq_zero (a b : mynat) : a + b = 0 → a = 0

but we can see that if we apply add_right_eq_zero with a c h1 as arguments where h1 has type a+c = 0 then the first two arguments (a and c) aren't strictly needed, theres only one possible thing they can be given the type of h1 for everything to make sense, so the underscores tell lean to work out those arguments automatically.

[Alex J. Best]

In this case theres not a huge amount of savings (you only have to type one character anyway), generally it saves us from having to retype long complicated terms sometimes, which can also improve readability, or from having to remember which way round arguments go. And it can make it easier to change variable names later or copy lines to different contexts.

[Alex J. Best]

But I think this is a bit confusing actually, as in the latest version of the natural number game the arguments for add_right_eq_zero are always implicit (this was changed only recently) so depending on which version is live for you it may be that you never needed to type add_right_eq_zero a c h1.

[Alex J. Best]

Looks like this is PR https://github.com/ImperialCollegeLondon/natural_number_game/pull/69/

[Sam Raleigh]

Thanks!

[edderiofer]

Alright, so I currently have hd : ∀ (b : mynat), a * b = a * d → b = d, and h : a * b = a * d as hypotheses; how do I use this to conclude that b = d?

[Mario Carneiro]

have := hd _ h

[Mario Carneiro]

or exact hd _ h if it's your goal

[Mario Carneiro]

or apply hd, apply h

[edderiofer]

Hooray! Thanks!

[edderiofer]

Currently I have hba : ¬a ≤ a, hab : a ≤ a as hypotheses; how do I show that this can prove false?

[edderiofer]

(Inequality World, level 15. https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=10&level=15 )

[Sam Lichtenstein]

edderiofer said:

Currently I have hba : ¬a ≤ a, hab : a ≤ a as hypotheses; how do I show that this can prove false?

Recall that ¬P is by definition P->false

[edderiofer]

Ah, yes.

[Jalex Stark]

i don't know if the contradiction tactic works in NNG, but it closes the goal when you have a statement and its negation in your hypothesis list

[edderiofer]

Ah, that's handy. Lemme check.

[edderiofer]

Yep, it does! :D

[edderiofer]

Alright, that's this game done. I think I'll do the next-suggested stuff tomorrow. For now, bed.

[Jalex Stark]

Good night, see you around!

[Sam Lichtenstein]

@Kevin Buzzard How about adding https://github.com/leanprover-community/mathematics_in_lean as a link on the "What's next" (after NNG) page? https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/WHATS_NEXT.md

[Patrick Massot]

A link to https://leanprover-community.github.io/learn.html would be better

[Patrick Massot]

except we need to add mathematics in Lean to that webpage that is already outdated

[Alexandre Rademaker]

In Level 5/9 of multiplication world, it looks like repeat { rw mul_zero } also evoke the refl to clear the goal, I didn't find anything about it in the TPinL. Am I right?

[Mario Carneiro]

link please

[Mario Carneiro]

In regular lean, rw calls refl to try to close the goal. In NNG it doesn't

[Alexandre Rademaker]

So inside the repeat, rw works as regular Lean...

[Mario Carneiro]

that seems unlikely

[Mario Carneiro]

link please

[Kevin Buzzard]

I think I rewired rw so it always does the non-refl version. Cut and paste the link!

[Mario Carneiro]

Do we have a linkifier for this?

[Kevin Buzzard]

we could ask the guy that made all the linkifiers...wait.

[Alexandre Rademaker]

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=3&level=5

[Kevin Buzzard]

You can cut and paste your proof -- check out the exciting new clip board in the top right of the input box

[Mario Carneiro]

I just enable the linkifiers, they are written by you folks

[Alexandre Rademaker]

After the induction on c, we can close the first goal with repeat {rw mul_zero}

induction c with d hd,
repeat { rw mul_zero },
...

[Mario Carneiro]

I recall a NNG linkifier being proposed but I guess I didn't enable that. Plus there are now like 4 NNG clones and I don't know all the appropriate links

[Kevin Buzzard]

Yeah that is puzzling!

[Kevin Buzzard]

Does repeat try refl when the thing it's repeating stops working?

[Mario Carneiro]

no

[Mario Carneiro]

assuming you didn't change it in NNG

[Kevin Buzzard]

then this must be a glitch in the matrix

[Mario Carneiro]

where's the source for the NNG tactic setup

[Alex J. Best]

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/nat_num_game.lean

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/modded.lean is my modded rw

[Alexandre Rademaker]

Hum, I didn't know that we have a layer of customizations on top of the Lean tactics...

[Kevin Buzzard]

Yup...

[Kevin Buzzard]

I did it specifically to confuse everyone, it's working really well

[Mario Carneiro]

I'm pretty sure "teaching non-transferrable skills" is the whole point of games

[Kevin Buzzard]

Actually, I did it because I didn't want rw randomly closing refl goals and confusing mathematicians who were just learning about equational reasoning

[Mario Carneiro]

I think what happened is that because repeat is not one of your overridden commands, it was copied verbatim from tactic.interactive; but the argument of repeat is an itactic which uses the tactic monad instead of nat_num_game. So repeat {rw ..} is calling tactic.interactive.rw instead of nat_num_game.interactive.rw

[Mario Carneiro]

Similar issues should exist for any commands that take a braced tactic list argument, like case, all_goals, any_goals, repeat, and possibly even focus, also known as the bare brackets { }. So I guess you did right to not teach people to use braces around subgoals

[Mario Carneiro]

correction, bare { tac } is not affected, but focus { tac } is

[Alexandre Rademaker]

in the game, I also noted that we can use { sorry } for moving to another goal... right?

[Bryan Gin-ge Chen]

Sort of. { and } focus the current goal, and then sorry finishes it. There are other goal management tactics like tactic#swap which allow you to switch between goals; try clicking "filter by tag" on the left of the mathlib tactic docs and then select "goal management" to see them all. (Not sure how many work inside the NNG.)

[Kevin Buzzard]

I tended to import what I needed when I needed it so what works will be random and will change over the course of the game

[Alexandre Rademaker]

lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
begin
 intros pq qr,
 split,
 intro p,
 exact qr.1 (pq.1 p),
 intro r,
 apply pq.2,
 apply qr.2,
 exact r,
end

The tactics have and apply were presented as the forward vs backward reasoning strategies. But exact t (when we think about the term t) vs apply is also a forward vs backward reasoning, does it make sense?

[Alexandre Rademaker]

In http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=8, I can't see any import but the text says Did you spot the import? What do you think it does?...

[Bryan Gin-ge Chen]

I think that's a holdover from when the game was meant to be played in VS Code: https://github.com/ImperialCollegeLondon/natural_number_game/blob/b83e7ebd56a82351e2fd8a187de543803074818b/src/game/world7/level8.lean#L1

[Bryan Gin-ge Chen]

Ah yes, see: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/natural.20number.20game.20questions/near/189524028

[Alexandre Rademaker]

the tactic tauto is from mathlib, right?

[Utensil Song]

I'm trying to rewrite some proofs in NGN to different styles and have 5 questions regarding the subtleties (marked as Q0 through Q4 in the comments of the following #mwe which is a bit long but I did try to minimalize it, please start reading at -------------------- ), thank you very much:

inductive mynat
| zero : mynat
| succ (n : mynat) : mynat

namespace mynat

instance : has_zero mynat := ⟨mynat.zero⟩

theorem mynat_zero_eq_zero : mynat.zero = 0 := rfl

def add : mynat → mynat → mynat
| m 0 := m
| m (succ n) := succ (add m n)

instance : has_add mynat := ⟨mynat.add⟩

def mul : mynat → mynat → mynat
| m zero := zero
| m (succ n) := mul m n + m

instance : has_mul mynat := ⟨mul⟩

lemma mul_zero (m : mynat) : m * 0 = 0 := rfl

lemma mul_succ (m n : mynat) : m * (succ n) = m * n + m := rfl

lemma add_zero (m : mynat) : m + 0 = m := rfl

----------------------------------------

-- The proof in tactic mode
lemma zero_mul (m : mynat) : 0 * m = 0 :=
begin
induction m,
{
-- Q0: Why do I need this extra line compared to in http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=3&level=1
  rw mynat_zero_eq_zero,
  rw mul_zero 0,
},
{
  rw mul_succ 0,
  rw add_zero (0 * m_n),
  rw m_ih,
}
end

-- The proof of a forall version of the lemma
-- ported from https://leanprover-community.github.io/mathlib_docs/core/init/data/nat/lemmas.html#nat.zero_mul
-- Q1: Why does it need an extra refl than the original proof?
lemma zero_mul_forall : ∀ (m : mynat), 0 * m = 0
| 0        := rfl
| (succ m) := begin
  rw [mul_succ, zero_mul_forall],
  refl
end

lemma zero_mul_forall_match : ∀ (m : mynat),  0 * m = 0
| zero :=
calc zero * zero
    = 0 * 0 : by rw mynat_zero_eq_zero
... = 0 : by rw mul_zero 0
| n@(succ m_n) :=
calc 0 * (succ m_n)
    = 0 * m_n + 0 : by rw mul_succ
... = 0 * m_n : by rw add_zero (0 * m_n)
... = 0 : by rw zero_mul_forall_match m_n

-- Q2: how can I refer to the lemma itself in the match proof at <marker>
lemma zero_mul_match (m : mynat) : 0 * m = 0 :=
match m with
| zero :=
calc zero * zero
    = 0 * 0 : by rw mynat_zero_eq_zero
... = 0 : by rw mul_zero 0
| n@(succ m_n) :=
calc 0 * (succ m_n)
    = 0 * m_n + 0 : by rw mul_succ
... = 0 * m_n : by rw add_zero (0 * m_n)
... = 0 : by sorry -- <marker>
end

lemma zero_mul_induction_zero : 0 * zero = 0 := rfl

lemma zero_mul_induction_m_n : ∀ (n : mynat), 0 * n = 0 → 0 * n.succ = 0 :=
λ m_n h, add_zero (0 * m_n) ▸ mul_succ 0 m_n ▸ h

-- Q3: Why `add_zero` is no longer needed?
lemma zero_mul_induction_m_n' : ∀ (n : mynat), 0 * n = 0 → 0 * n.succ = 0 :=
λ m_n h, mul_succ 0 m_n ▸ h

-- Q4: Why lean doesn't accept this
lemma zero_mul_rec (m : mynat) : 0 * m = 0 :=
m.rec_on zero_mul_induction_zero zero_mul_induction_m_n
/-
type mismatch at application
  m.rec_on zero_mul_induction_zero zero_mul_induction_m_n
term
  zero_mul_induction_m_n
has type
  ∀ (n : mynat), 0 * n = 0 → 0 * n.succ = 0
but is expected to have type
  ∀ (n : mynat), 0 * zero = n → 0 * zero = n.succ
-/

end mynat

[Johan Commelin]

@Utensil Song the rw in NNG is different from therw in mathlib. The one in mathlib automatically tries refl at the end. I guess that answers Q1.

[Utensil Song]

Thanks! I've also just added a Q0.

[Johan Commelin]

Q2: I think you can not (elegantly) refer to the lemma itself...

[Johan Commelin]

This is a known shortcoming of match.

[Utensil Song]

But in the zero_mul_forall_match version I can refer to it, and I can't find the explanation of this (whether doc or code).

[Mario Carneiro]

Writing recursive proofs in this style is characteristic of those coming from Coq. In lean you use the equation compiler instead, which is just as powerful but is sometimes limited by the fact that it only works at the top level of a definition

[Mario Carneiro]

That is, Lean obligates you to write zero_mul_match like this:

lemma zero_mul_match : ∀ (m : mynat), 0 * m = 0
| zero :=
calc zero * zero
    = 0 * 0 : by rw mynat_zero_eq_zero
... = 0 : by rw mul_zero 0
| n@(succ m_n) :=
calc 0 * (succ m_n)
    = 0 * m_n + 0 : by rw mul_succ
... = 0 * m_n : by rw add_zero (0 * m_n)
... = 0 : zero_mul_match m_n

[Utensil Song]

Thanks, @Mario Carneiro , but how can I use the equation compiler in this case? And I could not find a good doc of equation compiler.

[Utensil Song]

So the \forall in the lemma is inevitable and the only viable practice in Lean?

[Mario Carneiro]

The type of the lemma is the same in both cases

[Mario Carneiro]

there is no external difference between T (foo : bar) : baz and T : \forall (foo : bar), baz

[Mario Carneiro]

However within the definition it distinguishes between the variables that are allowed to change during the recursion and those that are fixed parameters

[Mario Carneiro]

So if you want to do a recursive call with a different value of m_n, you have to put it "right of the colon"

[Utensil Song]

I see(from "distinguishes between the variables that are allowed to change during the recursion and those that are fixed parameters", the former has to be "right of the colon").

[Mario Carneiro]

When you write a lemma without the equation compiler, that is, in theorem foo ... : ... := ... form, then it is not allowed to be recursive at all, and references to foo will be resolved as if foo doesn't exist yet

[Utensil Song]

By "could not find a good doc of equation compiler", no doc I found explains the . in the following while I once noticed this in Zulip that's also part of the equation compiler:

example (n : ℕ) : nat.succ n ≠ 0.

[Mario Carneiro]

That's an empty match

[Kevin Buzzard]

Q0: The natural number game is not pure lean, I modified the induction tactic so it did the rewrite for you.

[Mario Carneiro]

because nat.succ n and 0 are distinct constructors, when you pattern match rfl against the equality, you find there are no cases to handle, and so an empty proof works

[Mario Carneiro]

Note that the equation compiler sees that goal as \forall (h : nat.succ n = 0), false and effectively does | rfl := <wait a minute, this doesn't typecheck>

[Kevin Buzzard]

Q3 because add_zero is true by definition

[Mario Carneiro]

from a foundational POV, it's totally a circular proof, we are proving that succ is not zero by appeal to the fact that the equation compiler knows that succ is not zero because it proved it somewhere internally

[Kevin Buzzard]

Q4 read the error message

[Utensil Song]

@Mario Carneiro Isee, but the reference and doc I found seems to be not MECE enough to address this part of the behavior of the equation compiler.

[Utensil Song]

Kevin Buzzard said:

Q3 because add_zero is true by definition

But in the game, it seems that I do need it.

[Mario Carneiro]

MECE?

[Utensil Song]

@Kevin Buzzard So your answer to Q0 is my assumption, and it kind of contradicts with Q3, Q0 is more automation and Q3 is less.

[Kevin Buzzard]

In the game you can prove add_zero by rfl if you like and I modified rw so it wouldn't close definitional equality goals directly afterwards because I don't emphasise the non-mathematical concept of definitional equality in a game targeting mathematicians

[Utensil Song]

Mario Carneiro said:

MECE?

MECE stands for "both mutually exclusive and collectively exhaustive".

[Mario Carneiro]

There are 0 cases, they are obviously mutually exclusive, and they are collectively exhaustive because there are no valid cases

[Utensil Song]

For ., yes. But I mean for all the syntax that equation compiler supports...

[Mario Carneiro]

In general you provide it with more cases using | bla := ... syntax

[Mario Carneiro]

I have no idea what the docs say about the equation compiler. You are probably right that they are lacking

[Shing Tak Lam]

For Q4, it works if you replace m.rec_on with mynat.rec_on m. I don't know why though...

[Mario Carneiro]

You can't use projection notation with @[elab_as_eliminator] functions

[Mario Carneiro]

I doubt this is for any very good reason, but if I had to take a guess it would be that the use of projection notation delays the determination and typechecking of the function and you end up typechecking the arguments with the wrong type

[Utensil Song]

Kevin Buzzard said:

In the game you can prove add_zero by rfl if you like and I modified rw so it wouldn't close definitional equality goals directly afterwards because I don't emphasise the non-mathematical concept of definitional equality in a game targeting mathematicians

I see, so the intention probably is not to distract the newcomers with the boring mynat_zero_eq_zero and not to allow them to rely on smarter rw . I'm easily puzzled by seemingly conflicting intentions of the invisible designer of the behaviours of the code hence the question.

[Mario Carneiro]

If you think this way, then I would suggest working from the ground up, and understand dependent type theory, and then expand that to how elaboration makes things easier to write and how tactics automate the construction of terms

[Mario Carneiro]

#tpil is a good source for this order of learning

[Mario Carneiro]

NNG is more for people who prefer playing games and learning the rules as they go

[Utensil Song]

Mario Carneiro said:

If you think this way, then I would suggest working from the ground up, and understand dependent type theory, and then expand that to how elaboration makes things easier to write and how tactics automate the construction of terms

:+1: My path is sort of non-linear: "The Hitchhiker's Guide to Lean" -> "TPIL" -> "Logic and Proof" -> "Reading doc, mathlib code and Zulip" -> "NGN" (rewrite stuff in it to prepare for other games), so I know some basics of the ground and trying to have a coherent mental model when I encounter some seemingly weird behaviors.

[Utensil Song]

Mario Carneiro said:

You can't use projection notation with @[elab_as_eliminator] functions

No @[elab_as_eliminator has been specified for the rec_on of mynat, it seems?

[Utensil Song]

Also I never found the code of rec_on, I kind of assumed that it's a built-in method for inductive types.

[Utensil Song]

Kevin Buzzard said:

Q4 read the error message

The exact question is that the type requested by the first argument seems to be volatile.

I came up with the type 0 * zero = 0 of zero_mul_induction_zero by doing m.rec_on _ sorry and hover on _, but after I did the same for the second argument so that I have

lemma zero_mul_rec'' (m : mynat) : 0 * m = 0 :=
m.rec_on zero_mul_induction_zero zero_mul_induction_m_n

Lean complains that the first argument should be 0 * zero = n instead (against its own hint) but the proposition can't be true since there's no way 0 * 0 = n.

It smells like a bug.

[Kevin Buzzard]

Sorry, I misunderstood initially. I've had problems using projection notation with recursors before, I think also there are issues with list. As for the design of the game, I wanted mathematicians not to have to think at all about notation and I wanted them to learn about rewriting and equational reasoning, and after extensive testing amongst mathematics undergraduates at Imperial College so I changed the behaviour of the induction and rewrite tactics so they behaved in a way which mathematicians with no background in type theory found less confusing

[Utensil Song]

Thanks for the clarification, it all makes sense to me now. (The question is only raised after I did a few times of "add rw mynat_zero_eq_zero, at the beginning" and "remove refl" at the end during copying my solutions to a standalone lean file and making it type check).

[Utensil Song]

Also, having to explicitly write down refl when having the expectation of defeq as "press the same buttons on your computer in the same order" equal is indeed less confusing.

[Kevin Buzzard]

Yes that was the problem, non-syntactically equal defeq equality goals were being randomly closed after a rw.

[Utensil Song]

Just for fun, here's another story related to a similar trust crisis with Lean.

A while ago, I (who hadn't written a line of Lean code by the time) copy-pasted the following code from the default code in https://leanprover-community.github.io/lean-web-editor/

example (m n : ℕ) : m + n = n + m :=
by simp

and Lean fails to unify. You can imagine how I feel at the moment.

It took me quite some time to make Lean happy, but by cc. And sometime later, I simplified it to something I understand: by simp [add_comm]. Eventually, I reduced it to by apply add_comm.

And by accident, I noticed the changelog https://github.com/leanprover-community/lean/blob/master/doc/changes.md#v360c-26-feb-2020

and that's when I know the breaking change of removing lemmas about commutativity from simp default set.

I'm glad to see that this issue is now fixed on the online editor (I should have reported it back then but somehow I didn't, sorry)

[Kevin Buzzard]

We do the best we can, the lean prover community is run by volunteers. We believe in the potential of the software and are trying hard to juggle many projects such as running the website, the web editor, the installer including auto-downloading of mathlib oleans -- there is a lot of work being done, and of course on top of that is the constant stream of PR's. In some sense you're observing here that the project is expanding.

[Utensil Song]

Yes, I'm very grateful for the efforts of whole community. Sorry if the story sounds disrespect for that. The warm side of the story is that by reading many conversations happening in Zulip, the trust is fully recovered and strengthened.

[Pedro Sánchez Terraf]

Hi there, I'm new here (I followed the etiquette rule of --briefly!-- introducing myself in a topic; idk if I should wait for replies there before making noise here, but anyway). Today I started playing the Natural Number Game and I wondered if there was chance to save the all the code I've written there (not much, but to save me the trouble of navigating each screen).

[Heather Macbeth]

Whether or not it's possible (I'm not sure), did you realise that the game allows you to skip levels? So you can go directly to where you left off even if you don't have the nice node colouring :)

[Scott Morrison]

It should just automatically save progress in your browser.

[Heather Macbeth]

Welcome, btw! I switched from Coq a few months ago, nice to hear there are some Lean-curious Isabelle folks.

[Pedro Sánchez Terraf]

@Heather Macbeth @Scott Morrison thank you both! I'm aware of this, I just wanted to download my progress.

[Scott Morrison]

I think copy and paste into a editor is a solution. My son was playing for a while, before the browser caching arrived, and didn't like losing his progress so we copied and pasted. :-)

Alternatively, you can download the natural numbers game as a bunch of Lean files, and "work locally", although we'd have to ping someone for instructions.

[Pedro Sánchez Terraf]

@Scott Morrison Thanks again, c&p was the solution I was trying to avoid :-) For a while, I'm not able to run Lean on my laptop because of compatibility issues (my distro is too old, and I'm not at a good moment for a dist-upgrade).

[Pedro Sánchez Terraf]

@Heather Macbeth I'm a quite non-typical Isabelle user... I've been working fully in Isabelle/ZF. But I'm deeply in love with declarative proof style.

[Rene Recktenwald]

I'm stuck in the Natural Numbers game. Advanced Addition World Level 8. I have to show a+b=a implies b=0.
So I use

intro h,
rw ← add_zero a at h,

This leaves me at

a b : mynat,
h : a + 0 + b = a + 0
⊢ b = 0

But I cannot figure out how to use add_left_cancel to get rid of the a in the hypothesis.
Any hints would be appreciated.

[Kevin Buzzard]

The hypothesis says (a+0)+b=a+0 so you can't use add_left_cancel on it yet

[Kevin Buzzard]

I would love to know how to switch the brackets on so people can see where they really are, but apparently there's no easy way of doing this

[Rene Recktenwald]

I have tried using rw add_assoc at h, first, but still couldn't figure out how to proceed

[Rene Recktenwald]

if I have a hypothesis h : H and a function H->J how do I get a j in my stack of things I can use in general?

[Kevin Buzzard]

If h : H and f : H \to J then you can do let j := f h if J is a type, or have j := f h if J is a true/false statement

[Rene Recktenwald]

Hmm ok I'll see if I can proceed in my level via this.
by the way thanks for providing the natural number game =)

[Kevin Buzzard]

intro h,
rw ← add_zero a at h,
rw add_assoc at h,
have h2 := add_left_cancel _ _ _ h,

works

[Kevin Buzzard]

add_left_cancel is a function. It takes four inputs. The first three are numbers, and the last one is a proof.

[Kevin Buzzard]

I wrote the game for my students but I'm glad you're enjoying it too.

[Kevin Buzzard]

mynat.add_left_cancel : ∀ (t a b : mynat), t + a = t + b → a = b

It eats t, a, b, and then a proof that t+a=t+b, and it spits out a proof that a=b

[Rene Recktenwald]

Well Johan recommended it, when I was still in Freiburg, and I'm finally taking the time to dig into lean

[Rene Recktenwald]

Thank you for the help!

[Kevin Buzzard]

It's what #new members is for

[Johan Commelin]

@Rene Recktenwald Good to see you again :smiley:

[Rene Recktenwald]

@Johan Commelin Haha and I'm back once more =D Stuck on Inequality World Level 9 this time. Having to prove a \leq b or b\leq a.
I think I want to do induction on a, but then my induction hyp is a<=b or b<=a, and I would like to split this into two goals, one where I have just a<=b and the other where I have just b<=a, but I don't know how to do it.

[Kevin Buzzard]

You can split an or with cases

[Rene Recktenwald]

Ah yeah, I thought I had tried that but I must have made a mistake. Thanks once more :)

[Rene Recktenwald]

Hmm to be honest I'm still stuck. If I have $a\leq b$ as a hypothesis, is there a way to do cases on the $c$? My current goal is

b a : mynat,
hi : ∃ (c : mynat), b = a + c
⊢ succ a ≤ b ∨ b ≤ succ a

[Kevin Buzzard]

you don't have the c

[Kevin Buzzard]

so you can't do cases on it yet.

[Rene Recktenwald]

can I do something akin to use c at hi ?

[Kevin Buzzard]

In Lean, you have hypotheses, and goals. You want to use hypotheses, and solve goals.

[Kevin Buzzard]

But the logic of a hypothesis and of a goal are completely different. For example if you have a hypothesis hPQ : P -> Q, you can make progress if you have a hypothesis hP : P, but you can't use it if you have a hypothesis hq : Q. You could use if it you have a goal ⊢ Q but you can't use it if you have a goal ⊢ P.

[Kevin Buzzard]

Abstractly, what's going on is that things like "exists c, ..." and "P and Q", and all the other things, have constructors and eliminators.

[Kevin Buzzard]

If your _goal_ is "P and Q", then you are going to need a tactic which comes up with a constructor for "P and Q". The split tactic does this for you.

[Kevin Buzzard]

If you have a _hypothesis_ "P and Q" then you're going to need a tactic which comes up with an eliminator for "P and Q", because you have it, and you want to use it, so you want to turn it into other things. The cases tactic does this for you.

[Kevin Buzzard]

What I'm saying is that if you see an "exists" statement, and you want to work on that statement, then what you next very much depends on whether that statement is a hypothesis, or a goal, because the logic is completely different in the two situations.

[Kevin Buzzard]

The use tactic is the tactic which makes a constructor for "exists", so it's useful if the _goal_ is "exists".

[Kevin Buzzard]

But you need an eliminator for exists -- you have a proof that something exists, and you want to get to the something.

[Kevin Buzzard]

So use can never work, because all use does it that it makes proofs of "exists c, ...". You have a proof already, and you want to use that proof elsewhere.

[Kevin Buzzard]

So use a tactic which deconstructs existing data, like cases.

[Rene Recktenwald]

ok so I do cases on the hi and then this gives me access to the c, which I can then do cases on once more?

[Kevin Buzzard]

right

[Kevin Buzzard]

If h : A \and B then h is a term which has internally been constructed from a pair of terms -- a proof of A and a proof of B. cases will get to those terms for you.

[Kevin Buzzard]

If h : exists c, P(c) then h is a term which has been internally constructed from a pair of terms -- a natural c, and a proof of P(c). And cases h will again get to those terms for you.

[Kevin Buzzard]

"and" and "exists" are structures -- inductive types with one constructor.

[Kevin Buzzard]

in general, if you do cases on a term of an inductive type with n constructors, you will end up with n goals. This is why if you do cases on A or B, or on a natural number, you get two goals.

[Rene Recktenwald]

Ok thank you so much, I got it now. But I will revisit it later, because I used what we have to prove in Level 10 for level 9 already =D I want to find the better way

[Kevin Buzzard]

I can't guarantee there's a better way -- parts of the game are not very well-organised.

[Johan Commelin]

The real answer should be that we should write proper docstrings for \exists and friends that tell you which tactics you can use to (de)construct them... but we're somewhat stuck on deciding whether we add those docstrings in core or in mathlib.

[Julian Berman]

FWIW having recently done NNG the one thing I found quite nice to have at my side (which wasn't already mentioned within NNG) was the 1-sheeter tactic cheat sheet

[Julian Berman]

https://leanprover-community.github.io//img/lean-tactics.pdf this one -- @Rene Recktenwald maybe that'd help

[Julian Berman]

(it at least for me reinforced the "you need different tactics when things appear in goals vs. hypotheses" idea)

[Rene Recktenwald]

Oh that's so cool, thanks

[Bryan Gin-ge Chen]

Johan Commelin said:

The real answer should be that we should write proper docstrings for \exists and friends that tell you which tactics you can use to (de)construct them... but we're somewhat stuck on deciding whether we add those docstrings in core or in mathlib.

I think we were fine with adding them to core in lean#296, but I wanted to make sure the docstrings that referenced mathlib tactics made it clear that mathlib was required and how to import them.

[Johan Commelin]

@Bryan Gin-ge Chen can we add stubs to core, and overwrite them in mathlib with more extensive versions?

[Bryan Gin-ge Chen]

Good question. Is there a function that replaces docstrings rather than just adds them?

I'm not opposed to the idea but it seems like it could be more work for marginal benefit.