Basic definitions about impartial (pre-)games

We will define an impartial game, one in which left and right can make exactly the same moves. Our definition differs slightly by saying that the game is always equivalent to its negative, no matter what moves are played. This allows for games such as poker-nim to be classified as impartial.

def SetTheory.PGame.ImpartialAux : SetTheory.PGame → Prop

The definition for an impartial game, defined using Conway induction.

Equations

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

theorem SetTheory.PGame.impartialAux_def {G : SetTheory.PGame} : SetTheory.PGame.ImpartialAux G ↔ G ≈ -G ∧ (∀ (i : SetTheory.PGame.LeftMoves G), SetTheory.PGame.ImpartialAux (SetTheory.PGame.moveLeft G i)) ∧ ∀ (j : SetTheory.PGame.RightMoves G), SetTheory.PGame.ImpartialAux (SetTheory.PGame.moveRight G j)

class SetTheory.PGame.Impartial (G : SetTheory.PGame) : Prop

A typeclass on impartial games.

• out : SetTheory.PGame.ImpartialAux G

theorem SetTheory.PGame.impartial_iff_aux {G : SetTheory.PGame} : SetTheory.PGame.Impartial G ↔ SetTheory.PGame.ImpartialAux G

theorem SetTheory.PGame.impartial_def {G : SetTheory.PGame} : SetTheory.PGame.Impartial G ↔ G ≈ -G ∧ (∀ (i : SetTheory.PGame.LeftMoves G), SetTheory.PGame.Impartial (SetTheory.PGame.moveLeft G i)) ∧ ∀ (j : SetTheory.PGame.RightMoves G), SetTheory.PGame.Impartial (SetTheory.PGame.moveRight G j)

instance SetTheory.PGame.Impartial.impartial_zero : SetTheory.PGame.Impartial 0

Equations

• SetTheory.PGame.Impartial.impartial_zero = ⋯

instance SetTheory.PGame.Impartial.impartial_star : SetTheory.PGame.Impartial SetTheory.PGame.star

Equations

• SetTheory.PGame.Impartial.impartial_star = ⋯

theorem SetTheory.PGame.Impartial.neg_equiv_self (G : SetTheory.PGame) [h : SetTheory.PGame.Impartial G] : G ≈ -G

@[simp]

theorem SetTheory.PGame.Impartial.mk'_neg_equiv_self (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : -⟦G⟧ = ⟦G⟧

instance SetTheory.PGame.Impartial.moveLeft_impartial {G : SetTheory.PGame} [h : SetTheory.PGame.Impartial G] (i : SetTheory.PGame.LeftMoves G) : SetTheory.PGame.Impartial (SetTheory.PGame.moveLeft G i)

Equations

• ⋯ = ⋯

instance SetTheory.PGame.Impartial.moveRight_impartial {G : SetTheory.PGame} [h : SetTheory.PGame.Impartial G] (j : SetTheory.PGame.RightMoves G) : SetTheory.PGame.Impartial (SetTheory.PGame.moveRight G j)

Equations

• ⋯ = ⋯

theorem SetTheory.PGame.Impartial.impartial_congr {G : SetTheory.PGame} {H : SetTheory.PGame} : SetTheory.PGame.Relabelling G H → ∀ [inst : SetTheory.PGame.Impartial G], SetTheory.PGame.Impartial H

instance SetTheory.PGame.Impartial.impartial_add (G : SetTheory.PGame) (H : SetTheory.PGame) [SetTheory.PGame.Impartial G] [SetTheory.PGame.Impartial H] : SetTheory.PGame.Impartial (G + H)

Equations

• ⋯ = ⋯

instance SetTheory.PGame.Impartial.impartial_neg (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.Impartial (-G)

Equations

• ⋯ = ⋯

theorem SetTheory.PGame.Impartial.nonpos (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : ¬0 < G

theorem SetTheory.PGame.Impartial.nonneg (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : ¬G < 0

theorem SetTheory.PGame.Impartial.equiv_or_fuzzy_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : G ≈ 0 ∨ SetTheory.PGame.Fuzzy G 0

In an impartial game, either the first player always wins, or the second player always wins.

@[simp]

theorem SetTheory.PGame.Impartial.not_equiv_zero_iff (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : ¬G ≈ 0 ↔ SetTheory.PGame.Fuzzy G 0

@[simp]

theorem SetTheory.PGame.Impartial.not_fuzzy_zero_iff (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : ¬SetTheory.PGame.Fuzzy G 0 ↔ G ≈ 0

theorem SetTheory.PGame.Impartial.add_self (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : G + G ≈ 0

@[simp]

theorem SetTheory.PGame.Impartial.mk'_add_self (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : ⟦G⟧ + ⟦G⟧ = 0

theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] (H : SetTheory.PGame) : H ≈ G ↔ H + G ≈ 0

This lemma doesn't require H to be impartial.

theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero' (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] (H : SetTheory.PGame) : G ≈ H ↔ G + H ≈ 0

This lemma doesn't require H to be impartial.

theorem SetTheory.PGame.Impartial.le_zero_iff {G : SetTheory.PGame} [SetTheory.PGame.Impartial G] : G ≤ 0 ↔ 0 ≤ G

theorem SetTheory.PGame.Impartial.lf_zero_iff {G : SetTheory.PGame} [SetTheory.PGame.Impartial G] : SetTheory.PGame.LF G 0 ↔ SetTheory.PGame.LF 0 G

theorem SetTheory.PGame.Impartial.equiv_zero_iff_le (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : G ≈ 0 ↔ G ≤ 0

theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_lf (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.Fuzzy G 0 ↔ SetTheory.PGame.LF G 0

theorem SetTheory.PGame.Impartial.equiv_zero_iff_ge (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : G ≈ 0 ↔ 0 ≤ G

theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_gf (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.Fuzzy G 0 ↔ SetTheory.PGame.LF 0 G

theorem SetTheory.PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : (∀ (i : SetTheory.PGame.LeftMoves G), SetTheory.PGame.Fuzzy (SetTheory.PGame.moveLeft G i) 0) ↔ G ≈ 0

theorem SetTheory.PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : (∀ (j : SetTheory.PGame.RightMoves G), SetTheory.PGame.Fuzzy (SetTheory.PGame.moveRight G j) 0) ↔ G ≈ 0

theorem SetTheory.PGame.Impartial.exists_left_move_equiv_iff_fuzzy_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : (∃ (i : SetTheory.PGame.LeftMoves G), SetTheory.PGame.moveLeft G i ≈ 0) ↔ SetTheory.PGame.Fuzzy G 0

theorem SetTheory.PGame.Impartial.exists_right_move_equiv_iff_fuzzy_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : (∃ (j : SetTheory.PGame.RightMoves G), SetTheory.PGame.moveRight G j ≈ 0) ↔ SetTheory.PGame.Fuzzy G 0