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

• ConcreteGame.Poset.impartial_toIGame: poset games are impartial
• ConcreteGame.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 ConcreteGame.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

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

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

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

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

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

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

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

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

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

Poset game

@[reducible, inline]

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

The poset game, played on a poset α.

Equations

• ConcreteGame.poset α = ConcreteGame.ofImpartial fun (x : Set α) => {y : Set α | ConcreteGame.Poset.Rel y x}

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

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

A state of the poset game on α.

Equations

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

@[simp]

theorem ConcreteGame.Poset.leftMoves_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (s : Set α) : (toIGame s).leftMoves = toIGame '' {t : Set α | Rel t s}

@[simp]

theorem ConcreteGame.Poset.rightMoves_toIGame {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] (s : Set α) : (toIGame s).rightMoves = toIGame '' {t : Set α | Rel t s}

@[simp]

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

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

theorem ConcreteGame.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 {⊤}ᶜ.