Zulip Chat Archive

Stream: new members

Topic: Natural number game, excluded middle


view this post on Zulip Heather Macbeth (May 05 2020 at 03:53):

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!)

view this post on Zulip Shing Tak Lam (May 05 2020 at 04:01):

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

view this post on Zulip Shing Tak Lam (May 05 2020 at 04:03):

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.

view this post on Zulip Shing Tak Lam (May 05 2020 at 04:03):

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

view this post on Zulip Andrew Ashworth (May 05 2020 at 04:05):

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

view this post on Zulip Andrew Ashworth (May 05 2020 at 04:07):

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...

view this post on Zulip Heather Macbeth (May 05 2020 at 04:08):

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

view this post on Zulip Heather Macbeth (May 05 2020 at 04:09):

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

view this post on Zulip Andrew Ashworth (May 05 2020 at 04:11):

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

view this post on Zulip Heather Macbeth (May 05 2020 at 04:12):

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

view this post on Zulip Andrew Ashworth (May 05 2020 at 04:16):

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

view this post on Zulip Shing Tak Lam (May 05 2020 at 04:17):

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

view this post on Zulip Andrew Ashworth (May 05 2020 at 04:17):

that works too

view this post on Zulip Shing Tak Lam (May 05 2020 at 04:20):

done

view this post on Zulip Heather Macbeth (May 05 2020 at 04:24):

Thanks!

view this post on Zulip Kevin Buzzard (May 05 2020 at 09:54):

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


Last updated: May 08 2021 at 19:11 UTC