Zulip Chat Archive

Stream: new members

Topic: Natural Numbers Game


view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:09):

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.

view this post on Zulip Patrick Massot (Mar 14 2020 at 11:20):

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;

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:35):

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)

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:39):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:39):

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.

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:40):

OK, thanks very much

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:40):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:41):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:41):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:42):

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".

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:43):

Kevin Buzzard said:

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

Sorry, yes - this is true

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:43):

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

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:43):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:43):

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

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:45):

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

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:45):

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.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:47):

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.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:48):

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.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:49):

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).

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:50):

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

view this post on Zulip Patrick Stevens (Mar 14 2020 at 11:50):

Thanks very much

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 11:54):

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.

view this post on Zulip Daniel Keys (Mar 14 2020 at 17:58):

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.

view this post on Zulip Shing Tak Lam (Mar 15 2020 at 06:34):

@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

view this post on Zulip Shing Tak Lam (Mar 15 2020 at 06:36):

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 :)

view this post on Zulip Daniel Keys (Mar 15 2020 at 13:42):

@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.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 13:44):

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 :-)

view this post on Zulip Daniel Keys (Mar 15 2020 at 13:58):

@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!-:)

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 13:59):

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

view this post on Zulip Patrick Stevens (Mar 15 2020 at 14:08):

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

view this post on Zulip Filip Szczepański (Apr 10 2020 at 05:32):

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

view this post on Zulip Johan Commelin (Apr 10 2020 at 05:36):

It seems to be the one everyone gets stuck on.

view this post on Zulip Filip Szczepański (Apr 10 2020 at 05:52):

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

view this post on Zulip Johan Commelin (Apr 10 2020 at 05:52):

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

view this post on Zulip Filip Szczepański (Apr 10 2020 at 05:57):

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

view this post on Zulip Filip Szczepański (Apr 10 2020 at 05:58):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 06:05):

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:

view this post on Zulip Filip Szczepański (Apr 10 2020 at 06:06):

Oh, to get the forall?

view this post on Zulip Filip Szczepański (Apr 10 2020 at 06:07):

I should have taken that advice more literally

view this post on Zulip Filip Szczepański (Apr 10 2020 at 06:14):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 06:17):

backtrack

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 06:33):

Unless your hypothesis are contradictory

view this post on Zulip Mario Carneiro (Apr 10 2020 at 06:35):

then your goal isn't false, is it

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 06:37):

Depends how literally you interpret the statement

view this post on Zulip undef (Apr 10 2020 at 10:55):

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?

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 10:58):

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

view this post on Zulip undef (Apr 10 2020 at 11:00):

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

view this post on Zulip undef (Apr 10 2020 at 11:01):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 11:31):

Sorry, real life intervened

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 11:32):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 11:33):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 11:33):

For example add_succ is true by definition and succ_add is not

view this post on Zulip undef (Apr 10 2020 at 11:38):

Thank you, I will investigate that!

view this post on Zulip Moses Schönfinkel (Apr 10 2020 at 11:44):

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.

view this post on Zulip Moses Schönfinkel (Apr 10 2020 at 11:46):

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".

view this post on Zulip undef (Apr 10 2020 at 12:00):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 12:06):

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.

view this post on Zulip Patrick Massot (Apr 10 2020 at 12:07):

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).

view this post on Zulip Patrick Massot (Apr 10 2020 at 12:08):

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.

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 12:09):

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

view this post on Zulip Patrick Massot (Apr 10 2020 at 12:09):

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.

view this post on Zulip Patrick Massot (Apr 10 2020 at 12:09):

But NNG is all about foundations.

view this post on Zulip Patrick Massot (Apr 10 2020 at 12:10):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 12:11):

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

view this post on Zulip Filip Szczepański (Apr 10 2020 at 15:32):

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)

view this post on Zulip Nam (Apr 12 2020 at 05:46):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:47):

those two are defeq

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:47):

the connective is “and”.

view this post on Zulip Nam (Apr 12 2020 at 05:47):

oh, they are defeq. i see.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:47):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:48):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:48):

actually they aren't for nat

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:48):

but maybe they are for mynat or whatever NNG uses?

view this post on Zulip Nam (Apr 12 2020 at 05:50):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 06:02):

They're defeq in nng

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:03):

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?

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:05):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:05):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:09):

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?

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:10):

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:11):

so

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:11):

Aah! But

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:12):

exactly!

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:12):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:13):

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:13):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:14):

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:15):

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:16):

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.

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:16):

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.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:17):

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.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:19):

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.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:20):

Thanks for the comment :-)

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:22):

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

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:22):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 20:22):

: O

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:22):

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

view this post on Zulip Sam Raleigh (Apr 23 2020 at 21:52):

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?

view this post on Zulip orlando (Apr 23 2020 at 22:23):

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.

view this post on Zulip Aniruddh Agarwal (Apr 23 2020 at 23:53):

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

view this post on Zulip Sam Raleigh (Apr 24 2020 at 00:19):

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.

view this post on Zulip Alex J. Best (Apr 24 2020 at 00:23):

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.

view this post on Zulip Alex J. Best (Apr 24 2020 at 00:25):

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.

view this post on Zulip Alex J. Best (Apr 24 2020 at 00:33):

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.

view this post on Zulip Alex J. Best (Apr 24 2020 at 00:34):

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

view this post on Zulip Sam Raleigh (Apr 24 2020 at 01:45):

Thanks!

view this post on Zulip edderiofer (May 12 2020 at 21:07):

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?

view this post on Zulip Mario Carneiro (May 12 2020 at 21:15):

have := hd _ h

view this post on Zulip Mario Carneiro (May 12 2020 at 21:15):

or exact hd _ h if it's your goal

view this post on Zulip Mario Carneiro (May 12 2020 at 21:16):

or apply hd, apply h

view this post on Zulip edderiofer (May 12 2020 at 21:17):

Hooray! Thanks!

view this post on Zulip edderiofer (May 13 2020 at 01:04):

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

view this post on Zulip edderiofer (May 13 2020 at 01:04):

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

view this post on Zulip Sam Lichtenstein (May 13 2020 at 01:22):

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

view this post on Zulip edderiofer (May 13 2020 at 01:23):

Ah, yes.

view this post on Zulip Jalex Stark (May 13 2020 at 01:25):

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

view this post on Zulip edderiofer (May 13 2020 at 01:31):

Ah, that's handy. Lemme check.

view this post on Zulip edderiofer (May 13 2020 at 01:32):

Yep, it does! :D

view this post on Zulip edderiofer (May 13 2020 at 01:32):

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

view this post on Zulip Jalex Stark (May 13 2020 at 01:32):

Good night, see you around!

view this post on Zulip Sam Lichtenstein (May 13 2020 at 13:15):

@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

view this post on Zulip Patrick Massot (May 13 2020 at 13:33):

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

view this post on Zulip Patrick Massot (May 13 2020 at 13:33):

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

view this post on Zulip Alexandre Rademaker (May 25 2020 at 23:20):

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?

view this post on Zulip Mario Carneiro (May 25 2020 at 23:21):

link please

view this post on Zulip Mario Carneiro (May 25 2020 at 23:22):

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

view this post on Zulip Alexandre Rademaker (May 25 2020 at 23:23):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:23):

that seems unlikely

view this post on Zulip Mario Carneiro (May 25 2020 at 23:23):

link please

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:24):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:24):

Do we have a linkifier for this?

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:25):

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

view this post on Zulip Alexandre Rademaker (May 25 2020 at 23:25):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:25):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:26):

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

view this post on Zulip Alexandre Rademaker (May 25 2020 at 23:26):

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 },
...

view this post on Zulip Mario Carneiro (May 25 2020 at 23:26):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:27):

Yeah that is puzzling!

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:27):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:27):

no

view this post on Zulip Mario Carneiro (May 25 2020 at 23:27):

assuming you didn't change it in NNG

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:28):

then this must be a glitch in the matrix

view this post on Zulip Mario Carneiro (May 25 2020 at 23:28):

where's the source for the NNG tactic setup

view this post on Zulip Alex J. Best (May 25 2020 at 23:28):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:28):

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

view this post on Zulip Alexandre Rademaker (May 25 2020 at 23:29):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:29):

Yup...

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:30):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:30):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 23:30):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:34):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:36):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 23:41):

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

view this post on Zulip Alexandre Rademaker (May 26 2020 at 00:31):

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

view this post on Zulip Bryan Gin-ge Chen (May 26 2020 at 00:34):

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.)

view this post on Zulip Kevin Buzzard (May 26 2020 at 07:25):

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

view this post on Zulip Alexandre Rademaker (May 28 2020 at 20:05):

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?

view this post on Zulip Alexandre Rademaker (May 28 2020 at 21:36):

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?...

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 21:57):

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

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 21:59):

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

view this post on Zulip Alexandre Rademaker (May 28 2020 at 22:09):

the tactic tauto is from mathlib, right?

view this post on Zulip Utensil Song (Jun 06 2020 at 09:00):

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

view this post on Zulip Johan Commelin (Jun 06 2020 at 09:06):

@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.

view this post on Zulip Utensil Song (Jun 06 2020 at 09:08):

Thanks! I've also just added a Q0.

view this post on Zulip Johan Commelin (Jun 06 2020 at 09:08):

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

view this post on Zulip Johan Commelin (Jun 06 2020 at 09:08):

This is a known shortcoming of match.

view this post on Zulip Utensil Song (Jun 06 2020 at 09:09):

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).

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:10):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:11):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:11):

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.

view this post on Zulip Utensil Song (Jun 06 2020 at 09:12):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:12):

The type of the lemma is the same in both cases

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:13):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:13):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:14):

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"

view this post on Zulip Utensil Song (Jun 06 2020 at 09:17):

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").

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:18):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:19):

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.

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:20):

That's an empty match

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 09:20):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:21):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:22):

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>

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 09:23):

Q3 because add_zero is true by definition

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:24):

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

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 09:24):

Q4 read the error message

view this post on Zulip Utensil Song (Jun 06 2020 at 09:24):

@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.

view this post on Zulip Utensil Song (Jun 06 2020 at 09:25):

Kevin Buzzard said:

Q3 because add_zero is true by definition

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:25):

MECE?

view this post on Zulip Utensil Song (Jun 06 2020 at 09:26):

@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.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 09:27):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:27):

Mario Carneiro said:

MECE?

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:28):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:29):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:30):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:31):

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

view this post on Zulip Shing Tak Lam (Jun 06 2020 at 09:32):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:32):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:34):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:35):

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.

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:37):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:39):

#tpil is a good source for this order of learning

view this post on Zulip Mario Carneiro (Jun 06 2020 at 09:39):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 09:44):

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.

view this post on Zulip Utensil Song (Jun 06 2020 at 09:46):

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?

view this post on Zulip Utensil Song (Jun 06 2020 at 09:47):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 10:02):

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.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 10:23):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 10:27):

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).

view this post on Zulip Utensil Song (Jun 06 2020 at 10:30):

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.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 10:39):

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

view this post on Zulip Utensil Song (Jun 06 2020 at 10:47):

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)

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 10:53):

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.

view this post on Zulip Utensil Song (Jun 06 2020 at 11:00):

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.

view this post on Zulip Pedro Sánchez Terraf (Aug 04 2020 at 21:52):

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).

view this post on Zulip Heather Macbeth (Aug 04 2020 at 23:05):

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 :)

view this post on Zulip Scott Morrison (Aug 04 2020 at 23:07):

It should just automatically save progress in your browser.

view this post on Zulip Heather Macbeth (Aug 04 2020 at 23:07):

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

view this post on Zulip Pedro Sánchez Terraf (Aug 04 2020 at 23:43):

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 23:44):

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.

view this post on Zulip Pedro Sánchez Terraf (Aug 04 2020 at 23:47):

@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).

view this post on Zulip Pedro Sánchez Terraf (Aug 04 2020 at 23:50):

@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.

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:42):

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.

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:49):

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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:50):

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

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:51):

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

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:52):

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?

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:53):

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

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:54):

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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:55):

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

works

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:55):

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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:55):

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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:56):

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

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:57):

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

view this post on Zulip Rene Recktenwald (Sep 06 2020 at 22:57):

Thank you for the help!

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 22:58):

It's what #new members is for

view this post on Zulip Johan Commelin (Sep 07 2020 at 04:18):

@Rene Recktenwald Good to see you again :smiley:

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 10:06):

@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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 10:21):

You can split an or with cases

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 10:28):

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

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 11:12):

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

b a : mynat,
hi :  (c : mynat), b = a + c
 succ a  b  b  succ a

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:13):

you don't have the c

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:13):

so you can't do cases on it yet.

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 11:22):

can I do something akin to use c at hi ?

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:23):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:24):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:25):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:26):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:27):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:28):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:28):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:29):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:29):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:30):

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

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 11:32):

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?

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:32):

right

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:32):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:33):

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.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:33):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:34):

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.

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 11:41):

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

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 11:47):

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

view this post on Zulip Johan Commelin (Sep 19 2020 at 13:02):

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.

view this post on Zulip Julian Berman (Sep 19 2020 at 14:44):

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

view this post on Zulip Julian Berman (Sep 19 2020 at 14:45):

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

view this post on Zulip Julian Berman (Sep 19 2020 at 14:46):

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

view this post on Zulip Rene Recktenwald (Sep 19 2020 at 16:05):

Oh that's so cool, thanks

view this post on Zulip Bryan Gin-ge Chen (Sep 19 2020 at 16:22):

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.

view this post on Zulip Johan Commelin (Sep 19 2020 at 16:47):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 19 2020 at 16:57):

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.


Last updated: May 12 2021 at 22:15 UTC