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 Strip.Piece : Type

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

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

@[instance_reducible]

instance Strip.instDecidableEqPiece : DecidableEq Piece

Equations

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

def Strip.Piece.ofPlayer : Player → Piece

The piece belonging to a given player.

Equations

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

@[simp]

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

@[simp]

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

theorem Strip.Piece.ofPlayer_injective : Function.Injective ofPlayer

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

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

structure 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
• finite_support : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → self.board n = Piece.none

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

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

def Strip.Board.zero : Board

The empty board.

Equations

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

@[simp]

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

shiftDown: the shared move primitive

def 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

• 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 Strip.Piece.none else b i

@[simp]

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

@[simp]

theorem 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 Strip.Board.shiftDown_eq (b : ℕ → Piece) {start n : ℕ} (h : start ≤ n) : shiftDown b start n n = Piece.none

@[simp]

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

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

shiftDown applied to a board with finite support.

Equations

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

@[simp]

theorem 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 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 = Strip.Piece.none then 0 else i + 1

theorem 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 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 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 ≠ Strip.Piece.none) ⋯.choose

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

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

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

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

theorem 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 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 = Strip.Piece.ofPlayer p then s.rightmostPos + 1 else 0

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

theorem 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 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 Strip (R : Type u) : Type u

• 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 Strip.board {R : Type u} [Strip R] (r : R) (n : ℕ) : Piece

The piece at position n of r.

Equations

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

@[simp]

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

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

Weight of a position.

Equations

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

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

Rightmost occupied position.

Equations

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

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

The p-stride of a position.

Equations

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

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

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

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

Structural lemmas for push

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

@[simp]

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

theorem 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 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 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 Strip.moves {R : Type u} [Strip R] : Player → R → Set R

Equations

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

theorem 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 Strip.graph (R : Type u) [Strip R] : GameGraph R

The game graph of a strip ruleset.

Equations

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

theorem 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 Strip.instIsWellFoundedGraph {R : Type u} [Strip R] : (graph R).IsWellFounded

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

The GameForm of a strip position.

Equations

• Strip.toGameForm = GameGraph.toForm

@[simp]

theorem 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 Strip.toGameForm_zero_iff {R : Type u} [Strip R] (g : R) : Strip.toGameForm g = 0 ↔ ∀ (n : ℕ), board g n = Piece.none

theorem 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 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 Strip.rightmostPos_push_below {R : Type u} [Strip R] {s : R} {m : ℕ} (hm : m < rightmostPos s) : rightmostPos (push s m) = rightmostPos s

theorem 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 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 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 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 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 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 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 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 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 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 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 Strip.rightmostPos_greatest {R : Type u} [Strip R] {s : R} {k : ℕ} (hk : board s k ≠ Piece.none) : k ≤ rightmostPos s

theorem 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 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 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 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.

@[instance_reducible]

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

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

Equations

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

instance 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 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

• Strip.equivInt R = GameForm.MisereQuotient.stridedEquivInt

theorem 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