search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
292 stars 73 forks source link

contrapositive not proved? #48

Closed kbuzzard closed 4 years ago

kbuzzard commented 4 years ago

Andrew Helwer on Twitter:

"Also in advanced proposition world level 9 it says "we proved earlier that (P → Q) → (¬ Q → ¬ P)" but that was not in any previous lesson"

ghost commented 4 years ago

Wasn't that proved in Level 8 of the previous world (Proposition world)?

Screen Shot 2020-02-18 at 2 37 52 AM
kbuzzard commented 4 years ago

Thanks. I'm hoping to get back to this game within a few weeks and deal with all the comments which are appearing in completely random places and which I'm now trying to collect here.

ghost commented 4 years ago

Hopefully you don't mind I leave two more comments about advanced proposition world level 9 here:

  1. As a reader it is not clear when to use by_cases, the tutorial says it's for lemmas like ¬ ¬ P → P, but it's not obvious whether (P → Q) → (¬ Q → ¬ P) belongs to this category or not. (I tried to teach someone to play the natural number game and I realized that I was beaten by the question raised by the student)

  2. As a reader who happens to be a masochist, if someone tries to solve level 9 without depending on cc, he has to use exfalso which is introduced in the next level, but we assume the user has no knowledge of future levels. Does it make sense to swap level 9 and level 10, or is there something I missed here?

kbuzzard commented 4 years ago

I totally agree that it's not clear when to use by_cases. Classical logic has the completeness theorem but in constructive logic it seems to be an art to spot when you can prove something.

I don't see any reason why not to swap advanced proposition world levels 9 and 10.

robx commented 4 years ago

As a reader who happens to be a masochist, if someone tries to solve level 9 without depending on cc, he has to use exfalso which is introduced in the next level, but we assume the user has no knowledge of future levels. Does it make sense to swap level 9 and level 10, or is there something I missed here?

Just to note that I just came here struggling with the same thing. Thinking I should be able to handle all four cases by hand, but then having no idea how to synthesize a proof for Q having both P and not P.

I should also note that one thing that held me back here is that seemingly relevant things we'd proved before were not available (not_if_imp_false and contrapositive, in particular).

EDIT: And yes, switching 9 and 10 around made things clear to me!

kbuzzard commented 4 years ago

Also brought up by Victor Ahlquist on the Zulip chat.

kbuzzard commented 4 years ago

All this should be fixed now.