rewriting in hypotheses

Stream: new members

[Tim Hosgood]

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]

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]

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]

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]

have is a really useful tool here.

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

Does this solve your problem?

[Kevin Buzzard]

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]

The computer scientists have been working hard.

[Kevin Buzzard]

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]

There is so much to learn ;-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Tim Hosgood]

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]

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]

If you want to get serious, just download mathlib onto your computer

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]

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]

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]

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

[Kevin Buzzard]

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.

[Tim Hosgood]

will add that to my (already very long) reading list, thanks!

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Tim Hosgood]

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]

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]

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]

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]

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]

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]

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

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]

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]

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]

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

[Tim Hosgood]

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]

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

[waldo]

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]

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

[Kevin Buzzard]

Try holding down shift and clicking reload?

[Kevin Buzzard]

Let's make a new thread.

[waldo]

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

[Emily Riehl]

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]

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]

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

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

[Kevin Buzzard]

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