Documentation

CombinatorialGames.Misere.Blocking

@[irreducible]

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

A blocked end for player p: g is a p-end, and for every opponent move gr, either gr is again a p blocked end, or else p has a move from gr to a p blocked end. This is weaker than IsDeadEnd: every p dead end is a p blocked end (isBlockedEnd_of_isDeadEnd), but not the other way around.

Equations

Form.IsBlockedEnd p g = (Form.IsEnd p g ∧ ∀ gr ∈ Moves.moves (-p) g, Form.IsBlockedEnd p gr ∨ ∃ (grl : G) (_ : grl ∈ Moves.moves p gr), Form.IsBlockedEnd p grl)

Instances For

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

IsBlockedEnd p g ↔ IsEnd p g ∧ ∀ gr ∈ moves (-p) g, IsBlockedEnd p gr ∨ ∃ (grl : G) (_ : grl ∈ moves p gr), IsBlockedEnd p grl

theorem Form.isEnd_of_isBlockedEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsBlockedEnd p g) :

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

gr ∈ moves (-p) g → IsBlockedEnd p gr ∨ ∃ (grl : G) (_ : grl ∈ moves p gr), IsBlockedEnd p grl

@[simp]

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

gp ∉ moves p g

@[irreducible]

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

IsBlockedEnd p g

A dead end is a blocked end.

@[irreducible]

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

IsBlockedEnd p (g + h)

@[simp]

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

IsBlockedEnd p (-g) ↔ IsBlockedEnd (-p) g

@[simp]

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

IsBlockedEnd p 0

@[simp]

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

IsBlockedEnd Player.right ↑n

@[simp]

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

IsBlockedEnd Player.right ↑k

@[simp]

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

IsBlockedEnd Player.left ↑k

@[irreducible]

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

A game is blocking if every end is a blocked end, hereditarily.

Equations

Form.IsBlocking g = ((∀ (p : Player), Form.IsEnd p g → Form.IsBlockedEnd p g) ∧ ∀ (p : Player), ∀ gp ∈ Moves.moves p g, Form.IsBlocking gp)

Instances For

@[simp]

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

IsBlockedEnd p g

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

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

@[irreducible]

theorem Form.isBlocking_of_isDeadEnding {G : Type (u + 1)} [Form G] {g : G} (h1 : IsDeadEnding g) :

Every dead-ending game is blocking.

@[simp, irreducible]

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

IsBlocking (g + h)

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

ClosedUnderAdd IsBlocking

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

ClosedUnderNeg IsBlocking

@[simp]

theorem Form.isBlocking_zero {G : Type (u + 1)} [Form G] :

@[simp]

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

IsBlocking ↑n

@[simp]

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

IsBlocking ↑k

@[simp]

theorem Form.isBlocking_one {G : Type (u + 1)} [Form G] :

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

The short blocking universe.

short : IsShort g
blocking : IsBlocking g

Instances For

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

Hereditary ShortBlocking

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

ClosedUnderNeg ShortBlocking

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

ClosedUnderAdd ShortBlocking

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

ClosedUnderDicotic IsShort ShortBlocking

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

ShortUniverse ShortBlocking

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

HasNat ShortBlocking

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

ClosedUnderAddNat ShortBlocking

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

HasInt ShortBlocking

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

isBlocking {g : G} (hA : A g) : IsBlocking g

Instances

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

Blocking IsBlocking

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

Blocking ShortBlocking

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

instance GameForm.instIntegerInvertibleShortBlocking :

IntegerInvertible Form.ShortBlocking

This is Davies, Miller, Milley (Lemma 4.5 on p. 26)

theorem GameForm.IsBlocking.strong_of_isStrongTest {A : GameForm → Prop} [Form.Blocking A] {p : Player} {g : GameForm} (h_test : Form.IsStrongTest p g) :

Form.Strong A g p

This is one direction of Davies, Milley (Theorem 3.1 on p. 7)