Poset games

Let α be a partially ordered type (in fact, a preorder suffices). One can define the following impartial game: two players alternate turns choosing an element a : α, and "removing" the entire interval Ici a from the poset. As usual, whoever runs out of moves loses.

In a general poset, this game need not terminate. Adding the condition that α is well quasi-ordered (well-founded with no infinite antichains) is both sufficient and necessary to guarantee a finite game.

This setup generalizes other well-known games within CGT, most notably Chomp, which is simply the poset game on (Fin m × Fin n) \ {⊥}.

Main results

• GameGraph.Poset.impartial_toIGame: poset games are impartial
• GameGraph.Poset.univ_fuzzy_zero: any poset game with a top element is won by the second player, shown via a strategy stealing argument

Poset relation

def GameGraph.Poset.Rel {α : Type u_1} [Preorder α] (s t : Set α) : Prop

A valid move in the poset game is to change set t to set s, whenever s = t \ Ici a for some a ∈ t.

In a WQO, this relation is well-founded.

Equations

• GameGraph.Poset.Rel s t = ∃ a ∈ t, s = t \ Set.Ici a

theorem GameGraph.Poset.subrelation_rel {α : Type u_1} [Preorder α] : Subrelation (fun (x1 x2 : Set α) => Rel x1 x2) fun (x1 x2 : Set α) => x1 ⊂ x2

theorem GameGraph.Poset.not_rel_empty {α : Type u_1} [Preorder α] (s : Set α) : ¬Rel s ∅

theorem GameGraph.Poset.rel_irrefl {α : Type u_1} [Preorder α] (s : Set α) : ¬Rel s s

instance GameGraph.Poset.instIsIrreflSetRel {α : Type u_1} [Preorder α] : IsIrrefl (Set α) fun (x1 x2 : Set α) => Rel x1 x2

theorem GameGraph.Poset.top_compl_rel_univ {α : Type u_2} [PartialOrder α] [OrderTop α] : Rel {⊤}ᶜ Set.univ

theorem GameGraph.Poset.rel_univ_of_rel_top_compl {α : Type u_2} [PartialOrder α] [OrderTop α] {s : Set α} (h : Rel s {⊤}ᶜ) : Rel s Set.univ

theorem GameGraph.Poset.wellFounded_rel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : WellFounded fun (x1 x2 : Set α) => Rel x1 x2

instance GameGraph.Poset.isWellFounded_rel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : IsWellFounded (Set α) fun (x1 x2 : Set α) => Rel x1 x2

Poset game

@[reducible, inline]

abbrev GameGraph.poset (α : Type u_1) [Preorder α] : GameGraph (Set α)

The poset game, played on a poset α.

Equations

• GameGraph.poset α = { moves := fun (x : Player) (x_1 : Set α) => {y : Set α | GameGraph.Poset.Rel y x_1} }

instance GameGraph.Poset.instIsWellFoundedSetIsOptionPoset {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : IsWellFounded (Set α) (poset α).IsOption

noncomputable def GameGraph.Poset.toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (s : Set α) : IGame

A state of the poset game on α.

Equations

• GameGraph.Poset.toIGame s = (GameGraph.poset α).toIGame s

@[simp]

theorem GameGraph.Poset.moves_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (p : Player) (s : Set α) : IGame.moves p (toIGame s) = toIGame '' {t : Set α | Rel t s}

theorem GameGraph.Poset.mem_moves_toIGame_of_rel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (p : Player) {s t : Set α} (h : Rel t s) : toIGame t ∈ IGame.moves p (toIGame s)

@[simp]

theorem GameGraph.Poset.neg_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (s : Set α) : -toIGame s = toIGame s

instance GameGraph.Poset.impartial_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (s : Set α) : (toIGame s).Impartial

theorem GameGraph.Poset.univ_fuzzy_zero {α : Type u_2} [PartialOrder α] [WellQuasiOrderedLE α] [OrderTop α] : toIGame Set.univ ‖ 0

Any poset game on a toIGame with a top element is won by the first player. This is proven by a strategy stealing argument with {⊤}ᶜ.