Domineering as a combinatorial game.

We define the game of Domineering, played on a chessboard of arbitrary shape (possibly even disconnected). Left moves by placing a domino vertically, while Right moves by placing a domino horizontally.

This is only a fragment of a full development; in order to successfully analyse positions we would need some more theorems. Most importantly, we need a general statement that allows us to discard irrelevant moves. Specifically to domineering, we need the fact that disjoint parts of the chessboard give sums of games.

Todo

Refactor this file to adhere to the design notes specified in CombinatorialGames.Game.Graph.

def IGame.Domineering : Type

A Domineering board is an arbitrary finite subset of ℤ × ℤ.

Equations

• IGame.Domineering = Finset (ℤ × ℤ)

@[implicit_reducible]

instance IGame.instDecidableEqDomineering : DecidableEq Domineering

Equations

• IGame.instDecidableEqDomineering a b = a.decidableEq b

@[match_pattern]

def IGame.toDomineering : Finset (ℤ × ℤ) ≃ Domineering

Cast a finset to a domineering position.

Equations

• IGame.toDomineering = Equiv.refl (Finset (ℤ × ℤ))

@[match_pattern]

def IGame.ofDomineering : Domineering ≃ Finset (ℤ × ℤ)

Cast a domineering position to a finset.

Equations

• IGame.ofDomineering = Equiv.refl IGame.Domineering

@[simp]

theorem IGame.toDomineering_ofDomineering (a : Domineering) : toDomineering (ofDomineering a) = a

@[simp]

theorem IGame.ofDomineering_toDomineering (s : Finset (ℤ × ℤ)) : ofDomineering (toDomineering s) = s

@[implicit_reducible]

unsafe instance IGame.Domineering.instRepr : Repr Domineering

Equations

• IGame.Domineering.instRepr = Finset.instRepr

def IGame.Domineering.left (b : Domineering) : Finset (ℤ × ℤ)

Left can play anywhere that a square and the square below it are open.

Equations

• b.left = IGame.ofDomineering b ∩ Finset.map ((Equiv.refl ℤ).prodCongr (Equiv.addRight 1)).toEmbedding (IGame.ofDomineering b)

def IGame.Domineering.right (b : Domineering) : Finset (ℤ × ℤ)

Right can play anywhere that a square and the square to the left are open.

Equations

• b.right = IGame.ofDomineering b ∩ Finset.map (Equiv.prodCongr (Equiv.addRight 1) (Equiv.refl ℤ)).toEmbedding (IGame.ofDomineering b)

theorem IGame.Domineering.mem_left {b : Domineering} {m : ℤ × ℤ} : m ∈ b.left ↔ m ∈ ofDomineering b ∧ (m.1, m.2 - 1) ∈ ofDomineering b

theorem IGame.Domineering.mem_right {b : Domineering} {m : ℤ × ℤ} : m ∈ b.right ↔ m ∈ ofDomineering b ∧ (m.1 - 1, m.2) ∈ ofDomineering b

theorem IGame.Domineering.subset_of_mem_left {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : {m, (m.1, m.2 - 1)} ⊆ ofDomineering b

theorem IGame.Domineering.subset_of_mem_right {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : {m, (m.1 - 1, m.2)} ⊆ ofDomineering b

def IGame.Domineering.moveLeft (b : Domineering) (m : ℤ × ℤ) : Domineering

After Left moves, two vertically adjacent squares are removed from the Domineering.

Equations

• b.moveLeft m = IGame.toDomineering (((IGame.ofDomineering b).erase m).erase (m.1, m.2 - 1))

def IGame.Domineering.moveRight (b : Domineering) (m : ℤ × ℤ) : Domineering

After Left moves, two horizontally adjacent squares are removed from the Domineering.

Equations

• b.moveRight m = IGame.toDomineering (((IGame.ofDomineering b).erase m).erase (m.1 - 1, m.2))

theorem IGame.Domineering.moveLeft_subset (b : Domineering) (m : ℤ × ℤ) : ofDomineering (b.moveLeft m) ⊆ ofDomineering b

theorem IGame.Domineering.moveRight_subset (b : Domineering) (m : ℤ × ℤ) : ofDomineering (b.moveRight m) ⊆ ofDomineering b

def IGame.Domineering.relLeft (a b : Domineering) : Prop

Left can move from b to a when there exists some m ∈ left b with a = b.moveLeft m.

Equations

• a.relLeft b = ∃ m ∈ b.left, a = b.moveLeft m

def IGame.Domineering.relRight (a b : Domineering) : Prop

Right can move from b to a when there exists some m ∈ right b with a = b.moveRight m.

Equations

• a.relRight b = ∃ m ∈ b.right, a = b.moveRight m

@[implicit_reducible]

instance IGame.Domineering.instDecidableRelRelLeft : DecidableRel relLeft

Equations

• x✝¹.instDecidableRelRelLeft x✝ = inferInstanceAs (Decidable (∃ x ∈ x✝.left, x✝¹ = x✝.moveLeft x))

@[implicit_reducible]

instance IGame.Domineering.instDecidableRelRelRight : DecidableRel relRight

Equations

• x✝¹.instDecidableRelRelRight x✝ = inferInstanceAs (Decidable (∃ x ∈ x✝.right, x✝¹ = x✝.moveRight x))

theorem IGame.Domineering.card_of_mem_left {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : 2 ≤ (ofDomineering b).card

theorem IGame.Domineering.card_of_mem_right {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : 2 ≤ (ofDomineering b).card

theorem IGame.Domineering.moveLeft_card {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : (ofDomineering (b.moveLeft m)).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.moveRight_card {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : (ofDomineering (b.moveRight m)).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.card_of_relLeft {a b : Domineering} (h : a.relLeft b) : (ofDomineering a).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.card_of_relRight {a b : Domineering} (h : a.relRight b) : (ofDomineering a).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.subrelation_relLeft : Subrelation relLeft (InvImage (fun (x1 x2 : ℕ) => x1 < x2) fun (b : Domineering) => (ofDomineering b).card)

theorem IGame.Domineering.subrelation_relRight : Subrelation relRight (InvImage (fun (x1 x2 : ℕ) => x1 < x2) fun (b : Domineering) => (ofDomineering b).card)

instance IGame.Domineering.instIsWellFoundedRelLeft : IsWellFounded Domineering relLeft

instance IGame.Domineering.instIsWellFoundedRelRight : IsWellFounded Domineering relRight

def GameGraph.domineering : GameGraph IGame.Domineering

The game of domineering.

Equations

• GameGraph.domineering = { moves := fun (p : Player) (x : IGame.Domineering) => Player.cases {y : IGame.Domineering | y.relLeft x} {y : IGame.Domineering | y.relRight x} p }