Misere combinatorial games.

Push #

Push is played on the same horizontal strip of squares as Shove (see Strip.Piece), and a move again consists of choosing one of your pieces and sliding it one square to the left. The difference is that in Push only the adjacent run of pieces moves: the movement stops at the first empty square to the left of the chosen piece, which gets filled. If there is no empty square to the left, the leftmost piece falls off the board, exactly as in Shove.

In terms of the shared Strip primitive shiftDown, the Push move pushing the piece at position n is shiftDown b g n, where g is the position of the first empty square to the left of n (Push.startPos), or 0 if there is none. So Push is the Strip ruleset whose shift anchor start is the rightmost gap below n.

source

structure MisereGames.Push :

Type

A Push position is a strip board (a function from positions to pieces with finite support).

toBoard : Strip.Board
The underlying strip board.

Instances For

source

def MisereGames.Push.startPos (b : Strip.Board) (n : ℕ) :

ℕ

The anchor of a Push move at position n: the position of the rightmost empty square strictly to the left of n (the "gap" the adjacent block slides into), or 0 if there is no empty square to the left.

Equations

MisereGames.Push.startPos b n = Nat.findGreatest (fun (j : ℕ) => b.board j = MisereGames.Strip.Piece.none ∧ j < n) n

Instances For

source

theorem MisereGames.Push.startPos_le (b : Strip.Board) (n : ℕ) :

startPos b n ≤ n

source

theorem MisereGames.Push.startPos_lt (b : Strip.Board) {n : ℕ} (hn : 0 < n) :

startPos b n < n

source

@[implicit_reducible]

instance MisereGames.Push.instStrip :

Strip Push

Push is the Strip ruleset whose shift starts at the rightmost gap below n: pushing the piece at position n slides only the contiguous block of pieces adjacent to n into the first empty square to its left (or drops the leftmost piece when there is no gap).

Equations

One or more equations did not get rendered due to their size.

source

theorem MisereGames.Push.board_startPos_eq_none (b : Strip.Board) {n : ℕ} (h : ∃ j < n, b.board j = Strip.Piece.none) :

b.board (startPos b n) = Strip.Piece.none

When there is an empty square to the left of n, the Push anchor is itself an empty square: the adjacent block slides into it. This is what makes Push "stop at the first empty tile".

source

noncomputable def MisereGames.Push.toGameForm :

Push → GameForm

The GameForm of a Push position.

Equations