Misere combinatorial games.

Solved

@[irreducible]

def MisereGames.GameForm.IsSolved (p : Player) (g : GameForm) : Prop

Intuitively, a position is solved for a given player if they win regardless of the moves they make.

Equations

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

theorem MisereGames.GameForm.isSolved_def (p : Player) (g : GameForm) : IsSolved p g ↔ 0 ∉ Moves.moves p g ∧ (g ≠ 0 → ¬Form.IsEnd (-p) g) ∧ ∀ (gp : GameForm), Moves.IsOption gp g → IsSolved p gp

theorem MisereGames.GameForm.isSolved_zero_not_mem {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) : 0 ∉ Moves.moves p g

theorem MisereGames.GameForm.isSolved_zero_mem {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_isOption : Moves.IsOption 0 g) : 0 ∈ Moves.moves (-p) g

theorem MisereGames.GameForm.isSolved_not_isEnd {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_ne_zero : g ≠ 0) : ¬Form.IsEnd (-p) g

theorem MisereGames.GameForm.isSolved_of_isOption {g gp : GameForm} {p : Player} (h1 : IsSolved p g) (h2 : Moves.IsOption gp g) : IsSolved p gp

theorem MisereGames.GameForm.isSolved_of_subposition {g gp : GameForm} {p : Player} (h1 : IsSolved p g) (h2 : Moves.Subposition gp g) : IsSolved p gp

theorem MisereGames.GameForm.isSolved_of_mem_moves {p : Player} {g g' : GameForm} {q : Player} (h : IsSolved p g) (hm : g' ∈ Moves.moves q g) : IsSolved p g'

theorem MisereGames.GameForm.isSolved_neg_iff {p : Player} {g : GameForm} : IsSolved (-p) (-g) ↔ IsSolved p g

@[simp]

theorem MisereGames.GameForm.isSolved_neg_iff' {p : Player} {g : GameForm} : IsSolved p (-g) ↔ IsSolved (-p) g

theorem MisereGames.GameForm.isSolved_winsGoingFirst {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) : Form.Misere.Outcome.WinsGoingFirst p g

theorem MisereGames.GameForm.isSolved_ne_zero_misereOutcome {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_ne_zero : g ≠ 0) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p

theorem MisereGames.GameForm.isSolved_add {p : Player} {g h : GameForm} (h_isSolved_g : IsSolved p g) (h_isSolved_h : IsSolved p h) : IsSolved p (g + h)

The sum of two solved games is solved.

theorem MisereGames.GameForm.not_isSolved_add_left {p : Player} {g h : GameForm} (hg : ¬IsSolved p g) : ¬IsSolved p (g + h)

theorem MisereGames.GameForm.not_isSolved_add_right {p : Player} {g h : GameForm} (hh : ¬IsSolved p h) : ¬IsSolved p (g + h)

theorem MisereGames.GameForm.isSolved_add_iff {p : Player} {g h : GameForm} : IsSolved p g ∧ IsSolved p h ↔ IsSolved p (g + h)

Integers

@[simp]

theorem MisereGames.GameForm.isSolved_zero (p : Player) : IsSolved p 0

@[simp]

theorem MisereGames.GameForm.isSolved_right_natCast (n : ℕ) : IsSolved Player.right ↑n

@[simp]

theorem MisereGames.GameForm.isSolved_right_one : IsSolved Player.right 1

theorem MisereGames.GameForm.isSolved_iff_zero {g : GameForm} : IsSolved Player.left g ∧ IsSolved Player.right g ↔ g = 0

Zero is the only game solved for both players

@[simp]

theorem MisereGames.GameForm.isSolved_right_intCast_iff (k : ℤ) : IsSolved Player.right ↑k ↔ 0 ≤ k

@[simp]

theorem MisereGames.GameForm.isSolved_left_intCast_iff (k : ℤ) : IsSolved Player.left ↑k ↔ k ≤ 0

@[simp]

theorem MisereGames.GameForm.not_isSolved_left_one : ¬IsSolved Player.left 1

theorem MisereGames.GameForm.isSolved_deadEnd {p : Player} {g : GameForm} (h_deadEnd : Form.IsDeadEnd p g) : IsSolved p g

Strides

@[irreducible]

def MisereGames.GameForm.HasStride (p : Player) (g : GameForm) (n : ℕ) : Prop

Stride measures exactly how many moves away each player is from a solved position.

Stride is not well-defined for all game forms.

Equations

• One or more equations did not get rendered due to their size.
• MisereGames.GameForm.HasStride p g 0 = MisereGames.GameForm.IsSolved p g

@[simp]

theorem MisereGames.GameForm.hasStride_eq_zero_iff {p : Player} {g : GameForm} : HasStride p g 0 ↔ IsSolved p g

The stride equals zero if the game is solved.

theorem MisereGames.GameForm.hasStride_isSolved_iff_zero {p : Player} {g : GameForm} {n : ℕ} (h_hasStride : HasStride p g n) : IsSolved p g ↔ n = 0

A game is solved if its stride equals zero.

theorem MisereGames.GameForm.hasStride_not_isSolved_iff_pos {p : Player} {g : GameForm} {n : ℕ} (h_hasStride : HasStride p g n) : ¬IsSolved p g ↔ 0 < n

theorem MisereGames.GameForm.hasStride_succ_iff {p : Player} {g : GameForm} {n : ℕ} : HasStride p g (n + 1) ↔ ¬IsSolved p g ∧ (∀ g' ∈ Moves.moves p g, ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k) ∧ (∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ ∀ g'' ∈ Moves.moves p g, ∀ (m : ℕ), HasStride (-p) g'' m → ∃ (k : ℕ), m ≤ k ∧ HasStride (-p) g' k) ∧ (∀ g' ∈ Moves.moves (-p) g, ∃ k ≤ n + 1, HasStride p g' k) ∧ (Moves.moves (-p) g ≠ ∅ → ∃ (g' : GameForm) (_ : g' ∈ Moves.moves (-p) g), HasStride p g' (n + 1))

theorem MisereGames.GameForm.hasStride_succ_support {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) (g' : GameForm) (hg' : g' ∈ Moves.moves p g) : ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k

If the stride of $G$ is not zero, then every response lowers the stride by at most one.

theorem MisereGames.GameForm.hasStride_succ_exists_best {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ ∀ g'' ∈ Moves.moves p g, ∀ (m : ℕ), HasStride (-p) g'' m → ∃ (k : ℕ), m ≤ k ∧ HasStride (-p) g' k

If the stride of $G$ is not zero, then there exist some response to stride lower by one.

theorem MisereGames.GameForm.hasStride_succ_support_neg {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) (g' : GameForm) (hg' : g' ∈ Moves.moves (-p) g) : ∃ k ≤ n + 1, HasStride p g' k

If the stride of $G$ is not zero, then every opponent move preserves the stride.

theorem MisereGames.GameForm.hasStride_succ_exists_preserve_neg {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) (h_ne : Moves.moves (-p) g ≠ ∅) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves (-p) g), HasStride p g' (n + 1)

Some opponent move preserves stride.

theorem MisereGames.GameForm.hasStride_succ_not_isEnd {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) : ¬Form.IsEnd p g

theorem MisereGames.GameForm.hasStride_unique {p : Player} {g : GameForm} {n k : ℕ} (h_n : HasStride p g n) (h_k : HasStride p g k) : n = k

If a game has stride, then the value is unique.

This is a workaround for not defining stride as a function to option ℕ.

theorem MisereGames.GameForm.hasStride_mk_iff {p : Player} (n : ℕ) {k : ℕ} {g : GameForm} (h_stride : HasStride p g n) : HasStride p g k ↔ k = n

Helper for building iff lemmas

theorem MisereGames.GameForm.hasStride_good_move_neg_stride {p : Player} {g : GameForm} {n r : ℕ} (h : HasStride p g (n + 1)) (h_r : HasStride (-p) g r) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' r

The good move preserves (-p)-stride: if HasStride p g (n+1) and HasStride (-p) g r, then the good p-move has (-p)-stride exactly r.

theorem MisereGames.GameForm.hasStride_of_mem_moves_neg {p : Player} {g g' : GameForm} {n : ℕ} (hg : HasStride p g n) (hm : g' ∈ Moves.moves (-p) g) : ∃ k ≤ n, HasStride p g' k

Opponent moves have stride ≤ n.

theorem MisereGames.GameForm.hasStride_succ_iff' {p : Player} {g : GameForm} {n m : ℕ} (h_hasStride_m : HasStride (-p) g m) : HasStride p g (n + 1) ↔ ¬IsSolved p g ∧ (∀ g' ∈ Moves.moves p g, ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k) ∧ (∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' m) ∧ (∀ g' ∈ Moves.moves (-p) g, ∃ k ≤ n + 1, HasStride p g' k) ∧ (Moves.moves (-p) g ≠ ∅ → ∃ (g' : GameForm) (_ : g' ∈ Moves.moves (-p) g), HasStride p g' (n + 1))

A variant of hasStride_succ_iff that simplifies condition B' when we know the (-p)-stride. Instead of requiring the good move to have the max (-p)-stride among all p-moves, we simply require the good move to preserve the (-p)-stride exactly.

theorem MisereGames.GameForm.hasStride_succ_exists_best' {p : Player} {g : GameForm} {n m : ℕ} (h_n : HasStride p g (n + 1)) (h_m : HasStride (-p) g m) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' m

Variant of hasStride_succ_exists_best with known opponent stride

theorem MisereGames.GameForm.hasStride_of_mem_moves {p : Player} {g g' : GameForm} {n : ℕ} (hg : HasStride p g n) (hm : g' ∈ Moves.moves p g) : ∃ (j : ℕ), n - 1 ≤ j ∧ HasStride p g' j

Addition

theorem MisereGames.GameForm.hasStride_add {p : Player} {g h : GameForm} {sL_g sL_h sR_g sR_h : ℕ} (h_sL_g : HasStride p g sL_g) (h_sL_h : HasStride p h sL_h) (h_sR_g : HasStride (-p) g sR_g) (h_sR_h : HasStride (-p) h sR_h) : HasStride p (g + h) (sL_g + sL_h)

The stride of a sum is the sum of the strides.

theorem MisereGames.GameForm.hasStride_neg_iff {p : Player} {g : GameForm} {n : ℕ} : HasStride (-p) (-g) n ↔ HasStride p g n

@[simp]

theorem MisereGames.GameForm.hasStride_neg_iff' {p : Player} {g : GameForm} {n : ℕ} : HasStride p (-g) n ↔ HasStride (-p) g n

Integers

theorem MisereGames.GameForm.hasStride_zero (p : Player) : HasStride p 0 0

@[simp]

theorem MisereGames.GameForm.hasStride_zero_iff {p : Player} {n : ℕ} : HasStride p 0 n ↔ n = 0

theorem MisereGames.GameForm.hasStride_right_natCast (n : ℕ) : HasStride Player.right (↑n) 0

@[simp]

theorem MisereGames.GameForm.hasStride_right_natCast_iff (n : ℕ) {k : ℕ} : HasStride Player.right (↑n) k ↔ k = 0

theorem MisereGames.GameForm.hasStride_right_one : HasStride Player.right 1 0

@[simp]

theorem MisereGames.GameForm.hasStride_right_one_iff {n : ℕ} : HasStride Player.right 1 n ↔ n = 0

theorem MisereGames.GameForm.hasStride_left_one : HasStride Player.left 1 1

theorem MisereGames.GameForm.hasStride_left_natCast (n : ℕ) : HasStride Player.left (↑n) n

@[simp]

theorem MisereGames.GameForm.hasStride_left_natCast_iff (n : ℕ) {k : ℕ} : HasStride Player.left (↑n) k ↔ k = n

theorem MisereGames.GameForm.hasStride_left_intCast (n : ℤ) : HasStride Player.left (↑n) n.toNat

@[simp]

theorem MisereGames.GameForm.hasStride_left_intCast_iff (n : ℤ) {k : ℕ} : HasStride Player.left (↑n) k ↔ k = n.toNat

@[simp]

theorem MisereGames.GameForm.hasStride_right_intCast_iff (n : ℤ) {k : ℕ} : HasStride Player.right (↑n) k ↔ k = (-n).toNat

Outcomes

theorem MisereGames.GameForm.hasStride_winsGoingFirst_iff {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.WinsGoingFirst p g ↔ l ≤ r

If a game has both strides, then they determine who wins going first.

theorem MisereGames.GameForm.hasStride_misereOutcome_iff_lt {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p ↔ l < r

If a game has both strides, then they determine the outcome.

theorem MisereGames.GameForm.hasStride_misereOutcome_iff_ge {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer (-p) ↔ l > r

theorem MisereGames.GameForm.hasStride_misereOutcome_iff_eq {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.N ↔ l = r

If a game has both strides, then they determine the outcome.

theorem MisereGames.GameForm.hasStride_isPFree {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : IsPFree g

If a game has both strides, then it is $\mathscr{P}$-free.

class MisereGames.GameForm.Strided (A : GameForm → Prop) : Prop

A predicate containing games with prescribed Left and Right strides.

• mk_with_strides (l r : ℕ) : ∃ (g : GameForm), A g ∧ HasStride Player.left g l ∧ HasStride Player.right g r
• has_stride (p : Player) {g : GameForm} (h_g : A g) : ∃ (n : ℕ), HasStride p g n

theorem MisereGames.GameForm.ClosedUnderAdd.closure_has_stride_aux {R : Type u} [Ruleset R] (p : Player) {g : GameForm} (stride : R → Player → ℕ) (hasStride : ∀ (r : R) (p : Player), HasStride p (Ruleset.toGameForm r) (stride r p)) (h_g : Form.ClosedUnderAdd.closure (Ruleset.Forms R) g) : ∃ (n : ℕ), HasStride p g n

theorem MisereGames.GameForm.ClosedUnderAdd.closure_mk_with_strides_aux {A : GameForm → Prop} (mk_stride_other_zero : ∀ (p : Player) (n : ℕ), ∃ (g : GameForm), A g ∧ HasStride p g n ∧ HasStride (-p) g 0) (l r : ℕ) : ∃ (t : GameForm), Form.ClosedUnderAdd.closure A t ∧ HasStride Player.left t l ∧ HasStride Player.right t r

instance MisereGames.GameForm.instStridedClosure {A : GameForm → Prop} [Strided A] : Strided (Form.ClosedUnderAdd.closure A)

theorem MisereGames.GameForm.stride_diff_eq_of_misereEQ {A : GameForm → Prop} [Strided A] {g h : GameForm} (h_eq : g =m A h) {sL_g sR_g sL_h sR_h : ℕ} (h_ng : HasStride Player.left g sL_g) (h_rg : HasStride Player.right g sR_g) (h_nh : HasStride Player.left h sL_h) (h_rh : HasStride Player.right h sR_h) : ↑sL_g - ↑sR_g = ↑sL_h - ↑sR_h

theorem MisereGames.GameForm.misereEQ_of_stride_diff_eq {A : GameForm → Prop} [Strided A] {g h : GameForm} {sL_g sR_g sL_h sR_h : ℕ} (h_ng : HasStride Player.left g sL_g) (h_rg : HasStride Player.right g sR_g) (h_nh : HasStride Player.left h sL_h) (h_rh : HasStride Player.right h sR_h) (h_diff : ↑sL_g - ↑sR_g = ↑sL_h - ↑sR_h) : g =m A h

theorem MisereGames.GameForm.misereEQ_iff_stride_diff_eq {A : GameForm → Prop} [Strided A] {g h : GameForm} {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : g =m A h ↔ ↑ng - ↑rg = ↑nh - ↑rh

The stride difference characterises misère equivalence for strided games.

theorem MisereGames.GameForm.misereGE_of_stride_diff_le {A : GameForm → Prop} [Strided A] {g h : GameForm} {sL_g sR_g sL_h sR_h : ℕ} (h_sL_g : HasStride Player.left g sL_g) (h_sR_g : HasStride Player.right g sR_g) (h_sL_h : HasStride Player.left h sL_h) (h_sR_h : HasStride Player.right h sR_h) (h_le : ↑sL_g - ↑sR_g ≤ ↑sL_h - ↑sR_h) : g ≥m A h

theorem MisereGames.GameForm.misereQuotient_linearOrder {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ∨ b ≤ a

The misère quotient of a strided class is totally ordered. This follows from the fact that the ordering is determined by stride differences.

noncomputable def MisereGames.GameForm.Strided.strideDiff {A : GameForm → Prop} [Strided A] (g : GameForm) (hg : A g) : ℤ

The stride difference of a game in a strided class A. This is the left stride minus the right stride, as an integer.

Equations

• MisereGames.GameForm.Strided.strideDiff g hg = ↑⋯.choose - ↑⋯.choose

theorem MisereGames.GameForm.strideDiff_eq {A : GameForm → Prop} [Strided A] {g : GameForm} {hg : A g} {l r : ℕ} (hl : HasStride Player.left g l) (hr : HasStride Player.right g r) : Strided.strideDiff g hg = ↑l - ↑r

The stride difference is well-defined regardless of which stride witnesses are used.

theorem MisereGames.GameForm.Strided.strideDiff_eq_of_misereEQ {A : GameForm → Prop} [Strided A] {g h : GameForm} (hg : A g) (hh : A h) (heq : g =m A h) : strideDiff g hg = strideDiff h hh

Misère equivalent games have the same stride difference.

noncomputable def MisereGames.GameForm.MisereQuotient.strideDiff {A : GameForm → Prop} [Strided A] : MisereQuotient A → ℤ

The stride difference function on the misère quotient, defined via representative. This is well-defined because misère equivalent games have the same stride difference.

Equations

• MisereGames.GameForm.MisereQuotient.strideDiff = Quotient.lift (fun (g : { g : MisereGames.GameForm // A g }) => MisereGames.GameForm.Strided.strideDiff ↑g ⋯) ⋯

theorem MisereGames.GameForm.MisereQuotient.strideDiff_mk {A : GameForm → Prop} [Strided A] (g : GameForm) (hg : A g) : strideDiff (Form.MisereQuotient.mk ⟨g, hg⟩) = Strided.strideDiff g hg

theorem MisereGames.GameForm.MisereQuotient.strideDiff_injective {A : GameForm → Prop} [Strided A] : Function.Injective strideDiff

The stride difference function on the quotient is injective.

theorem MisereGames.GameForm.MisereQuotient.strideDiff_surjective {A : GameForm → Prop} [Strided A] : Function.Surjective strideDiff

The stride difference function on the quotient is surjective: for any integer d, there is a game in A with stride difference d.

noncomputable def MisereGames.GameForm.MisereQuotient.stridedEquivInt {A : GameForm → Prop} [Strided A] : MisereQuotient A ≃ ℤ

The misère quotient of a strided class is equivalent to the integers. The equivalence sends each equivalence class to its stride difference.

Equations

• MisereGames.GameForm.MisereQuotient.stridedEquivInt = Equiv.ofBijective MisereGames.GameForm.MisereQuotient.strideDiff ⋯

theorem MisereGames.GameForm.stride_diff_le_of_misereGE {A : GameForm → Prop} [Strided A] {g h : GameForm} (h_ge : g ≥m A h) {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : ↑ng - ↑rg ≤ ↑nh - ↑rh

If g ≥m A h then the stride difference of g is ≤ that of h. The converse of misereGE_of_stride_diff_le.

theorem MisereGames.GameForm.misereGE_iff_stride_diff_le {A : GameForm → Prop} [Strided A] {g h : GameForm} {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : g ≥m A h ↔ ↑ng - ↑rg ≤ ↑nh - ↑rh

Misère GE is equivalent to stride difference inequality.

theorem MisereGames.GameForm.MisereQuotient.mk_le_iff_strideDiff {A : GameForm → Prop} [Strided A] (g h : GameForm) (hg : A g) (hh : A h) : Form.MisereQuotient.mk ⟨g, hg⟩ ≤ Form.MisereQuotient.mk ⟨h, hh⟩ ↔ Strided.strideDiff g hg ≥ Strided.strideDiff h hh

The ordering on the misère quotient corresponds to ≥ on stride differences: mk A g hg ≤ mk A h hh iff strideDiff A g hg ≥ strideDiff A h hh.

theorem MisereGames.GameForm.MisereQuotient.le_iff_strideDiff_ge {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ↔ strideDiff a ≥ strideDiff b

theorem MisereGames.GameForm.MisereQuotient.le_iff_equiv_ge {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ↔ stridedEquivInt a ≥ stridedEquivInt b

The misère quotient ordering via the integer equivalence: a ≤ b iff the image of a under the equivalence is ≥ the image of b. Equivalently, the equivalence is an order-reversing bijection.