The Catch-Up game and conjecture

The game Catch-Up (Isaksen–Ismail–Brams–Nealen, 2015) is a two-player, perfect-information game played on a finite nonempty set S of positive integers. Each time a player removes a number from S, that number is added to the player’s score.

Rules.

• The scores start at 0. Player p1 starts by removing exactly one number from S.
• After the first move, players alternate turns. On a turn, the current player removes one or more numbers from S, one at a time, and must keep removing numbers until their score becomes at least the opponent’s score; before the final pick they must remain strictly behind.
• If the current player cannot catch up (in particular, even taking all remaining numbers would still leave them behind), the game ends immediately: the current player receives all remaining numbers.

When S is empty, the player with higher score wins; equal scores give a draw.

In this file we define:

• Player and Outcome,
• the recursive evaluator value (optimal play),
• the conjecture value_of_even_mul_succ_self_div_two.

Example

For S = {1,2,3,4} one play is: p1 takes 2, p2 takes 1 then 4, and p1 takes 3, ending with scores (5,5).

References

A. Isaksen, M. Ismail, S. J. Brams, A. Nealen, Catch-Up: A Game in Which the Lead Alternates, Game & Puzzle Design 1(2), 38–49 (2015).

inductive CatchUp.Player : Type

An arbitrary two elements type indexing the players in the Catch-Up game.

• p1 : Player
• p2 : Player

instance CatchUp.instDecidableEqPlayer : DecidableEq Player

Equations

• CatchUp.instDecidableEqPlayer x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CatchUp.instReprPlayer : Repr Player

Equations

• CatchUp.instReprPlayer = { reprPrec := CatchUp.reprPlayer✝ }

def CatchUp.Player.other : Player → Player

Returns the other player.

Equations

• CatchUp.Player.p1.other = CatchUp.Player.p2
• CatchUp.Player.p2.other = CatchUp.Player.p1

inductive CatchUp.Outcome : Type

The possible outcomes of a Catch-Up game.

• win : Outcome
• loss : Outcome
• draw : Outcome

instance CatchUp.instDecidableEqOutcome : DecidableEq Outcome

Equations

• CatchUp.instDecidableEqOutcome x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CatchUp.instReprOutcome : Repr Outcome

Equations

• CatchUp.instReprOutcome = { reprPrec := CatchUp.reprOutcome✝ }

def CatchUp.Outcome.neg : Outcome → Outcome

Negates an outcome, swapping win and loss. Used when switching player perspectives.

Equations

• CatchUp.Outcome.win.neg = CatchUp.Outcome.loss
• CatchUp.Outcome.loss.neg = CatchUp.Outcome.win
• CatchUp.Outcome.draw.neg = CatchUp.Outcome.draw

def CatchUp.Outcome.best (os : List Outcome) : Outcome

Computes the best outcome for the current player from a list of possible outcomes. Win > Draw > Loss.

Equations

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

Define the recursive game value functions.

@[irreducible]

noncomputable def CatchUp.valueAux (remaining : Finset ℕ) (s_me s_opp : ℕ) (isFirstMove : Bool) : Outcome

value remaining s_me s_opp isFirstMove evaluates the position where:

• remaining is the set S' of numbers not yet taken.
• s_me is the current score of the player who is about to act (the “current player”).
• s_opp is the opponent’s current score.
• isFirstMove indicates whether we are in the special very first move of the whole game, where the rules force exactly one pick and then the turn passes.

The result is the game-theoretic value from the current player’s point of view: .win / .loss / .draw, assuming optimal play from both sides.

We model a single turn (which may consist of several picks $x_1,...,x_k$) by recursion: the current player chooses one number x; if they are still strictly behind after taking it, they must continue the same turn (so the recursive call keeps the same “current player”); once they catch up (score ≥ opponent), the turn ends and we swap players.

Equations

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

noncomputable def CatchUp.value (S : Finset ℕ) : Outcome

Public API: The game-theoretic value of Catch-Up on the set S, assuming optimal play. Returns .win if player 1 wins, .loss if player 2 wins, .draw if the game is tied.

Equations

• CatchUp.value S = CatchUp.valueAux S 0 0 true

theorem CatchUp.value_of_even_mul_succ_self_div_two (N : ℕ) (h_even : Even (N * (N + 1) / 2)) : value (Finset.Icc 1 N) = Outcome.draw

Let (T_N = \sum_{k=1}^{N} k = \frac{N(N+1)}{2}). If (T_N) is even (equivalently (N \equiv 0 \pmod 4) or (N \equiv 3 \pmod 4)), then under optimal play the game Catch-Up(\(\{1, \ldots, N\}\)) ends in a draw.