LeanPool.MisereGames.Misere.DeadEnding

Misere combinatorial games.

source

@[irreducible]

def MisereGames.Form.IsDeadEnd {G : Type (u + 1)} [Form G] (p : Player) (g : G) :

Prop

A p-dead end is a p-end whose options are again p-dead ends.

Equations

MisereGames.Form.IsDeadEnd p g = (MisereGames.Form.IsEnd p g ∧ ∀ gp ∈ MisereGames.Moves.moves (-p) g, MisereGames.Form.IsDeadEnd p gp)

Instances For

source

theorem MisereGames.Form.isDeadEnd_def {G : Type (u + 1)} [Form G] (p : Player) (g : G) :

IsDeadEnd p g ↔ IsEnd p g ∧ ∀ gp ∈ moves (-p) g, IsDeadEnd p gp

source

theorem MisereGames.Form.isEnd_of_isDeadEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) :

IsEnd p g

source

theorem MisereGames.Form.IsDeadEnd.hereditary_def {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) (gp : G) :

gp ∈ moves (-p) g → IsDeadEnd p gp

source

@[simp]

theorem MisereGames.Form.not_mem_moves_of_isDeadEnd {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : IsDeadEnd p g) :

gp ∉ moves p g

source

theorem MisereGames.Form.player_eq_neg_of_isDeadEnd_mem_moves {G : Type (u + 1)} [Form G] {g gp : G} {p1 p2 : Player} (h1 : IsDeadEnd p1 g) (h2 : gp ∈ moves p2 g) :

p2 = -p1

source

theorem MisereGames.Form.isDeadEnd_of_mem_moves {G : Type (u + 1)} [Form G] {g gp : G} {p1 p2 : Player} (h1 : IsDeadEnd p1 g) (h2 : gp ∈ moves p2 g) :

IsDeadEnd p1 gp

source

theorem MisereGames.Form.isDeadEnd_isOption {G : Type (u + 1)} [Form G] {p : Player} {g gp : G} (h1 : IsDeadEnd p g) (h2 : IsOption gp g) :

gp ∈ moves (-p) g

source

theorem MisereGames.Form.isDeadEnd_of_isOption {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : IsDeadEnd p g) (h2 : IsOption gp g) :

IsDeadEnd p gp

source

theorem MisereGames.Form.IsDeadEnd.add {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsDeadEnd p g) (h2 : IsDeadEnd p h) :

IsDeadEnd p (g + h)

source

@[simp]

theorem MisereGames.Form.IsDeadEnd.neg_iff {G : Type (u + 1)} [Form G] {g : G} {p : Player} :

IsDeadEnd p (-g) ↔ IsDeadEnd (-p) g

source

theorem MisereGames.Form.isDeadEnd_zero {G : Type (u + 1)} [Form G] {p : Player} :

IsDeadEnd p 0

source

theorem MisereGames.Form.isDeadEnd_right_natCast {G : Type (u + 1)} [Form G] (n : ℕ) :

IsDeadEnd Player.right ↑n

source

theorem MisereGames.Form.isDeadEnd_right_nonneg_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≥ 0) :

IsDeadEnd Player.right ↑k

source

theorem MisereGames.Form.isDeadEnd_left_nonpos_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≤ 0) :

IsDeadEnd Player.left ↑k

source

theorem MisereGames.Form.isPFree_of_isDeadEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) :

IsPFree g

source

@[irreducible]

def MisereGames.Form.IsDeadEnding {G : Type (u + 1)} [Form G] (g : G) :

Prop

A form is dead-ending when all of its end options are dead ends, hereditarily.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MisereGames.Form.isDeadEnd_of_isDeadEnding {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnding g) (h2 : IsEnd p g) :

IsDeadEnd p g

source

theorem MisereGames.Form.isDeadEnding_of_mem_moves {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsDeadEnding g) (h2 : h ∈ moves p g) :

IsDeadEnding h

source

theorem MisereGames.Form.isDeadEnding_of_isOption {G : Type (u + 1)} [Form G] {g g' : G} (h1 : IsDeadEnding g) (h2 : IsOption g' g) :

IsDeadEnding g'

source

instance MisereGames.Form.instHereditaryIsDeadEnding {G : Type (u + 1)} [Form G] :

Hereditary IsDeadEnding

source

class MisereGames.Form.DeadEnding {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A predicate whose members are dead-ending forms.

isDeadEnding {g : G} (hA : A g) : IsDeadEnding g

Instances

source

instance MisereGames.Form.instDeadEndingIsDeadEnding {G : Type (u + 1)} [Form G] :

DeadEnding IsDeadEnding

source

@[simp]

theorem MisereGames.Form.DeadEnding.IsDeadEnding.add {G : Type (u + 1)} [Form G] {g h : G} (h1 : IsDeadEnding g) (h2 : IsDeadEnding h) :

IsDeadEnding (g + h)

source

instance MisereGames.Form.DeadEnding.instClosedUnderNegIsDeadEnding {G : Type (u + 1)} [Form G] :

ClosedUnderNeg IsDeadEnding

source

@[simp]

theorem MisereGames.Form.DeadEnding.isDeadEnding_zero {G : Type (u + 1)} [Form G] :

IsDeadEnding 0

source

@[simp]

theorem MisereGames.Form.DeadEnding.isDeadEnding_natCast {G : Type (u + 1)} [Form G] (n : ℕ) :

IsDeadEnding ↑n

source

@[simp]

theorem MisereGames.Form.DeadEnding.isDeadEnding_intCast {G : Type (u + 1)} [Form G] (k : ℤ) :

IsDeadEnding ↑k

source

@[simp]

theorem MisereGames.Form.DeadEnding.isDeadEnding_one {G : Type (u + 1)} [Form G] :

IsDeadEnding 1

source

structure MisereGames.Form.DeadEnding.ShortDeadEnding {G : Type (u + 1)} [Form G] (g : G) :

Prop

Forms that are both short and dead-ending.

short : IsShort g
dead_ending : IsDeadEnding g

Instances For

source

instance MisereGames.Form.DeadEnding.instShortDeadEnding {G : Type (u + 1)} [Form G] :

DeadEnding ShortDeadEnding

source

instance MisereGames.Form.DeadEnding.instHereditaryShortDeadEnding {G : Type (u + 1)} [Form G] :

Hereditary ShortDeadEnding

source

instance MisereGames.Form.DeadEnding.instShortUniverseShortDeadEnding {G : Type (u + 1)} [Form G] :

ShortUniverse ShortDeadEnding

source

instance MisereGames.Form.DeadEnding.instHasNatShortDeadEnding {G : Type (u + 1)} [Form G] :

HasNat ShortDeadEnding

source

instance MisereGames.Form.DeadEnding.instHasIntShortDeadEnding {G : Type (u + 1)} [Form G] :

HasInt ShortDeadEnding

source

theorem MisereGames.GameForm.DeadEnding.isDeadEnd_left_misereOutcome_L (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.left g) :

Form.Misere.Outcome.MisereOutcome g = Outcome.L

This is [Milley, Renault (Lemma 3 on p. 5)][milley:DeadEndsMisere:2013].

source

theorem MisereGames.GameForm.DeadEnding.isDeadEnd_right_misereOutcome_R (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.right g) :

Form.Misere.Outcome.MisereOutcome g = Outcome.R

This is [Milley, Renault (Lemma 3 on p. 5)][milley:DeadEndsMisere:2013].

source

instance MisereGames.GameForm.DeadEnding.instIntegerInvertibleShortDeadEnding :

IntegerInvertible Form.DeadEnding.ShortDeadEnding

source

instance MisereGames.GameForm.DeadEnding.instPropertyXShortDeadEnding :

IntegerInvertible.PropertyX Form.DeadEnding.ShortDeadEnding

source

theorem MisereGames.Form.misereGE_iff_strong_of_isDeadEnd_left {G : Type (u + 1)} [Form G] {A IsAmbient : G → Prop} (h_promain : Promain IsAmbient A) {g h : G} (h_g_dead : IsDeadEnd Player.left g) (h_h_dead : IsDeadEnd Player.left h) (h_g : IsAmbient g) (h_h : IsAmbient h) :

g ≥m A h ↔ (IsEndLike Player.right g → Strong A h Player.right) ∧ ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr ≥m A hr

For Left dead ends g and h (with A promain), comparison g ≥m A h reduces to the Right proviso plus maintenance of Right's moves.

source

theorem MisereGames.Form.misereGE_iff_isEndLike_of_isDeadEnd_left {G : Type (u + 1)} [Form G] {A IsAmbient : G → Prop} (h_promain : Promain IsAmbient A) (hA_end : ∃ (x : G), A x ∧ IsEnd Player.left x ∧ IsEnd Player.right x) {g h : G} (h_g_dead : IsDeadEnd Player.left g) (h_h_dead : IsDeadEnd Player.left h) (h_g : IsAmbient g) (h_h : IsAmbient h) :

g ≥m A h ↔ (IsEndLike Player.right g → IsEndLike Player.right h) ∧ ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr ≥m A hr

For Left dead ends, if A has a form that is an end for both players (such as 0), the Right proviso simplifies to Right end-like positions being preserved.

source