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

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

def posetRel {α : 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

• posetRel s t = ∃ a ∈ t, s = t \ Set.Ici a

theorem subrelation_posetRel {α : Type u_1} [Preorder α] : Subrelation (fun (x1 x2 : Set α) => posetRel x1 x2) fun (x1 x2 : Set α) => x1 ⊂ x2

theorem not_posetRel_empty {α : Type u_1} [Preorder α] (s : Set α) : ¬posetRel s ∅

theorem posetRel_irrefl {α : Type u_1} [Preorder α] (s : Set α) : ¬posetRel s s

instance instIsIrreflSetPosetRel {α : Type u_1} [Preorder α] : IsIrrefl (Set α) fun (x1 x2 : Set α) => posetRel x1 x2

theorem top_compl_posetRel_univ {α : Type u_2} [PartialOrder α] [OrderTop α] : posetRel {⊤}ᶜ Set.univ

theorem posetRel_univ_of_posetRel_top_compl {α : Type u_2} [PartialOrder α] [OrderTop α] {s : Set α} (h : posetRel s {⊤}ᶜ) : posetRel s Set.univ

theorem wellFounded_posetRel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : WellFounded fun (x1 x2 : Set α) => posetRel x1 x2

instance isWellFounded_posetRel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : IsWellFounded (Set α) fun (x1 x2 : Set α) => posetRel x1 x2

def IGame.Poset (α : Type u_2) [Preorder α] [WellQuasiOrderedLE α] : Type u_2

The set of states in a poset game. This is a type alias for Set α.

Equations

• IGame.Poset α = Set α

def IGame.toPoset {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : Set α ≃ Poset α

Equations

• IGame.toPoset = Equiv.refl (Set α)

def IGame.ofPoset {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : Poset α ≃ Set α

Equations

• IGame.ofPoset = Equiv.refl (IGame.Poset α)

@[simp]

theorem IGame.toPoset_ofPoset {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (a : Poset α) : toPoset (ofPoset a) = a

@[simp]

theorem IGame.ofPoset_toPoset {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (a : Set α) : ofPoset (toPoset a) = a

def IGame.Poset.rel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (a b : Poset α) : 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.

Equations

• a.rel b = posetRel (IGame.ofPoset a) (IGame.ofPoset b)

instance IGame.Poset.instIsWellFoundedRel {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : IsWellFounded (Poset α) rel

instance IGame.Poset.instWellFoundedRelation {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : WellFoundedRelation (Poset α)

Equations

• IGame.Poset.instWellFoundedRelation = { rel := IGame.Poset.rel, wf := ⋯ }

instance IGame.Poset.instConcreteGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : ConcreteGame (Poset α)

Equations

• IGame.Poset.instConcreteGame = ConcreteGame.ofImpartial IGame.Poset.rel

@[simp]

theorem IGame.Poset.neg_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (a : Poset α) : -ConcreteGame.toIGame a = ConcreteGame.toIGame a

instance IGame.Poset.impartial_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (a : Poset α) : (ConcreteGame.toIGame a).Impartial

def IGame.Poset.univ (α : Type u_2) [Preorder α] [WellQuasiOrderedLE α] : Poset α

The starting position in a poset game.

Equations

• IGame.Poset.univ α = IGame.toPoset Set.univ

theorem IGame.Poset.univ_fuzzy_zero {α : Type u_2} [PartialOrder α] [WellQuasiOrderedLE α] [OrderTop α] : ConcreteGame.toIGame (univ α) ‖ 0

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