Documentation

CombinatorialGames.Misere.PFree

@[irreducible]

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

Equations

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

Instances For

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

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

Instances

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

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

Form.ClosedUnderNeg IsPFree

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

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

@[simp]

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

@[simp]

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

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

Form.HasNat IsPFree

@[simp]

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

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

Form.HasInt IsPFree

@[simp]

theorem isPFree_one :

@[irreducible]

theorem isPFree_add_one {g : GameForm} (h1 : IsPFree g) :

IsPFree (g + 1)

theorem isPFree_add_natCast {g : GameForm} (h1 : IsPFree g) (n : ℕ) :

IsPFree (g + ↑n)

theorem isPFree_natCast_add {g : GameForm} (h1 : IsPFree g) (n : ℕ) :

IsPFree (↑n + g)

theorem isPFree_add_intCast {g : GameForm} (h1 : IsPFree g) (n : ℤ) :

IsPFree (g + ↑n)

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

Equations

PFreeSubset A g = (A g ∧ IsPFree g)

Instances For

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

A g

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

theorem 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 pfreeSubset_iff {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} :

PFreeSubset A g ↔ A g ∧ IsPFree g

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

PFree (PFreeSubset A)

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

Form.ClosedUnderNeg (PFreeSubset A)

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

Form.HasNat (PFreeSubset A)

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

Form.HasInt (PFreeSubset A)

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

Form.Hereditary (PFreeSubset A)

instance instClosedUnderAddNatGameFormPFreeSubset {A : GameForm → Prop} [Form.ClosedUnderAddNat A] :

Form.ClosedUnderAddNat (PFreeSubset A)

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

Form.Short (PFreeSubset A)

theorem PFree.misereOutcome_ne_P_of_pfree {A : GameForm → Prop} [PFree A] {g : GameForm} (h1 : A g) :

Form.Misere.Outcome.MisereOutcome g ≠ Outcome.P

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

theorem 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 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 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 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 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 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 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 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 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)

@[irreducible]

theorem PFree.isStrongTest {p : Player} {g : GameForm} (hp : IsPFree g) (ho : Form.Misere.Outcome.MisereOutcome g ≠ Outcome.ofPlayer (-p)) :

Form.IsStrongTest p g

theorem PFree.misereOutcome_of_not_winsGoingFirst {g : GameForm} (h_pfree : IsPFree g) (h_not_right : ¬Form.Misere.Outcome.WinsGoingFirst Player.right g) :

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

theorem PFree.pfreeSubset_short_ofSets {L R : Set GameForm} [Small.{u, u + 1} ↑L] [Small.{u, u + 1} ↑R] {A : GameForm → Prop} [ClosedUnderDicotic Form.IsShort A] [Form.Short A] (h_L_mem : ∀ gl ∈ L, PFreeSubset A gl) (h_R_mem : ∀ gr ∈ R, PFreeSubset A gr) (h_L_nonempty : L.Nonempty) (h_L_finite : L.Finite) (h_R_nonempty : R.Nonempty) (h_R_finite : R.Finite) (h_outcome_ne_P : Form.Misere.Outcome.MisereOutcome !{L | R} ≠ Outcome.P) :

PFreeSubset A !{L | R}

theorem PFree.not_misereGE_zero_of_misereOutcome_L {U : GameForm → Prop} [Form.HasInt U] {h : GameForm} (h_out : Form.Misere.Outcome.MisereOutcome h = Outcome.L) :

¬0 ≥m (PFreeSubset U)h

If MisereOutcome H = L then 0 ≥m H fails, immediately from testing at x = 0 (MisereOutcome 0 = N is not ≥ L, since L is the top of the outcome order).

theorem PFree.misereGE_iff_zero_of_isEnd_left_isEnd_right {U : GameForm → Prop} {g h : GameForm} (h_g_left : Form.IsEnd Player.left g) (h_g_right : Form.IsEnd Player.right g) :

g ≥m (PFreeSubset U)h ↔ 0 ≥m (PFreeSubset U)h

If g is both a Left and a Right end then g = 0 literally (both_ends_eq_zero), so comparing against g is just comparing against 0.

theorem PFree.misereGE_zero_of_isEnd_left_isEnd_right {U : GameForm → Prop} {h : GameForm} (h_h_left : Form.IsEnd Player.left h) (h_h_right : Form.IsEnd Player.right h) :

0 ≥m (PFreeSubset U)h

If H is both a Left and a Right end then H = 0, so 0 ≥m H is 0 ≥m 0, true by reflexivity.