LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Games

Auxiliary declarations for the Borel determinacy formalization.

structure GaleStewartGame.Game (A : Type u_2) : Type u_2

a Gale-Stewart game is given by a tree of valid plays (usually pruned) and a payoff set specifying the winner of an infinite play a : player 0 wins if and only if a ∈ G.payoff

• tree : ↥(Descriptive.tree A)

  Auxiliary declaration for the Borel determinacy formalization.

• payoff : Set ↑(Descriptive.Tree.body self.tree)

  Auxiliary declaration for the Borel determinacy formalization.

theorem GaleStewartGame.Game.ext_iff {A : Type u_2} {x y : Game A} : x = y ↔ x.tree = y.tree ∧ x.payoff ≍ y.payoff

theorem GaleStewartGame.Game.ext {A : Type u_2} {x y : Game A} (tree : x.tree = y.tree) (payoff : x.payoff ≍ y.payoff) : x = y

theorem GaleStewartGame.subtype_payoff {A : Type u_1} {G G' : Game A} (h : G = G') : Subtype.val '' G.payoff = Subtype.val '' G'.payoff

theorem GaleStewartGame.Game.ext' {A : Type u_1} {G G' : Game A} (ht : G.tree = G'.tree) (hp : Subtype.val '' G.payoff = Subtype.val '' G'.payoff) : G = G'

theorem GaleStewartGame.Game.ext'_iff {A : Type u_1} {G G' : Game A} : G = G' ↔ G.tree = G'.tree ∧ Subtype.val '' G.payoff = Subtype.val '' G'.payoff

def GaleStewartGame.Game.residual {A : Type u_1} (G : Game A) (x : List A) : Game A

The residual game starting in position x

Equations

• G.residual x = { tree := Descriptive.Tree.subAt G.tree x, payoff := Descriptive.Tree.body.append x ⁻¹' if x.length % 2 = 0 then G.payoff else G.payoffᶜ }

@[simp]

theorem GaleStewartGame.Game.residual_tree {A : Type u_1} (G : Game A) (x : List A) : (G.residual x).tree = Descriptive.Tree.subAt G.tree x

@[simp]

theorem GaleStewartGame.Game.residual_payoff_even {A : Type u_1} (G : Game A) (x : List A) (h : x.length % 2 = 0) : (G.residual x).payoff = Descriptive.Tree.body.append x ⁻¹' G.payoff

@[simp]

theorem GaleStewartGame.Game.residual_payoff_odd {A : Type u_1} (G : Game A) (x : List A) (h : x.length % 2 = 1) : (G.residual x).payoff = (Descriptive.Tree.body.append x ⁻¹' G.payoff)ᶜ

@[simp]

theorem GaleStewartGame.Game.residual_nil {A : Type u_1} (G : Game A) : G.residual [] = G

@[simp]

theorem GaleStewartGame.Game.residual_append {A : Type u_1} (G : Game A) (x y : List A) : (G.residual x).residual y = G.residual (x ++ y)

theorem GaleStewartGame.Game.empty_of_tree {A : Type u_1} (G : Game A) (h : G.tree = ⊥) : G = { tree := ⊥, payoff := ∅ }

theorem GaleStewartGame.Game.residual_notMem {A : Type u_1} (G : Game A) (x : List A) (h : x ∉ G.tree) : G.residual x = { tree := ⊥, payoff := ∅ }

@[reducible, inline]

abbrev GaleStewartGame.PreStrategy.subgame {A : Type u_1} {p : Player} {G : Game A} (S : PreStrategy G.tree p) : Game A

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.subgame = { tree := S.subtree, payoff := Subtype.val ⁻¹' Subtype.val '' G.payoff }

def GaleStewartGame.Player.payoff {A : Type u_1} (p : Player) (G : Game A) : Set ↑(Descriptive.Tree.body G.tree)

player p wins if and only if the resulting play lies in p.payoff G

Equations

• GaleStewartGame.Player.zero.payoff G = G.payoff
• GaleStewartGame.Player.one.payoff G = G.payoffᶜ

@[simp]

theorem GaleStewartGame.Player.payoff_zero {A : Type u_1} {G : Game A} : zero.payoff G = G.payoff

@[simp]

theorem GaleStewartGame.Player.payoff_one {A : Type u_1} {G : Game A} : one.payoff G = G.payoffᶜ

@[simp]

theorem GaleStewartGame.Player.payoff_swap {A : Type u_1} {p : Player} {G : Game A} : p.swap.payoff G = (p.payoff G)ᶜ

@[simp]

theorem GaleStewartGame.Player.payoff_swap_residual {A : Type u_1} {p : Player} {G : Game A} {x : List A} : (residual x p.swap).payoff G = ((residual x p).payoff G)ᶜ

@[simp]

theorem GaleStewartGame.Player.payoff_residual {A : Type u_1} {p : Player} {G : Game A} (x : List A) : p.payoff (G.residual x) = Descriptive.Tree.body.append x ⁻¹' (residual x p).payoff G

theorem GaleStewartGame.subtype_val_player_payoff {A : Type u_1} {p : Player} {G G' : Game A} {p' : Player} (h : G = G') (hp : p = p') : Subtype.val '' p.payoff G = Subtype.val '' p'.payoff G'

def GaleStewartGame.PreStrategy.IsWinning {A : Type u_1} {p : Player} {G : Game A} (s : PreStrategy G.tree p) : Prop

A pre-strategy is winning if all compatible plays are won. Keeping this as a definition lets API-level simp lemmas remain stated in terms of winning strategies.

Equations

• s.IsWinning = (Descriptive.Tree.body s.subtree ⊆ Subtype.val '' p.payoff G)

theorem GaleStewartGame.PreStrategy.sub_winning {A : Type u_1} {p : Player} {G : Game A} {s t : PreStrategy G.tree p} (h : s ≤ t) (h' : t.IsWinning) : s.IsWinning

theorem GaleStewartGame.PreStrategy.IsWinning.residual {A : Type u_1} {p : Player} {G : Game A} {s : PreStrategy G.tree p} (h : s.IsWinning) (x : ↥s.subtree) : (s.residual ↑x).IsWinning

theorem GaleStewartGame.PreStrategy.IsWinning.choose {A : Type u_1} {p : Player} {G : Game A} (s : QuasiStrategy G.tree p) (h : s.fst.IsWinning) : ⋯.choose.pre.IsWinning

theorem GaleStewartGame.Game.exists_isWinning {A : Type u_1} (S T : Game A) (p q : Player) (hS : S = T) (hp : p = q) : (∃ (s : Strategy S.tree p), s.pre.IsWinning) ↔ ∃ (s : Strategy T.tree q), s.pre.IsWinning

def GaleStewartGame.Game.ExistsWinning {A : Type u_1} (G : Game A) (p : Player) : Prop

whether a winning strategy exists for player p

Equations

• G.ExistsWinning p = ∃ (S : GaleStewartGame.Strategy G.tree p), S.pre.IsWinning

theorem GaleStewartGame.Game.existsWinning_iff_quasi {A : Type u_1} {p : Player} {G : Game A} : G.ExistsWinning p ↔ ∃ (S : QuasiStrategy G.tree p), S.fst.IsWinning

theorem GaleStewartGame.Game.ExistsWinning.pruned {A : Type u_1} {p : Player} {G : Game A} (hW : G.ExistsWinning p) (hW' : G.ExistsWinning p.swap) : Descriptive.Tree.IsPruned G.tree

theorem GaleStewartGame.Game.ExistsWinning.not_both_winning {A : Type u_1} {p : Player} {G : Game A} (hW : G.ExistsWinning p) (hNe : [] ∈ G.tree) : ¬G.ExistsWinning p.swap

def GaleStewartGame.Game.AllWinning {A : Type u_1} (G : Game A) (p : Player) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• G.AllWinning p = (p.payoff G = Set.univ)

theorem GaleStewartGame.Game.AllWinning.residual {A : Type u_1} {p : Player} {G : Game A} (hW : G.AllWinning p) (x : List A) : (G.residual x).AllWinning (Player.residual x p)

def GaleStewartGame.Game.IsDetermined {A : Type u_1} (G : Game A) : Prop

a game is determined if some player has a winning strategy

Equations

• G.IsDetermined = ∃ (p : GaleStewartGame.Player), G.ExistsWinning p