## Stream: new members

### Topic: Natural Numbers Game

#### 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]
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,
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,
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 (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;

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

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

namespace mynat

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

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

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

begin [nat_num_game]
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,
exact f,
rw (add_comm (succ a) b) at f,
injection f,
rw (add_comm' b a) at h_1,
sorry
end


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

#### Patrick Stevens (Mar 14 2020 at 11:40):

OK, thanks very much

#### 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,
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 (Mar 14 2020 at 11:41):

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

#### Kevin Buzzard (Mar 14 2020 at 11:41):

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

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

#### 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

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

#### Patrick Stevens (Mar 14 2020 at 11:43):

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

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

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

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

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

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

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

#### 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

Thanks very much

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

#### 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

#### Shing Tak Lam (Mar 15 2020 at 06:36):

Basically just Kevin's answers to my questions :)

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

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

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

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

#### Patrick Stevens (Mar 15 2020 at 14:08):

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

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

#### Johan Commelin (Apr 10 2020 at 05:36):

It seems to be the one everyone gets stuck on.

#### Filip Szczepański (Apr 10 2020 at 05:52):

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

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

#### 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


#### 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

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

#### Filip Szczepański (Apr 10 2020 at 06:06):

Oh, to get the forall?

#### Filip Szczepański (Apr 10 2020 at 06:07):

I should have taken that advice more literally

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

backtrack

#### Mario Carneiro (Apr 10 2020 at 06:35):

then your goal isn't false, is it

#### Kevin Buzzard (Apr 10 2020 at 06:37):

Depends how literally you interpret the statement

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

#### 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

#### undef (Apr 10 2020 at 11:00):

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

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

#### Kevin Buzzard (Apr 10 2020 at 11:31):

Sorry, real life intervened

#### 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

#### 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

#### undef (Apr 10 2020 at 11:38):

Thank you, I will investigate that!

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

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

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

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

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

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

#### Kevin Buzzard (Apr 10 2020 at 12:09):

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

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

#### Patrick Massot (Apr 10 2020 at 12:09):

But NNG is all about foundations.

#### Patrick Massot (Apr 10 2020 at 12:10):

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

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

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

#### Nam (Apr 12 2020 at 05:46):

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

#### Mario Carneiro (Apr 12 2020 at 05:47):

those two are defeq

#### Kenny Lau (Apr 12 2020 at 05:47):

the connective is “and”.

#### Nam (Apr 12 2020 at 05:47):

oh, they are defeq. i see.

#### 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

#### Kenny Lau (Apr 12 2020 at 05:48):

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

#### Mario Carneiro (Apr 12 2020 at 05:48):

actually they aren't for nat

#### Mario Carneiro (Apr 12 2020 at 05:48):

but maybe they are for mynat or whatever NNG uses?

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

#### Kevin Buzzard (Apr 12 2020 at 06:02):

They're defeq in nng

#### 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,
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 (Apr 23 2020 at 20:05):

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

#### Sam Raleigh (Apr 23 2020 at 20:05):

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

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

#### Kevin Buzzard (Apr 23 2020 at 20:10):

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


#### Kevin Buzzard (Apr 23 2020 at 20:11):

so

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


#### Kevin Buzzard (Apr 23 2020 at 20:11):

Aah! But

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


exactly!

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

#### 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

#### 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

#### Sam Raleigh (Apr 23 2020 at 20:14):

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

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

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

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

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

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

#### Kevin Buzzard (Apr 23 2020 at 20:20):

Thanks for the comment :-)

#### 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

#### Kevin Buzzard (Apr 23 2020 at 20:22):

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

: O

#### 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

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

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

#### 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

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

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

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

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

#### Alex J. Best (Apr 24 2020 at 00:34):

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

Thanks!

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

#### Mario Carneiro (May 12 2020 at 21:15):

have := hd _ h

#### Mario Carneiro (May 12 2020 at 21:15):

or exact hd _ h if it's your goal

#### Mario Carneiro (May 12 2020 at 21:16):

or apply hd, apply h

Hooray! Thanks!

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

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

#### 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

Ah, yes.

#### 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

#### edderiofer (May 13 2020 at 01:31):

Ah, that's handy. Lemme check.

Yep, it does! :D

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

#### Jalex Stark (May 13 2020 at 01:32):

Good night, see you around!

#### 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

#### Patrick Massot (May 13 2020 at 13:33):

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

#### Patrick Massot (May 13 2020 at 13:33):

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

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

#### 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

#### Alexandre Rademaker (May 25 2020 at 23:23):

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

#### Mario Carneiro (May 25 2020 at 23:23):

that seems unlikely

#### 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!

#### Mario Carneiro (May 25 2020 at 23:24):

Do we have a linkifier for this?

#### Alexandre Rademaker (May 25 2020 at 23:25):

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

#### 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

#### Mario Carneiro (May 25 2020 at 23:26):

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

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


#### 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

#### Kevin Buzzard (May 25 2020 at 23:27):

Yeah that is puzzling!

#### Kevin Buzzard (May 25 2020 at 23:27):

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

no

#### Mario Carneiro (May 25 2020 at 23:27):

assuming you didn't change it in NNG

#### Kevin Buzzard (May 25 2020 at 23:28):

then this must be a glitch in the matrix

#### Mario Carneiro (May 25 2020 at 23:28):

where's the source for the NNG tactic setup

#### Alex J. Best (May 25 2020 at 23:28):

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

#### 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

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

Yup...

#### Kevin Buzzard (May 25 2020 at 23:30):

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

#### Mario Carneiro (May 25 2020 at 23:30):

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

#### 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

#### 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

#### 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

#### Mario Carneiro (May 25 2020 at 23:41):

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

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

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

#### 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

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

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

#### 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

#### Alexandre Rademaker (May 28 2020 at 22:09):

the tactic tauto is from mathlib, right?

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

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

#### Utensil Song (Jun 06 2020 at 09:08):

Thanks! I've also just added a Q0.

#### Johan Commelin (Jun 06 2020 at 09:08):

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

#### Johan Commelin (Jun 06 2020 at 09:08):

This is a known shortcoming of match.

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

#### 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

#### 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


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

#### Utensil Song (Jun 06 2020 at 09:12):

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

#### Mario Carneiro (Jun 06 2020 at 09:12):

The type of the lemma is the same in both cases

#### Mario Carneiro (Jun 06 2020 at 09:13):

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

#### 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

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

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

#### 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

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


#### Mario Carneiro (Jun 06 2020 at 09:20):

That's an empty match

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

#### 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

#### 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>

#### Kevin Buzzard (Jun 06 2020 at 09:23):

Q3 because add_zero is true by definition

#### 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

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

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

MECE?

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

#### 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

#### Utensil Song (Jun 06 2020 at 09:27):

Mario Carneiro said:

MECE?

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

#### 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

#### Utensil Song (Jun 06 2020 at 09:29):

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

#### Mario Carneiro (Jun 06 2020 at 09:30):

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

#### 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

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

#### Mario Carneiro (Jun 06 2020 at 09:32):

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

#### 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

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

#### 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

#### Mario Carneiro (Jun 06 2020 at 09:39):

#tpil is a good source for this order of learning

#### Mario Carneiro (Jun 06 2020 at 09:39):

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

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

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

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

#### Utensil Song (Jun 06 2020 at 10:02):

Kevin Buzzard said:

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 (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

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

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

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

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

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

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

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

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

#### Scott Morrison (Aug 04 2020 at 23:07):

It should just automatically save progress in your browser.

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

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

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

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

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

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

#### 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

#### 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

#### 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

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

#### 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

#### 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 =)

#### Kevin Buzzard (Sep 06 2020 at 22:55):

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


works

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

#### Kevin Buzzard (Sep 06 2020 at 22:55):

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

#### 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

#### 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

#### Rene Recktenwald (Sep 06 2020 at 22:57):

Thank you for the help!

#### Kevin Buzzard (Sep 06 2020 at 22:58):

It's what #new members is for

#### Johan Commelin (Sep 07 2020 at 04:18):

@Rene Recktenwald Good to see you again :smiley:

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

#### Kevin Buzzard (Sep 19 2020 at 10:21):

You can split an or with cases

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

#### Rene Recktenwald (Sep 19 2020 at 11:12):

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 (Sep 19 2020 at 11:13):

you don't have the c

#### Kevin Buzzard (Sep 19 2020 at 11:13):

so you can't do cases on it yet.

#### Rene Recktenwald (Sep 19 2020 at 11:22):

can I do something akin to use c at hi ?

#### Kevin Buzzard (Sep 19 2020 at 11:23):

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

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Sep 19 2020 at 11:30):

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

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

right

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

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

#### Kevin Buzzard (Sep 19 2020 at 11:33):

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

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

#### 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

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

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

#### 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

#### 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

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

#### Rene Recktenwald (Sep 19 2020 at 16:05):

Oh that's so cool, thanks

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

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

#### 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