feat(set_theory/game): short games, boards, and domineering (#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
```
mathlib3
d84de804 - feat(set_theory/game): short games, boards, and domineering (#1540)
