Even/odd world

[kbuzzard]

We need an even/odd world. A proposal: IsEven x := \exists t, x = t + t, IsOdd x := \exists t, x = t + t + 1, and then the boss levels of that world is that every natural is either even or odd, and that no natural is both even and odd.

Ivan has started on writing the Lean code (but I don't have a link).

[ifarabella]

My code is here https://github.com/ifarabella/NNG4 . The relevant theorems are under NNG4/Game/Levels/EvenOddTest

[kbuzzard]

Ivan I cleaned up your code and put it here. Right now the plan is to have even-odd world after advanced addition world, which will introduce the theorems succ_inj and succ_ne_zero, and the tactics intro, exact and apply (and apply ... at). I want even-odd world to teach use and rcases. What we really need is ten or so files each containing one theorem from the levels of even-odd world, like we have already with addition world etc.

[kbuzzard]

OK so the status of this is that neither Ivan nor I have the time to work on it, I have tidied up the plan for the level and have pushed it to the file Game/LevelIdeas/EvenOdd.lean here in the branch EvenOdd_world_plan. What needs to be done is that this one Lean file needs to be turned into 12 files with explanations and hints and so on.

[kvanvels]

I am working on this.