natural number game questions

Stream: new members

[Craig Citro]

hi all! absolutely loving the natural number game (kudos @Kevin Buzzard). i had a few (largely silly) questions.

1. for adv proposition world, level 9, is there a way to beat it with only the tactics we know so far other than cc or tauto? in the second case, i spent a few minutes trying to figure out how to capitalize on having P \land \lnot P in hand before googling and discovering the contradiction tactic. was i missing a more "bare-handed" approach?

2. for adv proposition world, level 8, there's a "did you spot the import" comment at the end that's mysterious to me ... what import?

3. is there a github repo where the code for the game lives?

[Craig Citro]

... and a followup: how does one get inline expansion for latex here? ;)

[David Renshaw]

3 -> https://github.com/ImperialCollegeLondon/natural_number_game

[Bryan Gin-ge Chen]

1. You can do it using by_cases hq : Q, and exfalso (I guess that shows up in the next level though...) (edit: and you can replace exfalso by either using the term false.elim or by using cases H on a hypothesis H : false.)
2. I'm guessing Kevin was thinking of the line import tactic.finish in the source Lean file here and that paragraph was a subtle hint for you to try the finish tactic. Unfortunately, the import isn't visible in the generated HTML...

[Craig Citro]

awesome, thanks!

[Emily Riehl]

Inspired by @Scott Morrison I returned to the natural numbers game this weekend and was delighted to see all the new tactics and new levels. I feel like I'm getting somewhere now. Thanks everyone.

[Emily Riehl]

Now here's my question: I'm stuck on mul_left_cancel in the advanced multiplication world. I'd like to prove (a !=0) -> (a b = a c) -> b = c by (strong) double induction on b and c. This should give me four cases, three of which involve the hypothesis that either b or c is zero. Then for the fourth the plan is to use add_left_cancel to conclude from the hypothesis

a (succ b) = a (succ c)

that

a b = a c.

Then the inductive hypothesis should give me b = c, whence succ b = succ c.

But I have no idea how to set up this double induction. The hint says to use revert but I don't see where it would help.

[Scott Morrison]

My guess is that you want a forall in the goal at the moment you invoke induction, and to achieve that you need to use revert.

[Scott Morrison]

Spoiler:

revert c,
induction b,
{ intro c, sorry, },
{ intro c, induction c,
  { sorry, },
  { sorry, } }

[Scott Morrison]

(I haven't actually tried doing the proof after that step, I'm just guessing that's the structure you wanted.)

[Emily Riehl]

Thanks @Scott Morrison . That did the trick.

Here's the full gory thing (spoiler below):

revert c,
induction b with x hx,
intro c,
rw mul_zero,
intro hyp,
symmetry at hyp,
have lem := eq_zero_or_eq_zero_of_mul_eq_zero _ _ hyp,
cases lem with p q,
exfalso,
exact ha p,
symmetry,
assumption,
intro c,
induction c with y hy,
intro hyp,
rw mul_zero at hyp,
have lem := eq_zero_or_eq_zero_of_mul_eq_zero _ _ hyp,
cases lem with p q,
exfalso,
exact ha p,
assumption,
intro hyp,
repeat {rw mul_succ at hyp},
have lem := add_right_cancel _ _ _ hyp,
have step := hx y lem,
apply succ_eq_succ_of_eq,
assumption,

[Scott Morrison]

Next you need some braces and indenting. :-)

[Emily Riehl]

Haha on point ;)

[Scott Morrison]

Ah, earlier I couldn't work out why ex_falso didn't exist... Apparently because it's exfalso, but by_contradiction.

[Scott Morrison]

@Kevin Buzzard, what do you think of adding a @[simp] lemma that says succ n = n + 1? In some of the later levels I find myself writing proofs that want to use this fact often.

[Johan Commelin]

@Emily Riehl Congrats!

[Kevin Buzzard]

This is a bad level. Without revert it's probably impossible and I do a really bad job of explaining how revert works. This needs to be fixed

[Mario Carneiro]

It can be done without revert if you use induction b generalizing c instead (which is the correct way to do inductions like this anyway)

[Mario Carneiro]

It's debatable, but I think it is a good teaching moment to explain what it means to generalize an argument in an induction. This came up in discussions at the meeting in bonn

[Kevin Buzzard]

I will get back to this game in a few weeks and update it. There are several minor changes I want to make

[Ethan Horsfall]

apologies if I am being useless; on question 8 of advanced addition world, and whenever I try to use succ_inj something goes wrong.

b n : mynat,
an : n + b = n → b = 0,
h : succ (n + b) = succ n
⊢ b = 0

I want to apply succ_inj to h by applying it to h with parameters n+b and b, but this always raises an error. When I've had problems like this on previious levels, I've used the 'have' tactic, but this also won't import because it seems to get confused by the parameter name n+b

[Kevin Buzzard]

does have h2 := succ_inj h work?

[Kevin Buzzard]

I guess you could just go backwards the way the computer scientists want you to do -- apply an and then apply succ_inj will presumably work.

[Patrick Massot]

It looks like the official solution

[Ethan Horsfall]

ah thank you that works ! i also hadnt realised there was an official solution set oops so thank you for that also

[Ethan Horsfall]

also really enjoying the game, so thanks for making it :)

[Kevin Buzzard]

I'm not sure it's officially documented anywhere that there's an official solution set :-)

[Ethan Horsfall]

when calling a function, such as succ_inj or mul_pos, how do you pass in arguments which themselves are functions?

For instance,
have f := mul_pos a b,

works but
have f := mul_pos succ(a) succ(b),
does not work, with the error message indicating that it expected something of type mynat, whereas it read s succ as a function from mynat to mynat.

thank you:)

[Donald Sebastian Leung]

You probably need to wrap succ(a) and succ(b) itself in parentheses, like so: have f := mul_pos (succ(a)) (succ(b))

[Bryan Gin-ge Chen]

The parentheses around a and b in succ(a) and succ(b) are unnecessary. Note that you can also take advantage of "dot notation" and write have f := mul_pos a.succ b.succ.

[Ethan Horsfall]

thank you both:)

[Donald Sebastian Leung]

You're welcome :smile:

[Kevin Buzzard]

I always put the parentheses in succ(a) in the natural number game because I felt it was less intimidating for mathematicians

[Ethan Horsfall]

yes I find that much more natural

[Kevin Buzzard]

However this shows a downside to this idea -- succ(a) looks like an irreducible gadget to a mathematician, but is apparently parsed as succ a and hence succ can fall off and be eaten by an earlier function.

[Donald Sebastian Leung]

@Ethan Horsfall FYI the notation for function application in (functional) programming differs from that in conventional mathematics, for example f(x) in mathematics could be simply written as f x in Lean

[Ethan Horsfall]

on the last level of advanced multiplication world, i have got it to the point where I have the hypothesis
c : mynat,
c_ih : ∀ (a : mynat), a ≠ 0 → ∀ (b : mynat), a * b = a * c → b = c, ###
a : mynat,
ha : a ≠ 0, ###
n : mynat,
g : a * n + a = a * c + a,
W : a * n + a = a * c + a → a * n = a * c
⊢ a * n = a * c → n = c ###

I have put ### by the remaining relevant propositions

which should be very simple as if we only look at c_ih and ha, the goal is just a restatement of this. but i cannot work out how to introduce the right variables into c_ih or revert the goal correctly. The propositions in the middle muddle it up when I use revert

[Kevin Buzzard]

Does exact c_ih a ha n work?

[Kevin Buzzard]

You can think of c_ih as a function, which takes as input a natural number a, a proof that it's not zero, and a natural number b, and returns a proof that ab=ac -> b=c.

[Reid Barton]

Also you should be able to apply c_ih and let Lean work out what additional arguments are needed.

[Reid Barton]

(either supplying them automatically or turning them into new goals)

[Ethan Horsfall]

thank you, that seems to have worked. the slightly weird thing is that it now just says 'no goals' instead of proof complete. viewing it as a function makes a lot of sense

[Kevin Buzzard]

?? I'm impressed :-) I thought Mohammad had managed to completely banish "no goals"!

[Ethan Horsfall]

Finished the game!!

[Ethan Horsfall]

is the official documentation the best place to go next?

[Donald Sebastian Leung]

Ethan Horsfall said:

is the official documentation the best place to go next?

That, or you could try Theorem Proving in Lean next which teaches you how to define your own functions, mathematical objects, etc. on top of proving theorems with tactics.

[Bryan Gin-ge Chen]

In addition to TPiL, I found the Logic & Proof book useful when I was learning Lean. I also like the Logical Verification notes.

[Kevin Buzzard]

If you're a mathematician then one thing you could try is to choose an arbitrary piece of elementary mathematics and try doing it in Lean, and ask when you get stuck. For me the route was: basic 1st year introduction to proof stuff, definition of a scheme, theorems about schemes, definition of a perfectoid space. Because there is no ideal book for mathematicians we have to forge our own path right now. I guess there are always the maths challenges if they're up your street. What are you looking for?

[Kevin Buzzard]

PS @Ethan Horsfall Mohammad says that if you can reproduce "no goals" then you should tell us how and he'll try and fix it ;-) He's just submitted his PhD thesis so I'm sure he has plenty of time on his hands :-)

[Ethan Horsfall]

I'm an undergraduate student. (actually, an undergraduate economist, but I just secured my switch to maths recently :) ). I'm in the fortunate position of mostly pursuing what I find interesting. for the 'no goals' every time I refreshed the page it would lose previous progress, so I may not be able to reproduce it

[Kevin Buzzard]

What maths do you know already?

[Ethan Horsfall]

i've covered https://dec41.user.srcf.net/notes/ all of part ia except dynamics and relativity, and ib linear algebra, markov chains, and partway through some others

[Kevin Buzzard]

Are you in Cambridge right now? You know they have a Lean meeting on Wednesday evenings?

[Kevin Buzzard]

If you want to help make the group theory game, the current state of it is here

[Ethan Horsfall]

I am in cambridge right now, and didn't know there was a lean meeting! i doubt i have enough experience to be much help but would be willing to try :)

[Kevin Buzzard]

Believe me, I'm sure you'll be welcome. @Edward Ayers is perhaps the person to talk to about it. Bring some friends ;-)

[Kevin Buzzard]

I'm at an Imperial meeting right now.

[Edward Ayers]

Hi @Ethan Horsfall I've added you to the secret Cambridge group. meetings are 15:00 to 18:00 on Wednesdays somewhere in the CMS room TBC. The meeting is for all skill levels, there are 3 or 4 people learning the natural numbers game. If anyone else wants to be added to the cambridge group then ask me. I think if you are a member of the group you can add new members?

[Vaibhav Karve]

Level 8 of the Advanced Proposition World says

Pro tip
Did you spot the import? What do you think it does?

I do not see any import though. What am I missing? Was it a mathlib import?

[Kevin Buzzard]

Let's look in the source code :-)

[Kevin Buzzard]

I seem to be importing finish

[Kevin Buzzard]

Does finish just finish the level in one move?

[Kevin Buzzard]

This looks like an outdated comment -- it is impossible to spot the import if you're playing the game because of the --hide

[Kevin Buzzard]

Looks like there was a commit where I hid the import, but didn't change the comment.

[Vaibhav Karve]

Cool. Thanks!

[Simon Liesinger]

@Kevin Buzzard , I noticed that the statement of pow_succ in the sidebar is wrong. it says that pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * b, but I think it should be a^b*a

[Kevin Buzzard]

Yeah I know, it's on the list of things to fix. Thanks.

[ohhaimark]

How would one go writing a tactic that will select the first assumption in context that can be applyed to the goal?

[ohhaimark]

and apply it

[Anne Baanen]

The spoilery way is to look at the implementation of the assumption tactic in core Lean:

meta def assumption : tactic unit :=
do { ctx ← local_context,
     t   ← target,
     H   ← find_same_type t ctx,
     exact H }
<|> fail "assumption tactic failed"

[Anne Baanen]

Here, local_context gets the list of hypotheses, and target gives the goal type.

[Anne Baanen]

So instead of find_same_type, which finds the hypothesis with the exact same type as the goal, we could iterate over the local_context and try to apply each element in turn until it succeeds.

[ohhaimark]

Thanks. It somehow didn't occur to me to look at the definition of the basic tactics.

[Kevin Buzzard]

The best introduction we have to learning to write tactics in Lean is programming in Lean, which is a bit out of date but which does contain lots of juicy information. After that people just tend to ask in the chat.

[Bryan Gin-ge Chen]

The best introduction we have to learning to write tactics in Lean is programming in Lean,

I think the Logical Verification notes are also a good source (certainly less out of date).

[Jasmin Blanchette]

We're working on a 2nd edition. Keep an eye on the same URL, but with 2020 instead of 2019.

[Patrick Massot]

Recall we also have documentation in mathlib.

[Scott Morrison]

Do we know why sometimes we get stuck with "Lean is busy" in the natural numbers game?

[Scott Morrison]

It's happened to us again.

[Scott Morrison]

@Kevin Buzzard, I was just looking at the natural numbers game repo, and wondering about some a few things.

[Scott Morrison]

Are the src/my_solutions/ and src/solutions/ directories obsolete?

[Scott Morrison]

(The README currently suggests that if you wan to play the game in VSCode to use those directories, but they seem quite out of date relative to the src/game/ directory.)

[Scott Morrison]

It would be fun to be able to hack on this.

[Kevin Buzzard]

Yes I can quite believe that those directories are obsolete. I have no idea about any of the web issues. @Mohammad Pedramfar ?

[Mohammad Pedramfar]

Yes, the game maker only looks at the lean files specified in the game_config.toml file, which in this case are all contained in the game folder. The only other things that are needed are the files that are imported which, in this case, are contained in the mynat and tactic folder. The rest aren't needed.

[Jiekai]

Had a lot of fun with natural number game! Looking forward to more games.
The web game format works amazing. No setup hassle required at all.
Is real-number-game available on the web?

[Kevin Buzzard]

no, there is no real number game. Someone was coming to visit me in May and work on it but unfortunately this is now all up in the air. I should try and get a fan club together.

[Jiekai]

Inequality world Level 6

  cases hab,
  cases hba,
  rw hab_h at hba_h,
  rw add_assoc at hba_h,
  symmetry at hba_h,
  have h00: (hab_w + hba_w) = 0 := eq_zero_of_add_right_eq_self _ _ hba_h,
  cases hab_w,
  {
    rw hab_h,
    refl, -- cursor here shows 'no goals'
  },
  {
  }

@Mohammad Pedramfar

[Jiekai]

Since the game does not introduces { ... }, I guess it is not an issue.

[Kevin Buzzard]

No goals is correct with the cursor there because you have finished the goal which you isolated

[Kevin Buzzard]

Oh -- but the point is that it doesn't say "proof complete" or whatever?

[Jiekai]

Yeah, guess "no goals" is okay

[Jasmin Blanchette]

Concerning the logical verification notes discussed on March 9, be aware that there's a new version now, available under "material" below:

https://lean-forward.github.io/logical-verification/2020/index.html#material

It's much better than the old book. Please tell anybody who's reading the old one to stop! ;)

[Sara Fish]

On "Advanced addition world" level 6, the instructions say that there is a three-line solution. I assume this intended solution is the following.

rw add_comm t a,
rw add_comm t b,
exact add_right_cancel a t b,

Using repeat, which has previously been introduced, this can also be done in two lines.

repeat {rw add_comm t},
exact add_right_cancel a t b,

Not sure whether this is worth briefly mentioning as an added challenge? Maybe this is trivial to point out, but I think the trick of using rw add_comm t is kind of cute here.

[Kenny Lau]

does it count as one line if you use ;to join the two lines?

[Kenny Lau]

what is the point?

[Kevin Buzzard]

Golf?

[Kenny Lau]

the two versions are essentially the same proof. It isn't like you simplified the proof.

[Kevin Buzzard]

Kenny can you beat 25 single rewrites for (a+b)^2?

[Kenny Lau]

what's the setting?

[Kevin Buzzard]

I can't remember, I just remember saying I did something in 27 and then someone telling me they could do 25

[Kevin Buzzard]

Maybe last level of power world?

[Kevin Buzzard]

The game saves your progress now :tada:

[Kenny Lau]

  rw two_eq_succ_one,
  rw pow_succ,
  rw pow_succ,
  rw pow_succ,
  rw pow_one,
  rw pow_one,
  rw pow_one,
  rw add_mul,
  rw mul_add,
  rw mul_add,
  rw succ_mul,
  rw one_mul,
  rw add_mul,
  rw mul_comm b a,
  rw add_assoc,
  rw add_assoc,
  rw add_comm (b * b),
  rw add_assoc,
  refl,

[Kenny Lau]

19 lines

[Kenny Lau]

of course there is also the one line rw {insert huge proof term}

[Kevin Buzzard]

In her paper on ring, Mahboubi claims that it takes 30 rewrites to prove the analogous result for (a+b)^3 but I asked her about it and apparently there's no concrete reference for this

[Kevin Buzzard]

They just made an estimate

[Kevin Buzzard]

The exact numbers probably depend on whether x^3=x(xx) or xx(x) etc

[Shing Tak Lam]

Kevin Buzzard said:

I can't remember, I just remember saying I did something in 27 and then someone telling me they could do 25

I think it was the last time the NNG was on r/math?

https://old.reddit.com/r/math/comments/fwlgf4/natural_number_game_a_game_where_you_learn_to/fmql2y4/

Also they did it in 18, not 25.

[Kenny Lau]

18 rewrites, so 19 lines

[Kenny Lau]

so the same as mine

[Mario Carneiro]

example (a b : ℤ) : (a + b) ^ 2 = a*a + 2*a*b + b*b :=
by rw [pow_two, add_mul_self_eq]

[Kenny Lau]

@Mario Carneiro we're using mynat

[Kenny Lau]

in the last level of power world

[Mario Carneiro]

I don't like these floating tactic scripts with no context

[Johan Commelin]

Isn't the topic title enough context?

[Mario Carneiro]

not to know what the problem is

[Mario Carneiro]

reading a tactic script is hard enough as it is, the type of the theorem is the main clue about what's going on

[Mario Carneiro]

these NNG examples are just unreadable

[Kenny Lau]

well if you Ctrl+A and Ctrl+C and Ctrl+V then you don't get the theorem

[Mario Carneiro]

I don't have the page up

[Mario Carneiro]

I don't know what the theorem looks like, I just guessed

[Kenny Lau]

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=4&level=8

[Mario Carneiro]

lemma add_squared (a b : mynat) :
  (a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b :=
begin
  have : ∀ x:mynat, x ^ (2:mynat) = x * x := λ x, by rw [two_eq_succ_one, pow_succ, pow_one],
  rw [this, this, this],
  rw [add_mul, two_mul, add_right_comm, add_mul],
  rw [← add_assoc, ← mul_add, mul_add b, mul_comm b, add_assoc],
  refl
end

[Mario Carneiro]

it would have been even better if I had add_four_comm : (a + b) + (c + d) = (a + c) + (b + d)

[Mario Carneiro]

or its less used cousin add_four_rotate_right : (a + b) + (c + d) = (a + c) + (d + b). In a real theorem prover you have all these things proven already

[Kevin Buzzard]

add42? Do you need add4n for 1<=n<=24?

[Kenny Lau]

presumably one of them is rfl

[Alexandre Rademaker]

hi @Kevin Buzzard, can we still play the game offline? I would like to have my solutions saved in my machine...

[Kevin Buzzard]

I thought that solutions were saved on your machine now? (but not transferrable between machines). You can clone the repo and edit the lean files directly, but note that they will all have solutions in.

[Alexandre Rademaker]

Hum, I don’t know how to find them. The browser is now showing all worlds as unsolved.

[Kevin Buzzard]

I'm really sorry, this is part of the set-up which I understand nothing about :-( My browser remembers my previous attempts shrug.

[Bryan Gin-ge Chen]

If I remember correctly, the save data is placed in your browser's local storage. It will get cleared if you clear your browser's cache for that site.

[Bryan Gin-ge Chen]

It woudn't be impossible to add a button that would download all the solutions as e.g. a ZIP file containing a bunch of Lean files. @Mohammad Pedramfar what do you think?

[Julian Berman]

@Alexandre Rademaker what browser are you on?

[Julian Berman]

On Firefox for me, if I go to Tools > Web Developer > Toggle Tools, and then click Storage and then Local Storage in the sidebar, I see an entry for https://wwwf.imperial.ac.uk, and if I click on it, I see what's a big blob of JSON but it has all my solutions in it. Do you see something similar?

[Alexandre Rademaker]

Safari, i will try to find the json

[Alexandre Rademaker]

But I am afraid I lost the data in the last update of the system

[Kevin Buzzard]

If you don't want to solve the levels again you can cheat by looking at the internal solutions here https://github.com/ImperialCollegeLondon/natural_number_game/tree/master/src/game

[Mohammad Pedramfar]

Bryan Gin-ge Chen said:

It woudn't be impossible to add a button that would download all the solutions as e.g. a ZIP file containing a bunch of Lean files. Mohammad Pedramfar what do you think?

It is possible to add a save and load button, so that the users can save their progress on their computer. However, saving the progress as editable lean files is slightly tricky, since the use might change some parts of the lean files that shouldn't be changed and then loading those files could be a bit problematic. I can add the option to save and load a save file that is not meant to be edited by the user though.

[Bryan Gin-ge Chen]

You could include comments telling the user to edit only within some part of the file.

[Mohammad Pedramfar]

That's possible, but for it to work, I might need to rewrite a good part of python code in javascript, the parts that handle lean files and turn in into a format that the game can use. Unless it's actually going to be used by a reasonable number of players, I'd rather not go through with it.
Especially since what the user can download will not be a single file, it will be a folder, containing several lean files and config files. Basically the repository that Kevin sent the link to.
Another point is that it's not straightforward for the player to recognize if they changed some part that they shouldn't have. Even adding a single space to the statement of a lemma can make the game treat it as a different lemma! (The reason for this behaviour is version control. If you're making the game and continuously updating it to fix typos and add/modify levels, you'd prefer the player's saves to not be reset with every single minor update. The way this game tracks problems through minor updates is by remembering the exact statement of lemmas. After a minor update, even if you rearrange levels, the saved data for an unchanged lemma will be remembered.) Of course this could be circumvented, by letting the player change the statement of the lemmas as well. But in that case, the player might as well just clone the Lean-game-maker and play the game on localhost!

[Jon Eugster]

Hi! (I've been looking at Lean 2 years ago but honestly forgot everything about it meanwhile)

I was going through the natural numbers game and encountered something weird: I thought my proof was correct seems to work and ends with "no goals.", but simultaneously it says "Invalid syntax" for an intermediate line which executes fine when going through with the cursor.

The line is the following

have q1 := eq_zero_or_eq_zero_of_mul_eq_zero a (succ c) (←h),

I suspect it's that I don't know yet how to properly plug in objects, I have h : 0 = a * succ c and I want to use

eq_zero_or_eq_zero_of_mul_eq_zero
  (a b : mynat) (h : a * b = 0) :
  a = 0 ∨ b = 0

to get something like q: a = 0 ∨ succ c = 0 (to get a contradiction).

I had the same problem with feeding a*c (a natural number) into a statement, so I'd really appreachiate an insight on how to do that! Thank you

This is Advanced Multiplication World Level 4, and my full code is

revert b,
induction c with c hc,

intros b h,
rw mul_zero at h,
rw mul_eq_zero_iff at h,
cases h,
exfalso, exact ha(h),
exact h,

intros b h,
cases b,
exfalso,
rw mul_zero at h,

have q1 := eq_zero_or_eq_zero_of_mul_eq_zero a (succ c) (←h),
cases q1,
exact ha(q1),
exact succ_ne_zero c q1,

repeat{rw mul_succ at h},
rw add_right_cancel_iff at h,
have q := hc b h,
apply succ_eq_succ_of_eq,
exact q,

[Mario Carneiro]

my advice is to ignore anything else lean says if it also says "invalid syntax"

[Mario Carneiro]

that means you have invalid syntax and everything else is lean trying to pick up the pieces and probably getting more confused

[Mario Carneiro]

in this case the issue is (←h), that's not an expression

[Mario Carneiro]

probably h.symm works in that position

[Jon Eugster]

It does, thank you! so \l is only used in combination with rw?

[Jon Eugster]

And regarding the other part, if I have h: a*c + a = 0 and I want to use

 add_left_eq_zero
   {{a b : mynat}} (H : a + b = 0) : b = 0

to get a = 0, how do I do that?

I tried have h' := add_left_eq_zero (a*c) a h, is it the {{ that work differently than I expected?

[Kevin Buzzard]

The {{ }} brackets mean "Lean will supply these". Try have h' := add_left_eq_zero h. The point is that Lean can guess the other inputs after it sees the type of h so it doesn't want to bother the user with them.

[Kevin Buzzard]

Sorry, I don't ever explain {} brackets properly in NNG and this is a common question.

[Jon Eugster]

That makes sense, amazing!

The problem was again that I supplied either h: 0 = ... or ←h instead of h.symm.

Thank you both for the help!

[Kevin Buzzard]

Ps if you've finished with h then replace h := add_left_eq_zero h saves you from having to make a new hypothesis.

[Kwame Porter Robinson]

I’m learning about lean through the natural numbers game [1] and have only applied mathematics background from engineering. To gain greater familiarity I’m trying to rewrite proofs to force me to understand the concepts and syntax in different ways.

For World 9: Advanced Multiplication, level 1, is there a way to prove the first subgoal by contradiction or another strategy when starting with,

intros ha hb,
cases (a*b),

——- gives ——
a b : mynat,
ha : a ≠ 0,
hb : b ≠ 0
⊢ 0 ≠ 0

A lot of proof by contradiction assumes Prop variables but here we have mynat so I am unsure how to manipulate the goal proposition to show that 0 ≠ 0 is absurd.

[1] https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world9/level1.lean

[Kevin Buzzard]

I don't think you can solve that level after those tactics. Your goal is false and your hypotheses don't give you a contradiction

[Kwame Porter Robinson]

Thank you, that was helpful. I'm just learning. Couldn't I create a proposition based on the truthiness of equality, that 0 = 0 --> true, and use that implication as a hypothesis that gives a contradiction?

[Reid Barton]

You're trying to prove the goal (0 ≠ 0).

[Reid Barton]

If you had 0 ≠ 0 as a hypothesis, then you could use it to prove anything.

[Patrick Johnson]

@Kwame Porter Robinson If your question is whether ¬A → ¬B can be inferred from A → B, the answer is no.

[Kwame Porter Robinson]

@Patrick Johnson I think my question is whether A -> ¬B can be inferred or shown to be false, given A -> B. Here I wondered if taking A as a eq relation could show 0 = 0 --> true and used to prove the goal 0 ≠ 0 to be false.

[Reid Barton]

You can certainly prove that 0 ≠ 0 is false, but here you need to prove that it is true.

[Reid Barton]

That's what it means to be the goal.

[Kevin Buzzard]

Kevin Buzzard said:

I don't think you can solve that level after those tactics. Your goal is false and your hypotheses don't give you a contradiction

Just to be clear -- what I am saying is that you have made an incorrect move and this level is now impossible to solve.