## Stream: new members

### Topic: rewriting in hypotheses

#### Tim Hosgood (Oct 25 2019 at 17:03):

I'm working through the natural number game (which is really great, by the way, so thank you!) and I'm on level 2-12: showing that a + b = a → b = 0. Starting with intro h, takes me to

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


and what I'd like to do now is rewrite h with add_zero to get a + b = a + 0, but I can't figure out how to just rewrite the _last_ occurrence of a. If I do rw ← add_zero a at h, then it replaces _both_ as with a + 0, which I don't want, and if I don't give add_zero an argument then I get an error, so I'm not sure how to even just rewrite the first a (if I could, then I could somehow use symmetry to get what I want (and this is a bonus question: how can I apply symmetry to h? Using symmetry at h (my naive guess) doesn't work)).

#### Kevin Buzzard (Oct 25 2019 at 17:09):

ha ha you want to do something which is possible, but which I have never explained. So I can see why you're stuck :D

#### Kevin Buzzard (Oct 25 2019 at 17:10):

In fact I'd be very interested to hear what other problems there are after 2-6; I didn't really think hard about those at all. [by which I mean: I was more concerned with documenting 3-1 to 3.6 than 2-7 to 2-16]

#### Kevin Buzzard (Oct 25 2019 at 17:11):

I am surprised symmetry at h doesn't work -- I thought I had realised that this was something which should be useful and someone made a pull request to make it happen. You could do have h2 := h.symm, that would give you a = a + b, but it wouldn't solve your rewriting problem.

#### Kevin Buzzard (Oct 25 2019 at 17:14):

have is a really useful tool here.

begin
have h3 : a + b = a + 0,
-- now we have an extra goal!
exact h,
/-
a b : mynat,
h : a + b = a,
h3 : a + b = a + 0
⊢ b = 0
-/


#### Kevin Buzzard (Oct 25 2019 at 17:16):

If you want your mind to be blown, here are some other tactics you can use: https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

#### Kevin Buzzard (Oct 25 2019 at 17:16):

The computer scientists have been working hard.

#### Kevin Buzzard (Oct 25 2019 at 17:18):

But here is an explanation of how you can do that rewrite for just one a: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

#### Kevin Buzzard (Oct 25 2019 at 17:18):

There is so much to learn ;-)

#### Kevin Buzzard (Oct 25 2019 at 17:19):

example (a b : ℕ) (h : a + b = a) : b = 0 :=
begin
conv at h begin
to_rhs,
end,
-- h : a + b = a + 0
sorry
end


#### Kevin Buzzard (Oct 25 2019 at 17:25):

Oh! Just looking back through old PR's I find this: https://github.com/leanprover-community/mathlib/pull/1269 -- apparently you have to use symmetry'and I don't think I imported this into the natural number game :-/ I'll fix this in v1.1. I think symmetry at h is a very good guess and it should work, and I think I have the power to make it work (thanks to @Rob Lewis ). The issue is that symmetry is defined in core Lean so we can't mess with it and add the "at h" functionality, but I can mess with it in the natural number game because I am already basically using a hacked Lean.

#### Kevin Buzzard (Oct 25 2019 at 17:27):

Right now, clearly the have solution is the easiest for the end user. I should add documentation about have for those brave enough to venture into those extra levels. For inequality world all that $a+b=a\implies b=0$ stuff is essential.

#### Kevin Buzzard (Oct 25 2019 at 17:45):

https://github.com/ImperialCollegeLondon/natural_number_game/issues/9

#### Tim Hosgood (Oct 25 2019 at 17:45):

wow, thanks for the massive response! I'll have a proper read through in a bit and let you know if I have any further questions :-)

#### Tim Hosgood (Oct 25 2019 at 17:46):

so far I haven't had any other such 'why doesn't this thing work' moments up to this level, but will keep you updated if I come across any others

#### Kevin Buzzard (Oct 25 2019 at 17:47):

https://github.com/leanprover-community/mathlib#installation

and then just install the game locally. You can play on your own machine, you don't need an internet connection, it's faster, the error messages are ever so slightly better, and you can save your progress.

#### Tim Hosgood (Oct 25 2019 at 17:49):

I'm guessing that begin and end are hidden in the game, and secretly surrounding the text box into which you type your solutions?

#### Tim Hosgood (Oct 25 2019 at 17:50):

I'm starting to get into Lean. I've been wanting to get into proof assistants for quite some time, coming from a theoretical background, but never managed to decide which one was 'best' to learn. I started playing this game though and before I knew it I had already learnt more than I had in any other assistant, so probably just going to explore Lean a bit more

#### Tim Hosgood (Oct 25 2019 at 17:50):

the docs for mathlib seem really _really_ well written as well, which is a big bonus

#### Kevin Buzzard (Oct 25 2019 at 17:52):

https://leanprover.github.io/theorem_proving_in_lean/ is another cracker. But honestly, I learnt 90% of what I know by just asking questions here.

#### Kevin Buzzard (Oct 25 2019 at 17:54):

Yes, begin and end are surrounding the text box which you can type in in the natural number game. I'm a mathematician, and for me, the proofs are always the most fun part. My original ideas about how to teach this stuff are here https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/ but the game is an attempt to make it much easier for the end user.

#### Tim Hosgood (Oct 25 2019 at 18:40):

in 2-13, there's the hint of using zero_ne_succ, which seems to imply that maybe we want to be doing a proof by contradiction? is this something that you can do in Lean, or are proofs by contradiction not 'constructive' enough?

#### Tim Hosgood (Oct 25 2019 at 18:40):

(also I suppose I've never actually proved this lemma without contradiction before!)

#### Kevin Buzzard (Oct 25 2019 at 20:30):

I don't know if I've introduced cases b with x, which splits one goal into two, the cases b = 0 and b = succ x.

#### Kevin Buzzard (Oct 25 2019 at 20:30):

I also don't know if I've introduced apply and I'm pretty sure that I have not told you that a \ne b is by definition a = b -> false

#### Kevin Buzzard (Oct 25 2019 at 21:06):

Yeah, I think this is pretty much impossible to solve given what I've told you. I'll need to document this a bit better. I had to release the game because chalkdust was coming out and in it I claim that the game will be ready, whereas in fact I had several other big things going on in my life (teaching and a deadline for the perfectoid paper) so these later world 2 levels are very rough around the edges. I will try and fix them up this weekend once I've read the 717 unread emails in my inbox

#### Tim Hosgood (Oct 25 2019 at 21:36):

ah, I see how cases would help here :-)

#### Tim Hosgood (Oct 25 2019 at 21:37):

that's ok, I really don't think it's particularly bad! you do specifically say that you won't really give any hints for the bonus levels and one needs to look stuff up etc

#### Kevin Buzzard (Oct 25 2019 at 22:38):

You can do cases on equality too! If you managed to get h : succ x = 0 then try cases h and see what happens.

#### Tim Hosgood (Oct 26 2019 at 01:06):

I've spotted just a few typos and stuff when playing through. Nothing major, but would you like me to keep a track of the few I see and let you know?

#### Kevin Buzzard (Oct 26 2019 at 08:20):

Absolutely. You could put them on the issues page at https://github.com/ImperialCollegeLondon/natural_number_game/issues if you didn't want them to just be lost in a pile of starred zulip messages or the 717 unread emails I currently have (the joys of teaching). I would be completely happy to have 25 trivial comments. There are several completely minor things there already. I plan on releasing v1.01 soon after all the admin for my course is over (i.e. soon after 1st November) with a ton of minor bug fixes and corrections. I know this should all have been done before v1.0 but I wanted to release the game at the same time as the chalkdust magazine came out.

#### Emily Riehl (Oct 26 2019 at 17:54):

Just wanted to say thanks for putting this game out. I'm having fun with it. I'm also very slowly trying to work through the back levels of world 2, trying to learn some more tactics (my first time using lean). But it's been great.

#### Kevin Buzzard (Oct 26 2019 at 18:42):

Hey @Emily Riehl it's great to see you here! I am really sorry about the later levels in world 2, they are really poorly documented.

#### Tim Hosgood (Oct 26 2019 at 18:54):

@Kevin Buzzard are you planning on writing up example solutions/further hints at any point? if not, I might write a sort of 'guided tour' to the game, with some example solutions, but I'm sure that mine aren't exactly always the most direct...

#### Tim Hosgood (Oct 26 2019 at 18:54):

at by 'at any point' I really do mean 'some arbitrary point in the future', and not 'tomorrow' or 'this week' or anything

#### Kevin Buzzard (Oct 26 2019 at 18:55):

You can see my plans here https://github.com/ImperialCollegeLondon/natural_number_game/issues but actually you can probably find all the solutions here https://github.com/ImperialCollegeLondon/natural_number_game/tree/master/src/solutions or here https://github.com/ImperialCollegeLondon/natural_number_game/tree/master/src/game if you look around.

#### Kevin Buzzard (Oct 26 2019 at 18:57):

The repo is currently doing two completely distinct jobs, which is probably bad. You can clone it and play the levels on your own computer, or you can compile the repo using https://github.com/mpedramfar/Lean-game-maker -- but this compilation process needs the solutions. So the solutions are in two completely different places right now :-/

#### Tim Hosgood (Oct 26 2019 at 18:57):

oh brilliant, that can help on a level I was stuck on!

#### Tim Hosgood (Oct 26 2019 at 19:00):

and thanks again for doing this, by the way. it really makes actually getting started with a proof assistant so much easier than otherwise

#### Kevin Buzzard (Oct 26 2019 at 19:04):

yeah that was exactly the point :D Sorry it took me two years!

#### waldo (Oct 26 2019 at 19:15):

I'm getting the Lean is busy message do you know how to make it actually work? (site didn't load for me on firefox, so went for edge)

#### Kevin Buzzard (Oct 26 2019 at 19:16):

I don't know anything about the web side of things.

#### Kevin Buzzard (Oct 26 2019 at 19:16):

Try holding down shift and clicking reload?

#### waldo (Oct 26 2019 at 19:17):

sure, I'm new to this platform so I'm not sure how everything works here. it seems different from irc

#### Emily Riehl (Oct 27 2019 at 01:18):

You can do cases on equality too! If you managed to get h : succ x = 0 then try cases h and see what happens.

Can you explain what cases h does? It seems like I should be calling the function zero_ne_succ to apply to h to get a term of type bot or something but I'm really not sure what's going on under the hood.

#### Jesse Michael Han (Oct 27 2019 at 01:24):

cases applies the induction principle and then discards the induction hypothesis; in this case equality is an inductive type and applying the induction principle amounts to substituting it

#### Floris van Doorn (Oct 29 2019 at 03:01):

@Jesse Michael Han's answer is part of what cases does.
cases also has special support for equality between constructors of an inductive type. It will apply nat.no_confusion in your example (which is almost the same as encode in HoTT. This means that if h is an equality between two different constructors, then it will close the goal, and if h is an equality between the same constructor, it will derive the equalities between the arguments of this constructor, and apply cases to those equalities.

open nat
example {n : ℕ} (h : succ n = 0) : false := by cases h
example {n m : ℕ} (h : succ n = succ m) : n = m := by { cases h, refl }


#### Kevin Buzzard (Oct 29 2019 at 07:32):

There is something interesting with these examples because they are propositions, and yet their proof uses recursion rather than just induction

#### Kevin Buzzard (Oct 29 2019 at 07:33):

They are the two axioms that Peano isolated in his original work defining the naturals but which are absent in Lean's definition

Last updated: May 12 2021 at 05:19 UTC