New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(set_theory/game): short games, boards, and domineering #1540
Conversation
a275993
to
ed4c53e
Compare
Obviously this, as some "recreational maths", is low priority, but I'll assign to @rwbarton as the only person who's previously been interested. :-) |
I'll take a look after the linting errors are addressed: https://github.com/leanprover-community/mathlib/runs/475593766#step:12:16 |
@bryangingechen, I've fixed up the linting problems. |
Thanks, I'll try to take a look this week. Update (2020-03-11): I have been looking at this, but it's taking a while since I started looking over all of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall this looks good to me! Mainly I would like the lines to be within the <100 limit if possible, and I also made a bunch of mostly proof golf suggestions, though some of those might break after you merge in master.
It's nice to see computable definitions put to work in Lean. The real test of short
and state
will be how easy it will be to define other games, so let's try and get this in quickly and then continue the experimentation in future PRs.
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
… into domineering
Sorry about the line lengths, that PR was particularly egregious. Perhaps we need a linter. :-) Thanks very much for the review comments, they were all helpful! (And now I want to go off and tell mathlib about Hex. :-) |
bors r+ |
👎 Rejected by label |
bors r+ |
This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes! To achieve this, I follow Reid's advice: generalise! We define ``` class state (S : Type u) := (turn_bound : S → ℕ) (L : S → finset S) (R : S → finset S) (left_bound : ∀ {s t : S} (m : t ∈ L s), turn_bound t < turn_bound s) (right_bound : ∀ {s t : S} (m : t ∈ R s), turn_bound t < turn_bound s) ``` a typeclass describing `S` as "the state of a game", and provide `pgame.of [state S] : S \to pgame`. This allows a short and straightforward definition of Domineering: ```lean /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ def board := finset (ℤ × ℤ) ... /-- The instance describing allowed moves on a Domineering board. -/ instance state : state board := { turn_bound := λ s, s.card / 2, L := λ s, (left s).image (move_left s), R := λ s, (right s).image (move_right s), left_bound := _ right_bound := _, } ``` which computes: ``` example : (domineering ([(0,0), (0,1), (1,0), (1,1)].to_finset) ≈ pgame.of_lists [1] [-1]) := dec_trivial ```
Build succeeded |
Pull request successfully merged into master. |
This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes! To achieve this, I follow Reid's advice: generalise! We define ``` class state (S : Type u) := (turn_bound : S → ℕ) (L : S → finset S) (R : S → finset S) (left_bound : ∀ {s t : S} (m : t ∈ L s), turn_bound t < turn_bound s) (right_bound : ∀ {s t : S} (m : t ∈ R s), turn_bound t < turn_bound s) ``` a typeclass describing `S` as "the state of a game", and provide `pgame.of [state S] : S \to pgame`. This allows a short and straightforward definition of Domineering: ```lean /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ def board := finset (ℤ × ℤ) ... /-- The instance describing allowed moves on a Domineering board. -/ instance state : state board := { turn_bound := λ s, s.card / 2, L := λ s, (left s).image (move_left s), R := λ s, (right s).image (move_right s), left_bound := _ right_bound := _, } ``` which computes: ``` example : (domineering ([(0,0), (0,1), (1,0), (1,1)].to_finset) ≈ pgame.of_lists [1] [-1]) := dec_trivial ```
…er-community#1540) This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes! To achieve this, I follow Reid's advice: generalise! We define ``` class state (S : Type u) := (turn_bound : S → ℕ) (L : S → finset S) (R : S → finset S) (left_bound : ∀ {s t : S} (m : t ∈ L s), turn_bound t < turn_bound s) (right_bound : ∀ {s t : S} (m : t ∈ R s), turn_bound t < turn_bound s) ``` a typeclass describing `S` as "the state of a game", and provide `pgame.of [state S] : S \to pgame`. This allows a short and straightforward definition of Domineering: ```lean /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ def board := finset (ℤ × ℤ) ... /-- The instance describing allowed moves on a Domineering board. -/ instance state : state board := { turn_bound := λ s, s.card / 2, L := λ s, (left s).image (move_left s), R := λ s, (right s).image (move_right s), left_bound := _ right_bound := _, } ``` which computes: ``` example : (domineering ([(0,0), (0,1), (1,0), (1,1)].to_finset) ≈ pgame.of_lists [1] [-1]) := dec_trivial ```
…er-community#1540) This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes! To achieve this, I follow Reid's advice: generalise! We define ``` class state (S : Type u) := (turn_bound : S → ℕ) (L : S → finset S) (R : S → finset S) (left_bound : ∀ {s t : S} (m : t ∈ L s), turn_bound t < turn_bound s) (right_bound : ∀ {s t : S} (m : t ∈ R s), turn_bound t < turn_bound s) ``` a typeclass describing `S` as "the state of a game", and provide `pgame.of [state S] : S \to pgame`. This allows a short and straightforward definition of Domineering: ```lean /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ def board := finset (ℤ × ℤ) ... /-- The instance describing allowed moves on a Domineering board. -/ instance state : state board := { turn_bound := λ s, s.card / 2, L := λ s, (left s).image (move_left s), R := λ s, (right s).image (move_right s), left_bound := _ right_bound := _, } ``` which computes: ``` example : (domineering ([(0,0), (0,1), (1,0), (1,1)].to_finset) ≈ pgame.of_lists [1] [-1]) := dec_trivial ```
…er-community#1540) This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes! To achieve this, I follow Reid's advice: generalise! We define ``` class state (S : Type u) := (turn_bound : S → ℕ) (L : S → finset S) (R : S → finset S) (left_bound : ∀ {s t : S} (m : t ∈ L s), turn_bound t < turn_bound s) (right_bound : ∀ {s t : S} (m : t ∈ R s), turn_bound t < turn_bound s) ``` a typeclass describing `S` as "the state of a game", and provide `pgame.of [state S] : S \to pgame`. This allows a short and straightforward definition of Domineering: ```lean /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ def board := finset (ℤ × ℤ) ... /-- The instance describing allowed moves on a Domineering board. -/ instance state : state board := { turn_bound := λ s, s.card / 2, L := λ s, (left s).image (move_left s), R := λ s, (right s).image (move_right s), left_bound := _ right_bound := _, } ``` which computes: ``` example : (domineering ([(0,0), (0,1), (1,0), (1,1)].to_finset) ≈ pgame.of_lists [1] [-1]) := dec_trivial ```
This is a do-over of my previous attempt to implement the combinatorial game of domineering. This time, we get a nice clean definition, and it computes!
To achieve this, I follow Reid's advice: generalise! We define
a typeclass describing
S
as "the state of a game", and providepgame.of [state S] : S \to pgame
.This allows a short and straightforward definition of Domineering:
which computes: