Misere combinatorial games.

@[irreducible]

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

A form is P-free if it and all of its options avoid outcome P.

Equations

• MisereGames.IsPFree g = (MisereGames.Form.Misere.Outcome.MisereOutcome g ≠ MisereGames.Outcome.P ∧ ∀ (p : MisereGames.Player), ∀ gp ∈ MisereGames.Moves.moves p g, MisereGames.IsPFree gp)

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

A predicate whose members are P-free forms.

• pfree {g : G} (h1 : A g) : IsPFree g

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

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

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

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

@[simp]

theorem MisereGames.isPFree_zero {G : Type (u + 1)} [Form G] : IsPFree 0

@[simp]

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

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

@[simp]

theorem MisereGames.isPFree_intCast {G : Type (u + 1)} [Form G] (k : ℤ) : IsPFree ↑k

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

@[simp]

theorem MisereGames.isPFree_one : IsPFree 1

theorem MisereGames.isPFree_add_one {g : GameForm} (h1 : IsPFree g) : IsPFree (g + 1)

theorem MisereGames.isPFree_add_natCast {g : GameForm} (h1 : IsPFree g) (n : ℕ) : IsPFree (g + ↑n)

theorem MisereGames.isPFree_natCast_add {g : GameForm} (h1 : IsPFree g) (n : ℕ) : IsPFree (↑n + g)

theorem MisereGames.isPFree_add_intCast {g : GameForm} (h1 : IsPFree g) (n : ℤ) : IsPFree (g + ↑n)

def MisereGames.PFreeSubset {G : Type (u + 1)} [Form G] (A : G → Prop) (g : G) : Prop

The P-free subpredicate of A.

Equations

• MisereGames.PFreeSubset A g = (A g ∧ MisereGames.IsPFree g)

theorem MisereGames.PFreeSubset.mem {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (h : PFreeSubset A g) : A g

theorem MisereGames.PFreeSubset.isPFree {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (h : PFreeSubset A g) : IsPFree g

theorem MisereGames.PFreeSubset.mk {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (h_mem : A g) (h_isPFree : IsPFree g) : PFreeSubset A g

theorem MisereGames.pfreeSubset_iff {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} : PFreeSubset A g ↔ A g ∧ IsPFree g

instance MisereGames.instPFreePFreeSubset {G : Type (u + 1)} [Form G] {A : G → Prop} : PFree (PFreeSubset A)

instance MisereGames.instClosedUnderNegPFreeSubset {G : Type (u + 1)} [Form G] {A : G → Prop} [Form.ClosedUnderNeg A] : Form.ClosedUnderNeg (PFreeSubset A)

instance MisereGames.instHasNatPFreeSubset {G : Type (u + 1)} [Form G] {A : G → Prop} [Form.HasNat A] : Form.HasNat (PFreeSubset A)

instance MisereGames.instHasIntPFreeSubset {G : Type (u + 1)} [Form G] {A : G → Prop} [Form.HasInt A] : Form.HasInt (PFreeSubset A)

instance MisereGames.instHereditaryPFreeSubset {G : Type (u + 1)} [Form G] {A : G → Prop} [Form.Hereditary A] : Form.Hereditary (PFreeSubset A)

instance MisereGames.instClosedUnderAddNatGameFormPFreeSubset {A : GameForm → Prop} [Form.ClosedUnderAddNat A] : Form.ClosedUnderAddNat (PFreeSubset A)

theorem MisereGames.PFree.misereOutcome_ne_P_of_pfree {A : GameForm → Prop} [PFree A] {g : GameForm} (h1 : A g) : Form.Misere.Outcome.MisereOutcome g ≠ Outcome.P

theorem MisereGames.PFree.isPFree_ofMoves {A : GameForm → Prop} [PFree A] {g gp : GameForm} {p : Player} (h1 : A g) (h2 : gp ∈ Moves.moves p g) : IsPFree gp

theorem MisereGames.PFree.exists_move_of_winsGoingFirst_not_isEnd {A : GameForm → Prop} [PFree A] {g : GameForm} {p : Player} (h1 : ¬Form.IsEnd p g) (h2 : A g) (h3 : Form.Misere.Outcome.WinsGoingFirst p g) : ∃ gr ∈ Moves.moves p g, Form.Misere.Outcome.WinsGoingFirst p gr

theorem MisereGames.PFree.misereOutcome_add_one_R_of_misereOutcome_R {A : GameForm → Prop} [PFree A] {g : GameForm} (h0 : A g) (h1 : Form.Misere.Outcome.MisereOutcome g = Outcome.R) : Form.Misere.Outcome.MisereOutcome (g + 1) = Outcome.R

theorem MisereGames.PFree.misereOutcome_add_natCast_R_of_misereOutcome_R {A : GameForm → Prop} [PFree A] {g : GameForm} (n : ℕ) (h0 : A g) (h1 : Form.Misere.Outcome.MisereOutcome g = Outcome.R) : Form.Misere.Outcome.MisereOutcome (g + ↑n) = Outcome.R

theorem MisereGames.PFree.misereOutcome_sub_one_L_of_misereOutcome_L {A : GameForm → Prop} [PFree A] {g : GameForm} (h0 : A g) (h1 : Form.Misere.Outcome.MisereOutcome g = Outcome.L) : Form.Misere.Outcome.MisereOutcome (g + -1) = Outcome.L

theorem MisereGames.PFree.misereOutcome_sub_natCast_L_of_misereOutcome_L {A : GameForm → Prop} [PFree A] {g : GameForm} (n : ℕ) (h0 : A g) (h1 : Form.Misere.Outcome.MisereOutcome g = Outcome.L) : Form.Misere.Outcome.MisereOutcome (g + -↑n) = Outcome.L

theorem MisereGames.PFree.misereOutcome_of_isEnd {A : GameForm → Prop} [PFree A] {g : GameForm} {p : Player} (h1 : A g) (h2 : Form.IsEnd p g) : Form.Misere.Outcome.MisereOutcome g = Outcome.N ∨ Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayers p p

theorem MisereGames.PFree.misereOutcome_of_isEnd_left {A : GameForm → Prop} [PFree A] {g : GameForm} (h1 : A g) (h2 : Form.IsEnd Player.left g) : Form.Misere.Outcome.MisereOutcome g = Outcome.N ∨ Form.Misere.Outcome.MisereOutcome g = Outcome.L

theorem MisereGames.PFree.misereOutcome_of_isEnd_right {A : GameForm → Prop} [PFree A] {g : GameForm} (h1 : A g) (h2 : Form.IsEnd Player.right g) : Form.Misere.Outcome.MisereOutcome g = Outcome.N ∨ Form.Misere.Outcome.MisereOutcome g = Outcome.R

theorem MisereGames.PFree.not_isEndLike_right_add_of_L {A : GameForm → Prop} [PFree A] {g h : GameForm} (hAg : A g) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) : ¬Form.IsEndLike Player.right (g + h)

theorem MisereGames.PFree.isStrongTest_left {g : GameForm} (hp : IsPFree g) (ho : Form.Misere.Outcome.MisereOutcome g ≠ Outcome.R) : Form.IsStrongTest Player.left g

theorem MisereGames.PFree.isStrongTest_right {g : GameForm} (h_isPFree : IsPFree g) (h_outcome : Form.Misere.Outcome.MisereOutcome g ≠ Outcome.L) : Form.IsStrongTest Player.right g