[Merged by Bors] - feat(set_theory/game): impartial games and the Sprague-Grundy theorem #3855

foxthomson · 2020-08-18T11:44:34Z

Blocked by leanprover-community/lean#451

src/set_theory/game/impartial.lean

src/set_theory/game/nim.lean

Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

src/set_theory/game/impartial.lean

src/set_theory/game/nim.lean

src/set_theory/game/position.lean

src/set_theory/game/nim.lean

src/set_theory/game/impartial.lean

…athlib into impartial

semorrison · 2020-08-20T03:56:57Z

src/set_theory/game/nim.lean

+
+/-- The definition of single-heap nim, which can be viewed as a pile of stones where each player can
+ take a positive number of stones from it on their turn. -/
+noncomputable def nim : ordinal → pgame


I get a warning definition 'nim' was incorrectly marked as noncomputable here. Do you?

However removing it gives the error rec_fn_macro only allowed in meta definitions... Sounds like it may be a Lean bug?

I get this too, it should be noncomputable due to the quotient.out, right? Where would be best to flag this?

Can you try to minimise this as an example? Ideally we could even get a MWE that doesn't even import mathlib, but it would suffice to get a MWE that just depends on the current mathlib. Can you try just copy and pasting this definition into a file that just imports pgame, nth_rewrite and ordinal? Check also if the from blocks can by replaced by sorry without making the problem go away.

After that, create a new issue here on github, and make a post on zulip to bring it to people's attention.

(Unfortunately I think we better get to the bottom of this before merging, as we don't want warning in mathlib.)

leanprover-community/lean#451

Mario has provided a workaround at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/neither.20computable.20nor.20noncomputable.

This reverts commit eb05399.

semorrison · 2020-08-22T10:07:05Z

Fantastic, thanks for this! 🎉

bors merge

…#3855) Co-authored-by: foxthomson <11833933+foxthomson@users.noreply.github.com>

bors · 2020-08-22T10:39:42Z

Pull request successfully merged into master.

Build succeeded:

@semorrison

* Misc. style cleanups and code golf * Changed naming and namespace to adhere more closely to the naming convention * Changed `impartial` to be a `class`. I am aware that @semorrison explicitly requested not to make `impartial` a class in the #3855, but after working with the definition a bit I concluded that making it a class is worth it, simply because writing `impartial_add (nim_impartial _) (nim_impartial _)` gets annoying quite quickly, but also because you tend to get goal states of the form `Grundy_value _ = Grundy_value _`. By making `impartial` a class and making the game argument explicit, these goal states look like `grundy_value G = grundy_value H`, which is much nicer to work with.

@semorrison

* Misc. style cleanups and code golf * Changed naming and namespace to adhere more closely to the naming convention * Changed `impartial` to be a `class`. I am aware that @semorrison explicitly requested not to make `impartial` a class in the #3855, but after working with the definition a bit I concluded that making it a class is worth it, simply because writing `impartial_add (nim_impartial _) (nim_impartial _)` gets annoying quite quickly, but also because you tend to get goal states of the form `Grundy_value _ = Grundy_value _`. By making `impartial` a class and making the game argument explicit, these goal states look like `grundy_value G = grundy_value H`, which is much nicer to work with.

@semorrison

* Misc. style cleanups and code golf * Changed naming and namespace to adhere more closely to the naming convention * Changed `impartial` to be a `class`. I am aware that @semorrison explicitly requested not to make `impartial` a class in the #3855, but after working with the definition a bit I concluded that making it a class is worth it, simply because writing `impartial_add (nim_impartial _) (nim_impartial _)` gets annoying quite quickly, but also because you tend to get goal states of the form `Grundy_value _ = Grundy_value _`. By making `impartial` a class and making the game argument explicit, these goal states look like `grundy_value G = grundy_value H`, which is much nicer to work with.

foxthomson added 2 commits August 18, 2020 12:36

Added code from foxthomson/impartial

e20e4a4

Correcteted tactic imports for impartial.lean

12a8b4d

foxthomson added the awaiting-review The author would like community review of the PR label Aug 18, 2020

Corrected import in nim

3cd2635

rwbarton changed the title ~~feat(set_theory/game/position,set_theory/game/impartial,set_theory/game/nim): impartial games and the Sprague-Grundy theorem~~ feat(set_theory/game): impartial games and the Sprague-Grundy theorem Aug 18, 2020

foxthomson added 2 commits August 18, 2020 13:54

Corrected imports (again)

577428f

Corrected for linter

f4dc90d

bryangingechen reviewed Aug 18, 2020

View reviewed changes

src/set_theory/game/impartial.lean Outdated Show resolved Hide resolved

bryangingechen reviewed Aug 18, 2020

View reviewed changes

src/set_theory/game/nim.lean Show resolved Hide resolved

foxthomson added 2 commits August 18, 2020 20:08

Replaced tabs with spaces

97b22e9

Added module doc

c42d69e

awainverse reviewed Aug 18, 2020

View reviewed changes

src/set_theory/game/nim.lean Outdated Show resolved Hide resolved

Corrected typo

5acabd6

Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>