Natural number game, excluded middle

Stream: new members

[Heather Macbeth]

In Level 9 of Advanced Proposition World ("law of excluded middle"), the narrative text starts by explaining why

intro h,
intro p,
repeat {rw not_iff_imp_false at h},

is not strong enough to solve the level. But when I play around with this in the code box, for example,

rw not_iff_imp_false,

I obtain the error unknown identifier 'not_iff_imp_false'.

Perhaps the lemma not_iff_imp_false was not imported in the source code for this level? If so, perhaps it would be useful to do this? It looks like the lemma is from game.world6.level8. Indeed, the source code for the following level, Level 10 (which does use that lemma in its answer) imports game.world6.level8 at the start of the file.

(Or perhaps I have made a newbie mistake and this is a misunderstanding, or browser caching issue, or something. If so, sorry!)

[Shing Tak Lam]

It's not an issue on your end I'd think. I tried what you did and can reproduce the error.

[Shing Tak Lam]

Ah, I think I've figured it out.

repeat {rw not_iff_imp_false},

works, and does nothing. If you copy the snippet into the box, and look at the state before and after the repeat {rw not_iff_imp_false},, you'll notice it's the same. Essentially the repeat did nothing.

[Shing Tak Lam]

and for some reason, repeat suppresses the unknown identifier error...

[Andrew Ashworth]

I'm guessing this is an oversight, that lemma is not necessary to solve the stage

[Andrew Ashworth]

not_iff_imp_false is something that's just true by definition, that is not p <-> (p -> false), not sure if that's covered in the natural number game...

[Heather Macbeth]

@Shing Tak Lam Thank you for reproducing the error! @Andrew Ashworth, I know the lemma is not needed to solve the level (I've solved it). But I'm suggesting that the lemma be imported in the source code for the level, to allow for experimentation along the lines suggested in the level's narrative.

[Heather Macbeth]

The lemma is from a previous level, game.world6.level8.

[Andrew Ashworth]

well, surely they would be interested in a contribution fixing this. If you go to the file listing for world 7 level 9 and click on the edit button, you can cut and paste lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl -- hide somewhere near the top. Or if you are not so familiar with github, somebody here with commit rights can do it for you

[Heather Macbeth]

It'd be great if someone could propose this edit. I would have, but I don't have a github account.

[Andrew Ashworth]

I am not sure who can commit to this repository or propose pull requests. @Kevin Buzzard

[Shing Tak Lam]

You can fork then PR? (I'm doing it now)

[Andrew Ashworth]

that works too

[Shing Tak Lam]

done

[Heather Macbeth]

Thanks!

[Kevin Buzzard]

Thanks! I was going to push a new version today, I'll incorporate this.