LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Player

Auxiliary declarations for the Borel determinacy formalization.

inductive GaleStewartGame.Player : Type

a player in a Gale-Stewart game

• zero : Player
• one : Player

def GaleStewartGame.tacticCasesPlayer : Lean.ParserDescr

Tactic support used by the Borel determinacy formalization.

Equations

• GaleStewartGame.tacticCasesPlayer = Lean.ParserDescr.node `GaleStewartGame.tacticCasesPlayer 1024 (Lean.ParserDescr.nonReservedSymbol "casesPlayer" false)

def GaleStewartGame.tacticCasesPlayers : Lean.ParserDescr

Tactic support used by the Borel determinacy formalization.

Equations

• GaleStewartGame.tacticCasesPlayers = Lean.ParserDescr.node `GaleStewartGame.tacticCasesPlayers 1024 (Lean.ParserDescr.nonReservedSymbol "casesPlayers" false)

def GaleStewartGame.tacticSynthIsPosition : Lean.ParserDescr

Tactic support used by the Borel determinacy formalization.

Equations

• GaleStewartGame.tacticSynthIsPosition = Lean.ParserDescr.node `GaleStewartGame.tacticSynthIsPosition 1024 (Lean.ParserDescr.nonReservedSymbol "synthIsPosition" false)

def GaleStewartGame.Player.toNat : Player → ℕ

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Player.zero.toNat = 0
• GaleStewartGame.Player.one.toNat = 1

theorem GaleStewartGame.Player.apply_ite_toNat (P : Prop) [Decidable P] (a b : Player) : (if P then a else b).toNat = if P then a.toNat else b.toNat

Auxiliary declaration for the Borel determinacy formalization.

@[simp]

theorem GaleStewartGame.Player.zero_toNat : zero.toNat = 0

@[simp]

theorem GaleStewartGame.Player.one_toNat : one.toNat = 1

theorem GaleStewartGame.Player.ext (p q : Player) (h : p.toNat = q.toNat) : p = q

theorem GaleStewartGame.Player.ext_iff {p q : Player} : p = q ↔ p.toNat = q.toNat

def GaleStewartGame.Player.swap : Player → Player

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Player.zero.swap = GaleStewartGame.Player.one
• GaleStewartGame.Player.one.swap = GaleStewartGame.Player.zero

theorem GaleStewartGame.Player.apply_ite_swap (P : Prop) [Decidable P] (a b : Player) : (if P then a else b).swap = if P then a.swap else b.swap

Auxiliary declaration for the Borel determinacy formalization.

@[simp]

theorem GaleStewartGame.Player.swap_zero : zero.swap = one

@[simp]

theorem GaleStewartGame.Player.swap_one : one.swap = zero

def GaleStewartGame.Player.residual {A : Type u_1} (x : List A) (p : Player) : Player

if p moves in position [], then p.residual x moves in position x

Equations

• GaleStewartGame.Player.residual x p = if x.length % 2 = 0 then p else p.swap

def GaleStewartGame.IsPosition {A : Type u_1} (x : List A) (p : Player) : Prop

is player p to move in position x?

Equations

• GaleStewartGame.IsPosition x p = (x.length % 2 = p.toNat)

@[simp]

theorem GaleStewartGame.Player.residual_swap {A : Type u_1} (x : List A) (p : Player) : (residual x p).swap = residual x p.swap

@[simp]

theorem GaleStewartGame.Player.residual_residual {A : Type u_1} (p : Player) {x y : List A} : residual y (residual x p) = residual (x ++ y) p

@[simp]

theorem GaleStewartGame.Player.residual_even {A : Type u_1} (x : List A) (p : Player) (h : x.length % 2 = 0) : residual x p = p

@[simp]

theorem GaleStewartGame.Player.residual_odd {A : Type u_1} (x : List A) (p : Player) (h : x.length % 2 = 1) : residual x p = p.swap

@[simp]

theorem GaleStewartGame.Player.residual_append_both {A : Type u_1} (x : List A) (p : Player) {y : List A} : residual (x ++ (y ++ x)) p = residual y p

@[simp]

theorem GaleStewartGame.Player.residual_cons {A : Type u_1} (x : List A) (p : Player) {a : A} : residual (a :: x) p = (residual x p).swap

@[simp]

theorem GaleStewartGame.Player.residual_append_cons {A : Type u_1} (x : List A) (p : Player) {a : A} {y : List A} : residual (x ++ a :: y) p = (residual (x ++ y) p).swap

theorem GaleStewartGame.Player.residual_concat {A : Type u_1} (x : List A) (p : Player) {a : A} : residual (x ++ [a]) p = (residual x p).swap

theorem GaleStewartGame.Player.residual_concat2 {A : Type u_1} (x : List A) (p : Player) {a b : A} : residual (x ++ [a, b]) p = residual x p