From ad50c210a9ecdfd14fe426c5f6cad85f165fddd5 Mon Sep 17 00:00:00 2001 From: Timo Date: Sun, 2 Jul 2023 10:02:15 +0000 Subject: [PATCH] feat: port SetTheory.Game.Domineering (#5654) --- Mathlib.lean | 1 + Mathlib/SetTheory/Game/Domineering.lean | 210 ++++++++++++++++++++++++ 2 files changed, 211 insertions(+) create mode 100644 Mathlib/SetTheory/Game/Domineering.lean diff --git a/Mathlib.lean b/Mathlib.lean index e79decf8ce48d..9f6d01aee934f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2809,6 +2809,7 @@ import Mathlib.SetTheory.Cardinal.Ordinal import Mathlib.SetTheory.Cardinal.SchroederBernstein import Mathlib.SetTheory.Game.Basic import Mathlib.SetTheory.Game.Birthday +import Mathlib.SetTheory.Game.Domineering import Mathlib.SetTheory.Game.Impartial import Mathlib.SetTheory.Game.Nim import Mathlib.SetTheory.Game.Ordinal diff --git a/Mathlib/SetTheory/Game/Domineering.lean b/Mathlib/SetTheory/Game/Domineering.lean new file mode 100644 index 0000000000000..44e82fbd67db8 --- /dev/null +++ b/Mathlib/SetTheory/Game/Domineering.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2019 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison + +! This file was ported from Lean 3 source module set_theory.game.domineering +! leanprover-community/mathlib commit b134b2f5cf6dd25d4bbfd3c498b6e36c11a17225 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.SetTheory.Game.State + +/-! +# 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. +-/ + + +namespace PGame + +namespace Domineering + +open Function + +/-- The equivalence `(x, y) ↦ (x, y+1)`. -/ +@[simps!] +def shiftUp : ℤ × ℤ ≃ ℤ × ℤ := + (Equiv.refl ℤ).prodCongr (Equiv.addRight (1 : ℤ)) +#align pgame.domineering.shift_up PGame.Domineering.shiftUp + +/-- The equivalence `(x, y) ↦ (x+1, y)`. -/ +@[simps!] +def shiftRight : ℤ × ℤ ≃ ℤ × ℤ := + (Equiv.addRight (1 : ℤ)).prodCongr (Equiv.refl ℤ) +#align pgame.domineering.shift_right PGame.Domineering.shiftRight + +/-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/ +-- Porting note: `reducible` cannot be `local`. For now there are no dependents of this file so +-- being globally reducible is fine. +@[reducible] +def Board := + Finset (ℤ × ℤ) +deriving Inhabited +#align pgame.domineering.board PGame.Domineering.Board + +/-- Left can play anywhere that a square and the square below it are open. -/ +def left (b : Board) : Finset (ℤ × ℤ) := + b ∩ b.map shiftUp +#align pgame.domineering.left PGame.Domineering.left + +/-- Right can play anywhere that a square and the square to the left are open. -/ +def right (b : Board) : Finset (ℤ × ℤ) := + b ∩ b.map shiftRight +#align pgame.domineering.right PGame.Domineering.right + +theorem mem_left {b : Board} (x : ℤ × ℤ) : x ∈ left b ↔ x ∈ b ∧ (x.1, x.2 - 1) ∈ b := + Finset.mem_inter.trans (and_congr Iff.rfl Finset.mem_map_equiv) +#align pgame.domineering.mem_left PGame.Domineering.mem_left + +theorem mem_right {b : Board} (x : ℤ × ℤ) : x ∈ right b ↔ x ∈ b ∧ (x.1 - 1, x.2) ∈ b := + Finset.mem_inter.trans (and_congr Iff.rfl Finset.mem_map_equiv) +#align pgame.domineering.mem_right PGame.Domineering.mem_right + +/-- After Left moves, two vertically adjacent squares are removed from the board. -/ +def moveLeft (b : Board) (m : ℤ × ℤ) : Board := + (b.erase m).erase (m.1, m.2 - 1) +#align pgame.domineering.move_left PGame.Domineering.moveLeft + +/-- After Left moves, two horizontally adjacent squares are removed from the board. -/ +def moveRight (b : Board) (m : ℤ × ℤ) : Board := + (b.erase m).erase (m.1 - 1, m.2) +#align pgame.domineering.move_right PGame.Domineering.moveRight + +theorem fst_pred_mem_erase_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : + (m.1 - 1, m.2) ∈ b.erase m := by + rw [mem_right] at h + apply Finset.mem_erase_of_ne_of_mem _ h.2 + exact ne_of_apply_ne Prod.fst (pred_ne_self m.1) +#align pgame.domineering.fst_pred_mem_erase_of_mem_right PGame.Domineering.fst_pred_mem_erase_of_mem_right + +theorem snd_pred_mem_erase_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : + (m.1, m.2 - 1) ∈ b.erase m := by + rw [mem_left] at h + apply Finset.mem_erase_of_ne_of_mem _ h.2 + exact ne_of_apply_ne Prod.snd (pred_ne_self m.2) +#align pgame.domineering.snd_pred_mem_erase_of_mem_left PGame.Domineering.snd_pred_mem_erase_of_mem_left + +theorem card_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : 2 ≤ Finset.card b := by + have w₁ : m ∈ b := (Finset.mem_inter.1 h).1 + have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left h + have i₁ := Finset.card_erase_lt_of_mem w₁ + have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂) + exact Nat.lt_of_le_of_lt i₂ i₁ +#align pgame.domineering.card_of_mem_left PGame.Domineering.card_of_mem_left + +theorem card_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : 2 ≤ Finset.card b := by + have w₁ : m ∈ b := (Finset.mem_inter.1 h).1 + have w₂ := fst_pred_mem_erase_of_mem_right h + have i₁ := Finset.card_erase_lt_of_mem w₁ + have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂) + exact Nat.lt_of_le_of_lt i₂ i₁ +#align pgame.domineering.card_of_mem_right PGame.Domineering.card_of_mem_right + +theorem moveLeft_card {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : + Finset.card (moveLeft b m) + 2 = Finset.card b := by + dsimp [moveLeft] + rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)] + rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)] + exact tsub_add_cancel_of_le (card_of_mem_left h) +#align pgame.domineering.move_left_card PGame.Domineering.moveLeft_card + +theorem moveRight_card {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : + Finset.card (moveRight b m) + 2 = Finset.card b := by + dsimp [moveRight] + rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)] + rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)] + exact tsub_add_cancel_of_le (card_of_mem_right h) +#align pgame.domineering.move_right_card PGame.Domineering.moveRight_card + +theorem moveLeft_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : + Finset.card (moveLeft b m) / 2 < Finset.card b / 2 := by simp [← moveLeft_card h, lt_add_one] +#align pgame.domineering.move_left_smaller PGame.Domineering.moveLeft_smaller + +theorem moveRight_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : + Finset.card (moveRight b m) / 2 < Finset.card b / 2 := by simp [← moveRight_card h, lt_add_one] +#align pgame.domineering.move_right_smaller PGame.Domineering.moveRight_smaller + +/-- The instance describing allowed moves on a Domineering board. -/ +instance state : State Board where + turnBound s := s.card / 2 + l s := (left s).image (moveLeft s) + r s := (right s).image (moveRight s) + left_bound m := by + simp only [Finset.mem_image, Prod.exists] at m + rcases m with ⟨_, _, ⟨h, rfl⟩⟩ + exact moveLeft_smaller h + right_bound m := by + simp only [Finset.mem_image, Prod.exists] at m + rcases m with ⟨_, _, ⟨h, rfl⟩⟩ + exact moveRight_smaller h +#align pgame.domineering.state PGame.Domineering.state + +end Domineering + +/-- Construct a pre-game from a Domineering board. -/ +def domineering (b : Domineering.Board) : PGame := + PGame.ofState b +#align pgame.domineering PGame.domineering + +/-- All games of Domineering are short, because each move removes two squares. -/ +instance shortDomineering (b : Domineering.Board) : Short (domineering b) := by + dsimp [domineering] + infer_instance +#align pgame.short_domineering PGame.shortDomineering + +/-- The Domineering board with two squares arranged vertically, in which Left has the only move. -/ +def domineering.one := + domineering [(0, 0), (0, 1)].toFinset +#align pgame.domineering.one PGame.domineering.one + +/-- The `L` shaped Domineering board, in which Left is exactly half a move ahead. -/ +def domineering.L := + domineering [(0, 2), (0, 1), (0, 0), (1, 0)].toFinset +set_option linter.uppercaseLean3 false in +#align pgame.domineering.L PGame.domineering.L + +instance shortOne : Short domineering.one := by dsimp [domineering.one]; infer_instance +#align pgame.short_one PGame.shortOne + +instance shortL : Short domineering.L := by dsimp [domineering.L]; infer_instance +set_option linter.uppercaseLean3 false in +#align pgame.short_L PGame.shortL + +-- The VM can play small games successfully: +-- #eval decide (domineering.one ≈ 1) +-- #eval decide (domineering.L + domineering.L ≈ 1) +-- The following no longer works since Lean 3.29, since definitions by well-founded +-- recursion no longer reduce definitionally. +-- We can check that `Decidable` instances reduce as expected, +-- and so our implementation of domineering is computable. +-- run_cmd tactic.whnf `(by apply_instance : Decidable (domineering.one ≤ 1)) >>= tactic.trace +-- dec_trivial can handle most of the dictionary of small games described in [conway2001] +-- example : domineering.one ≈ 1 := by decide +-- example : domineering.L + domineering.L ≈ 1 := by decide +-- example : domineering.L ≈ PGame.ofLists [0] [1] := by decide +-- example : (domineering ([(0,0), (0,1), (0,2), (0,3)].toFinset) ≈ 2) := by decide +-- example : (domineering ([(0,0), (0,1), (1,0), (1,1)].toFinset) ≈ PGame.ofLists [1] [-1]) := +-- by decide +-- The 3x3 grid is doable, but takes a minute... +-- example : +-- (domineering ([(0,0), (0,1), (0,2), (1,0), (1,1), (1,2), (2,0), (2,1), (2,2)].toFinset) ≈ +-- PGame.ofLists [1] [-1]) := by decide +-- The 5x5 grid is actually 0, but brute-forcing this is too challenging even for the VM. +-- #eval decide (domineering ([ +-- (0,0), (0,1), (0,2), (0,3), (0,4), +-- (1,0), (1,1), (1,2), (1,3), (1,4), +-- (2,0), (2,1), (2,2), (2,3), (2,4), +-- (3,0), (3,1), (3,2), (3,3), (3,4), +-- (4,0), (4,1), (4,2), (4,3), (4,4) +-- ].toFinset) ≈ 0) +end PGame