Misere combinatorial games.

Strips: shared board theory for Shove and Push

Both Shove and Push are played on a horizontal strip of squares, each square either empty or occupied by a Left or Right piece (see Strip.Piece). In both games a move consists of choosing one of your pieces and shifting a contiguous "block" of pieces one square to the left.

The two rulesets differ only in which block of pieces is moved:

• In Shove, choosing the piece at position n shifts everything at positions 0 .. n one square to the left, regardless of gaps. The piece at position 0 falls off the strip.
• In Push, only the adjacent run of pieces moves: the block stops at the first empty square to the left of n (which gets filled). If there is no empty square the leftmost piece falls off, just like Shove.

This module factors out everything that both rulesets have in common. The single shared primitive is Strip.shiftDown b start n, which shifts the squares (start, n] one place to the left into [start, n). Both rulesets are special cases:

• Shove's move is shiftDown b 0 n.
• Push's move is shiftDown b g n, where g is the position of the first empty square left of n (or 0 if there is none).

The crucial fact about either game is its stride: the distance to the rightmost tile of a given colour. Since the stride only ever depends on the rightmost tile, and since pushing the rightmost tile behaves identically in Shove and Push, the entire stride theory — culminating in the proof that the misère quotient is isomorphic to ℤ — is developed once here, generically, in terms of a Strip typeclass.

inductive MisereGames.Strip.Piece : Type

A single square of a strip: empty, or occupied by a Left/Right piece.

• none : Piece
• left : Piece
• right : Piece

@[implicit_reducible]

instance MisereGames.Strip.instDecidableEqPiece : DecidableEq Piece

Equations

• MisereGames.Strip.instDecidableEqPiece x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MisereGames.Strip.Piece.ofPlayer : Player → Piece

The piece belonging to a given player.

Equations

• MisereGames.Strip.Piece.ofPlayer MisereGames.Player.left = MisereGames.Strip.Piece.left
• MisereGames.Strip.Piece.ofPlayer MisereGames.Player.right = MisereGames.Strip.Piece.right

@[simp]

theorem MisereGames.Strip.Piece.ofPlayer_ne_none (p : Player) : ofPlayer p ≠ none

@[simp]

theorem MisereGames.Strip.Piece.none_ne_ofPlayer (p : Player) : none ≠ ofPlayer p

theorem MisereGames.Strip.Piece.ofPlayer_injective : Function.Injective ofPlayer

theorem MisereGames.Strip.Piece.eq_none_of_ne_ofPlayer {x : Piece} (hl : x ≠ ofPlayer Player.left) (hr : x ≠ ofPlayer Player.right) : x = none

theorem MisereGames.Strip.Piece.ne_none_of_ofPlayer {p : Player} {x : Piece} (h : x = ofPlayer p) : x ≠ none

structure MisereGames.Strip.Board : Type

A strip board: a function from positions on the strip (leftmost being 0) to the piece at that position, with finite support (only finitely many occupied squares).

• board : ℕ → Piece

  The piece at each board position.

• finite_support : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → self.board n = Piece.none

theorem MisereGames.Strip.Board.ext {s t : Board} (h : ∀ (n : ℕ), s.board n = t.board n) : s = t

theorem MisereGames.Strip.Board.ext_iff {s t : Board} : s = t ↔ ∀ (n : ℕ), s.board n = t.board n

def MisereGames.Strip.Board.zero : Board

The empty board.

Equations

• MisereGames.Strip.Board.zero = { board := fun (x : ℕ) => MisereGames.Strip.Piece.none, finite_support := MisereGames.Strip.Board.zero._proof_1 }

@[simp]

theorem MisereGames.Strip.Board.zero_board (n : ℕ) : Board.zero.board n = Piece.none

shiftDown: the shared move primitive

def MisereGames.Strip.Board.shiftDown (b : ℕ → Piece) (start n : ℕ) : ℕ → Piece

shiftDown b start n shifts the squares in (start, n] one place to the left, into [start, n). Concretely: squares strictly below start are unchanged; squares start ≤ i < n receive the piece from i + 1; square n becomes empty; squares above n are unchanged.

When start = 0 this is the Shove move (the piece at 0 falls off). When start is the position of the first empty square below n, the empty square is filled and this is the Push move.

Equations

• MisereGames.Strip.Board.shiftDown b start n i = if i < start then b i else if i < n then b (i + 1) else if i = n then MisereGames.Strip.Piece.none else b i

@[simp]

theorem MisereGames.Strip.Board.shiftDown_lt_start (b : ℕ → Piece) {start n i : ℕ} (h : i < start) : shiftDown b start n i = b i

@[simp]

theorem MisereGames.Strip.Board.shiftDown_mid (b : ℕ → Piece) {start n i : ℕ} (h1 : start ≤ i) (h2 : i < n) : shiftDown b start n i = b (i + 1)

@[simp]

theorem MisereGames.Strip.Board.shiftDown_eq (b : ℕ → Piece) {start n : ℕ} (h : start ≤ n) : shiftDown b start n n = Piece.none

@[simp]

theorem MisereGames.Strip.Board.shiftDown_gt (b : ℕ → Piece) {start n i : ℕ} (h : n < i) : shiftDown b start n i = b i

def MisereGames.Strip.Board.shiftDownB (s : Board) (start n : ℕ) : Board

shiftDown applied to a board with finite support.

Equations

• s.shiftDownB start n = { board := MisereGames.Strip.Board.shiftDown s.board start n, finite_support := ⋯ }

@[simp]

theorem MisereGames.Strip.Board.shiftDownB_board (s : Board) (start n : ℕ) : (s.shiftDownB start n).board = shiftDown s.board start n

Weight measure for well-foundedness

noncomputable def MisereGames.Strip.Board.weight (s : Board) : ℕ

The weight of a board is the sum of i + 1 over each non-empty position i. This is finite by finite support, and strictly decreases with each shiftDown (as long as the pushed square n was occupied).

Equations

• s.weight = ∑ i ∈ Finset.range ⋯.choose, if s.board i = MisereGames.Strip.Piece.none then 0 else i + 1

theorem MisereGames.Strip.Board.weight_eq_of_bound {s : Board} (N : ℕ) (hN : ∀ (n : ℕ), N ≤ n → s.board n = Piece.none) : s.weight = ∑ i ∈ Finset.range N, if s.board i = Piece.none then 0 else i + 1

theorem MisereGames.Strip.Board.weight_shiftDownB_lt {s : Board} {start n : ℕ} (hsn : start ≤ n) (hn : s.board n ≠ Piece.none) : (s.shiftDownB start n).weight < s.weight

The rightmost occupied position

noncomputable def MisereGames.Strip.Board.rightmostPos (s : Board) : ℕ

The position of the rightmost occupied square (or 0 if the board is empty).

Equations

• s.rightmostPos = Nat.findGreatest (fun (n : ℕ) => s.board n ≠ MisereGames.Strip.Piece.none) ⋯.choose

theorem MisereGames.Strip.Board.rightmostPos_le (s : Board) : s.rightmostPos ≤ ⋯.choose

theorem MisereGames.Strip.Board.rightmostPos_spec (s : Board) {k : ℕ} (hk : k ≤ ⋯.choose) (hne : s.board k ≠ Piece.none) : s.board s.rightmostPos ≠ Piece.none

theorem MisereGames.Strip.Board.board_eq_none_of_gt_rightmostPos {s : Board} {k : ℕ} (hk : s.rightmostPos < k) : s.board k = Piece.none

theorem MisereGames.Strip.Board.rightmostPos_greatest {s : Board} {k : ℕ} (hk : s.board k ≠ Piece.none) : k ≤ s.rightmostPos

theorem MisereGames.Strip.Board.board_rightmostPos_ne_none {s : Board} (h : 0 < s.rightmostPos) : s.board s.rightmostPos ≠ Piece.none

A nonzero rightmostPos is always occupied.

The stride

noncomputable def MisereGames.Strip.Board.stride (s : Board) (p : Player) : ℕ

The p-stride of a board: the distance to the rightmost tile when it is of colour p, and 0 otherwise. This is the same definition for Shove and Push.

Equations

• s.stride p = if s.board s.rightmostPos = MisereGames.Strip.Piece.ofPlayer p then s.rightmostPos + 1 else 0

theorem MisereGames.Strip.Board.stride_neg_eq_zero {s : Board} (p : Player) (hp : s.board s.rightmostPos = Piece.ofPlayer p) : s.stride (-p) = 0

theorem MisereGames.Strip.Board.rightmost_of_stride_pos {p : Player} {s : Board} (hs : s.stride p ≠ 0) : s.board s.rightmostPos = Piece.ofPlayer p ∧ s.rightmostPos + 1 = s.stride p

theorem MisereGames.Strip.Board.neg_push_below_rightmost {s : Board} {p : Player} {m : ℕ} (hrm : s.board s.rightmostPos = Piece.ofPlayer p) (hm : s.board m = Piece.ofPlayer (-p)) : m < s.rightmostPos

The Strip typeclass

A Strip is a type R of game positions whose underlying data is a Board, equipped with a move push r n (push the piece at position n). Both Shove and Push are instances. The move is required to be a shiftDown of the board, anchored at a position start r n ≤ n (with start r n < n whenever `n

0`). This single description captures both rulesets.

class MisereGames.Strip (R : Type u) : Type u

A strip ruleset with positions backed by a finite-support board.

• toBoard : R → Board

  The underlying board of a position.

• ofBoard : Board → R

  Construct a position from a board (used to realise prescribed strides).

• toBoard_ofBoard (b : Board) : toBoard (ofBoard b) = b
• push : R → ℕ → R

  The move: push the piece at position n.

• start : R → ℕ → ℕ

  The anchor position of the shift.

• start_le (r : R) (n : ℕ) : start r n ≤ n
• start_lt (r : R) {n : ℕ} (hn : 0 < n) : start r n < n
• push_eq (r : R) (n : ℕ) : toBoard (push r n) = (toBoard r).shiftDownB (start r n) n

  The move is a shiftDown of the board anchored at start.

def MisereGames.Strip.board {R : Type u} [Strip R] (r : R) (n : ℕ) : Piece

The piece at position n of r.

Equations

• MisereGames.Strip.board r n = (MisereGames.Strip.toBoard r).board n

@[simp]

theorem MisereGames.Strip.board_def {R : Type u} [Strip R] (r : R) (n : ℕ) : board r n = (toBoard r).board n

noncomputable def MisereGames.Strip.weight {R : Type u} [Strip R] (r : R) : ℕ

Weight of a position.

Equations

• MisereGames.Strip.weight r = (MisereGames.Strip.toBoard r).weight

noncomputable def MisereGames.Strip.rightmostPos {R : Type u} [Strip R] (r : R) : ℕ

Rightmost occupied position.

Equations

• MisereGames.Strip.rightmostPos r = (MisereGames.Strip.toBoard r).rightmostPos

noncomputable def MisereGames.Strip.stride {R : Type u} [Strip R] (r : R) (p : Player) : ℕ

The p-stride of a position.

Equations

• MisereGames.Strip.stride r p = (MisereGames.Strip.toBoard r).stride p

theorem MisereGames.Strip.weight_def {R : Type u} [Strip R] (r : R) : weight r = (toBoard r).weight

theorem MisereGames.Strip.rightmostPos_def {R : Type u} [Strip R] (r : R) : rightmostPos r = (toBoard r).rightmostPos

theorem MisereGames.Strip.stride_def {R : Type u} [Strip R] (r : R) (p : Player) : stride r p = (toBoard r).stride p

Structural lemmas for push

theorem MisereGames.Strip.board_push_above {R : Type u} [Strip R] (r : R) {n i : ℕ} (h : n < i) : board (push r n) i = board r i

theorem MisereGames.Strip.board_push_eq {R : Type u} [Strip R] (r : R) (n : ℕ) : board (push r n) n = Piece.none

theorem MisereGames.Strip.board_push_below {R : Type u} [Strip R] (r : R) {n i : ℕ} (h : i < start r n) : board (push r n) i = board r i

theorem MisereGames.Strip.board_push_shift {R : Type u} [Strip R] (r : R) {n : ℕ} (hn : 0 < n) : board (push r n) (n - 1) = board r n

theorem MisereGames.Strip.weight_push_lt {R : Type u} [Strip R] (r : R) {n : ℕ} (hn : board r n ≠ Piece.none) : weight (push r n) < weight r

Moves and the associated GameForm

def MisereGames.Strip.moves {R : Type u} [Strip R] : Player → R → Set R

Legal moves in a strip ruleset.

Equations

• MisereGames.Strip.moves p s = MisereGames.Strip.push s '' {n : ℕ | MisereGames.Strip.board s n = MisereGames.Strip.Piece.ofPlayer p}

theorem MisereGames.Strip.mem_moves_iff {R : Type u} [Strip R] (p : Player) (s s' : R) : s' ∈ Strip.moves p s ↔ ∃ (n : ℕ), board s n = Piece.ofPlayer p ∧ s' = push s n

def MisereGames.Strip.graph (R : Type u) [Strip R] : GameGraph R

The game graph of a strip ruleset.

Equations

• MisereGames.Strip.graph R = { moves := MisereGames.Strip.moves }

theorem MisereGames.Strip.weight_lt_of_mem_move {R : Type u} [Strip R] {p : Player} {s s' : R} (h_mem : s' ∈ (graph R).moves p s) : weight s' < weight s

instance MisereGames.Strip.instIsWellFoundedGraph {R : Type u} [Strip R] : (graph R).IsWellFounded

noncomputable def MisereGames.Strip.toGameForm {R : Type u} [Strip R] : R → GameForm

The GameForm of a strip position.

Equations

• MisereGames.Strip.toGameForm = MisereGames.GameGraph.toForm

@[simp]

theorem MisereGames.Strip.moves_toGameForm {R : Type u} [Strip R] (p : Player) (s : R) : Moves.moves p (Strip.toGameForm s) = Strip.toGameForm '' Strip.moves p s

theorem MisereGames.Strip.toGameForm_zero_iff {R : Type u} [Strip R] (g : R) : Strip.toGameForm g = 0 ↔ ∀ (n : ℕ), board g n = Piece.none

theorem MisereGames.Strip.toGameForm_push_mem_moves {R : Type u} [Strip R] {s : R} (p : Player) {m : ℕ} (hm : board s m = Piece.ofPlayer p) : Strip.toGameForm (push s m) ∈ Moves.moves p (Strip.toGameForm s)

theorem MisereGames.Strip.mem_moves_toGameForm_iff {R : Type u} [Strip R] (s : R) (p : Player) (g' : GameForm) : g' ∈ Moves.moves p (Strip.toGameForm s) ↔ ∃ (m : ℕ), board s m = Piece.ofPlayer p ∧ g' = Strip.toGameForm (push s m)

rightmostPos and stride under push

theorem MisereGames.Strip.rightmostPos_push_below {R : Type u} [Strip R] {s : R} {m : ℕ} (hm : m < rightmostPos s) : rightmostPos (push s m) = rightmostPos s

theorem MisereGames.Strip.rightmostPos_push_at {R : Type u} [Strip R] {s : R} {k : ℕ} (hk : rightmostPos s = k) (hpos : 0 < k) (hne : board s k ≠ Piece.none) : rightmostPos (push s k) = k - 1

theorem MisereGames.Strip.stride_push_below {R : Type u} [Strip R] {s : R} (p : Player) {m : ℕ} (hm : m < rightmostPos s) : stride (push s m) p = stride s p

theorem MisereGames.Strip.stride_push_at_rightmost {R : Type u} [Strip R] {s : R} (p : Player) {k : ℕ} (hk : rightmostPos s = k) (hpos : 0 < k) (hp : board s k = Piece.ofPlayer p) : stride (push s k) p = k

theorem MisereGames.Strip.stride_neg_push_at_rightmost {R : Type u} [Strip R] {s : R} (p : Player) {k : ℕ} (hk : rightmostPos s = k) (hp : board s k = Piece.ofPlayer p) (hpos : 0 < k) : stride (push s k) (-p) = 0

theorem MisereGames.Strip.push_rightmost_zero_empty {R : Type u} [Strip R] {s : R} (h0 : rightmostPos s = 0) (n : ℕ) : board (push s 0) n = Piece.none

theorem MisereGames.Strip.stride_neg_zero_of_p_move {R : Type u} [Strip R] {s : R} (p : Player) {m : ℕ} (hrm : board s (rightmostPos s) = Piece.ofPlayer p) (hm : board s m = Piece.ofPlayer p) : stride (push s m) (-p) = 0

theorem MisereGames.Strip.stride_push_eq_rightmostPos {R : Type u} [Strip R] {s : R} (p : Player) {m : ℕ} (hm1 : board s m ≠ Piece.none) (hm2 : m = rightmostPos s) : stride (push s m) p = stride s p - 1

theorem MisereGames.Strip.stride_push_le {R : Type u} [Strip R] {s : R} (p : Player) {m : ℕ} (hm : board s m ≠ Piece.none) : stride (push s m) p ≤ stride s p

theorem MisereGames.Strip.stride_zero_of_push {R : Type u} [Strip R] {s : R} {p : Player} {m : ℕ} (hs : stride s p = 0) (hm : board s m ≠ Piece.none) : stride (push s m) p = 0

theorem MisereGames.Strip.push_to_empty_is_neg {R : Type u} [Strip R] {s : R} {p : Player} {m : ℕ} (hs : stride s p = 0) (hm_piece : board s m ≠ Piece.none) (h_empty : ∀ (n : ℕ), board (push s m) n = Piece.none) : board s m = Piece.ofPlayer (-p)

theorem MisereGames.Strip.isSolved_of_stride_zero {R : Type u} [Strip R] {p : Player} {s : R} (hs : stride s p = 0) : GameForm.IsSolved p (Strip.toGameForm s)

theorem MisereGames.Strip.rightmostPos_greatest {R : Type u} [Strip R] {s : R} {k : ℕ} (hk : board s k ≠ Piece.none) : k ≤ rightmostPos s

theorem MisereGames.Strip.rightmost_of_stride_pos {R : Type u} [Strip R] {p : Player} {s : R} (hs : stride s p ≠ 0) : board s (rightmostPos s) = Piece.ofPlayer p ∧ rightmostPos s + 1 = stride s p

theorem MisereGames.Strip.neg_push_below_rightmost {R : Type u} [Strip R] {s : R} {p : Player} {m : ℕ} (hrm : board s (rightmostPos s) = Piece.ofPlayer p) (hm : board s m = Piece.ofPlayer (-p)) : m < rightmostPos s

theorem MisereGames.Strip.toGameForm_hasStride {R : Type u} [Strip R] (s : R) (p : Player) : GameForm.HasStride p (Strip.toGameForm s) (stride s p)

Every strip position has a stride: HasStride p (toGameForm s) (stride s p). This is the heart of the shared theory.

Building the Strided structure and the equivalence with ℤ

theorem MisereGames.Strip.mk_with_stride {R : Type u} [Strip R] (p : Player) (n : ℕ) : ∃ (r : R), GameForm.HasStride p (Strip.toGameForm r) n ∧ GameForm.HasStride (-p) (Strip.toGameForm r) 0

For every player p and every n, there is a strip position with p-stride n and (-p)-stride 0: namely a single piece of colour p at position n - 1.

@[implicit_reducible]

noncomputable instance MisereGames.Strip.ruleset (R : Type u) [Strip R] : Ruleset R

Every Strip ruleset is a Ruleset, with the shared toGameForm.

Equations

• MisereGames.Strip.ruleset R = { toGameForm := MisereGames.Strip.toGameForm, moves_toGameForm := ⋯ }

instance MisereGames.Strip.strided (R : Type u) [Strip R] : GameForm.Strided (Form.ClosedUnderAdd.closure (Ruleset.Forms R))

The Strided structure on the additive closure of any Strip ruleset.

noncomputable def MisereGames.Strip.equivInt (R : Type u) [Strip R] : MisereQuotient (Form.ClosedUnderAdd.closure (Ruleset.Forms R)) ≃ ℤ

The misère quotient of any Strip ruleset is isomorphic to ℤ.

Equations

• MisereGames.Strip.equivInt R = MisereGames.GameForm.MisereQuotient.stridedEquivInt

theorem MisereGames.Strip.le_iff_equiv_ge (R : Type u) [Strip R] (a b : MisereQuotient (Form.ClosedUnderAdd.closure (Ruleset.Forms R))) : a ≤ b ↔ GameForm.MisereQuotient.stridedEquivInt a ≥ GameForm.MisereQuotient.stridedEquivInt b