mathlib documentation

set_theory.game.pgame

Combinatorial (pre-)games. #

The basic theory of combinatorial games, following Conway's book On Numbers and Games. We construct "pregames", define an ordering and arithmetic operations on them, then show that the operations descend to "games", defined via the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p.

The surreal numbers will be built as a quotient of a subtype of pregames.

A pregame (pgame below) is axiomatised via an inductive type, whose sole constructor takes two types (thought of as indexing the possible moves for the players Left and Right), and a pair of functions out of these types to pgame (thought of as describing the resulting game after making a move).

Combinatorial games themselves, as a quotient of pregames, are constructed in game.lean.

Conway induction #

By construction, the induction principle for pregames is exactly "Conway induction". That is, to prove some predicate pgame → Prop holds for all pregames, it suffices to prove that for every pregame g, if the predicate holds for every game resulting from making a move, then it also holds for g.

While it is often convenient to work "by induction" on pregames, in some situations this becomes awkward, so we also define accessor functions pgame.left_moves, pgame.right_moves, pgame.move_left and pgame.move_right. There is a relation pgame.subsequent p q, saying that p can be reached by playing some non-empty sequence of moves starting from q, an instance well_founded subsequent, and a local tactic pgame_wf_tac which is helpful for discharging proof obligations in inductive proofs relying on this relation.

Order properties #

Pregames have both a and a < relation, satisfying the usual properties of a preorder. The relation 0 < x means that x can always be won by Left, while 0 ≤ x means that x can be won by Left as the second player.

It turns out to be quite convenient to define various relations on top of these. We define the "less or fuzzy" relation x ⧏ y as ¬ y ≤ x, the equivalence relation x ≈ y as x ≤ y ∧ y ≤ x, and the fuzzy relation x ∥ y as x ⧏ y ∧ y ⧏ x. If 0 ⧏ x, then x can be won by Left as the first player. If x ≈ 0, then x can be won by the second player. If x ∥ 0, then x can be won by the first player.

Statements like zero_le_lf, zero_lf_le, etc. unfold these definitions. The theorems le_def and lf_def give a recursive characterisation of each relation in terms of themselves two moves later. The theorems zero_le, zero_lf, etc. also take into account that 0 has no moves.

Later, games will be defined as the quotient by the relation; that is to say, the antisymmetrization of pgame.

Algebraic structures #

We next turn to defining the operations necessary to make games into a commutative additive group. Addition is defined for $x = \{xL | xR\}$ and $y = \{yL | yR\}$ by $x + y = \{xL + y, x + yL | xR + y, x + yR\}$. Negation is defined by $\{xL | xR\} = \{-xR | -xL\}$.

The order structures interact in the expected way with addition, so we have

theorem le_iff_sub_nonneg {x y : pgame} : x  y  0  y - x := sorry
theorem lt_iff_sub_pos {x y : pgame} : x < y  0 < y - x := sorry

We show that these operations respect the equivalence relation, and hence descend to games. At the level of games, these operations satisfy all the laws of a commutative group. To prove the necessary equivalence relations at the level of pregames, we introduce the notion of a relabelling of a game, and show, for example, that there is a relabelling between x + (y + z) and (x + y) + z.

Future work #

References #

The material here is all drawn from

An interested reader may like to formalise some of the material from

Pre-game moves #

inductive pgame  :
Type (u+1)

The type of pre-games, before we have quotiented by equivalence (pgame.setoid). In ZFC, a combinatorial game is constructed from two sets of combinatorial games that have been constructed at an earlier stage. To do this in type theory, we say that a pre-game is built inductively from two families of pre-games indexed over any type in Type u. The resulting type pgame.{u} lives in Type (u+1), reflecting that it is a proper class in ZFC.

Instances for pgame
def pgame.move_left (g : pgame) :

The new game after Left makes an allowed move.

Equations
Instances for pgame.move_left

The new game after Right makes an allowed move.

Equations
Instances for pgame.move_right
@[simp]
theorem pgame.left_moves_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).left_moves = xl
@[simp]
theorem pgame.move_left_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).move_left = xL
@[simp]
theorem pgame.right_moves_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).right_moves = xr
@[simp]
theorem pgame.move_right_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).move_right = xR
def pgame.of_lists (L R : list pgame) :

Construct a pre-game from list of pre-games describing the available moves for Left and Right.

Equations
Instances for pgame.of_lists

Converts a number into a left move for of_lists.

Equations

Converts a number into a right move for of_lists.

Equations
def pgame.move_rec_on {C : pgameSort u_2} (x : pgame) (IH : Π (y : pgame), (Π (i : y.left_moves), C (y.move_left i))(Π (j : y.right_moves), C (y.move_right j))C y) :
C x

A variant of pgame.rec_on expressed in terms of pgame.move_left and pgame.move_right.

Both this and pgame.rec_on describe Conway induction on games.

Equations
inductive pgame.is_option  :
pgamepgame → Prop

is_option x y means that x is either a left or right option for y.

theorem pgame.is_option_iff (ᾰ ᾰ_1 : pgame) :
ᾰ.is_option ᾰ_1 (∃ (i : ᾰ_1.left_moves), = ᾰ_1.move_left i) ∃ (i : ᾰ_1.right_moves), = ᾰ_1.move_right i
theorem pgame.is_option.mk_left {xl xr : Type u} (xL : xl → pgame) (xR : xr → pgame) (i : xl) :
(xL i).is_option (pgame.mk xl xr xL xR)
theorem pgame.is_option.mk_right {xl xr : Type u} (xL : xl → pgame) (xR : xr → pgame) (i : xr) :
(xR i).is_option (pgame.mk xl xr xL xR)
def pgame.subsequent  :
pgamepgame → Prop

subsequent x y says that x can be obtained by playing some nonempty sequence of moves from y. It is the transitive closure of is_option.

Equations
Instances for pgame.subsequent
@[trans]
theorem pgame.subsequent.trans {x y z : pgame} :
x.subsequent yy.subsequent zx.subsequent z
theorem pgame.subsequent.mk_left {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) (i : xl) :
(xL i).subsequent (pgame.mk xl xr xL xR)
theorem pgame.subsequent.mk_right {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) (j : xr) :
(xR j).subsequent (pgame.mk xl xr xL xR)

A local tactic for proving well-foundedness of recursive definitions involving pregames.

Basic pre-games #

@[protected, instance]

The pre-game zero is defined by 0 = { | }.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]

The pre-game one is defined by 1 = { 0 | }.

Equations
@[simp]
@[simp]
theorem pgame.one_move_left (x : 1.left_moves) :
1.move_left x = 0
@[protected, instance]

Pre-game order relations #

def pgame.le_lf (x y : pgame) :
Prop × Prop

Define simultaneously by mutual induction the relation and its swapped converse on pre-games.

The ZFC definition says that x = {xL | xR} is less or equal to y = {yL | yR} if ∀ x₁ ∈ xL, x₁ ⧏ y and ∀ y₂ ∈ yR, x ⧏ y₂, where x ⧏ y means ¬ y ≤ x. This is a tricky induction because it only decreases one side at a time, and it also swaps the arguments in the definition of . The solution is to define x ≤ y and x ⧏ y simultaneously.

Equations
@[protected, instance]

The less or equal relation on pre-games.

If 0 ≤ x, then Left can win x as the second player.

Equations
def pgame.lf (x y : pgame) :
Prop

The less or fuzzy relation on pre-games.

If 0 ⧏ x, then Left can win x as the first player.

Equations
Instances for pgame.lf
@[simp]
theorem pgame.mk_le_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} :
pgame.mk xl xr xL xR pgame.mk yl yr yL yR (∀ (i : xl), (xL i).lf (pgame.mk yl yr yL yR)) ∀ (j : yr), (pgame.mk xl xr xL xR).lf (yR j)

Definition of x ≤ y on pre-games built using the constructor.

theorem pgame.le_iff_forall_lf {x y : pgame} :
x y (∀ (i : x.left_moves), (x.move_left i).lf y) ∀ (j : y.right_moves), x.lf (y.move_right j)

Definition of x ≤ y on pre-games, in terms of

theorem pgame.le_of_forall_lf {x y : pgame} (h₁ : ∀ (i : x.left_moves), (x.move_left i).lf y) (h₂ : ∀ (j : y.right_moves), x.lf (y.move_right j)) :
x y
@[simp]
theorem pgame.mk_lf_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} :
(pgame.mk xl xr xL xR).lf (pgame.mk yl yr yL yR) (∃ (i : yl), pgame.mk xl xr xL xR yL i) ∃ (j : xr), xR j pgame.mk yl yr yL yR

Definition of x ⧏ y on pre-games built using the constructor.

theorem pgame.lf_iff_exists_le {x y : pgame} :
x.lf y (∃ (i : y.left_moves), x y.move_left i) ∃ (j : x.right_moves), x.move_right j y

Definition of x ⧏ y on pre-games, in terms of

@[protected, simp]
theorem pgame.not_le {x y : pgame} :
¬x y y.lf x
@[simp]
theorem pgame.not_lf {x y : pgame} :
¬x.lf y y x
theorem has_le.le.not_gf {x y : pgame} :
x y¬y.lf x
theorem pgame.lf.not_ge {x y : pgame} :
x.lf y¬y x
theorem pgame.le_or_gf (x y : pgame) :
x y y.lf x
theorem pgame.move_left_lf_of_le {x y : pgame} (h : x y) (i : x.left_moves) :
(x.move_left i).lf y
theorem has_le.le.move_left_lf {x y : pgame} (h : x y) (i : x.left_moves) :
(x.move_left i).lf y

Alias of pgame.move_left_lf_of_le.

theorem pgame.lf_move_right_of_le {x y : pgame} (h : x y) (j : y.right_moves) :
x.lf (y.move_right j)
theorem has_le.le.lf_move_right {x y : pgame} (h : x y) (j : y.right_moves) :
x.lf (y.move_right j)

Alias of pgame.lf_move_right_of_le.

theorem pgame.lf_of_move_right_le {x y : pgame} {j : x.right_moves} (h : x.move_right j y) :
x.lf y
theorem pgame.lf_of_le_move_left {x y : pgame} {i : y.left_moves} (h : x y.move_left i) :
x.lf y
theorem pgame.lf_of_le_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {y : pgame} :
pgame.mk xl xr xL xR y∀ (i : xl), (xL i).lf y
theorem pgame.lf_of_mk_le {x : pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} :
x pgame.mk yl yr yL yR∀ (j : yr), x.lf (yR j)
theorem pgame.mk_lf_of_le {xl xr : Type u_1} {y : pgame} {j : xr} (xL : xl → pgame) {xR : xr → pgame} :
xR j y(pgame.mk xl xr xL xR).lf y
theorem pgame.lf_mk_of_le {x : pgame} {yl yr : Type u_1} {yL : yl → pgame} (yR : yr → pgame) {i : yl} :
x yL ix.lf (pgame.mk yl yr yL yR)
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem pgame.lt_iff_le_and_lf {x y : pgame} :
x < y x y x.lf y
theorem pgame.lt_of_le_of_lf {x y : pgame} (h₁ : x y) (h₂ : x.lf y) :
x < y
theorem pgame.lf_of_lt {x y : pgame} (h : x < y) :
x.lf y
theorem has_lt.lt.lf {x y : pgame} (h : x < y) :
x.lf y

Alias of pgame.lf_of_lt.

theorem pgame.lf_irrefl (x : pgame) :
¬x.lf x
@[protected, instance]
@[trans]
theorem pgame.lf_of_le_of_lf {x y z : pgame} (h₁ : x y) (h₂ : y.lf z) :
x.lf z
@[trans]
theorem pgame.lf_of_lf_of_le {x y z : pgame} (h₁ : x.lf y) (h₂ : y z) :
x.lf z
theorem has_le.le.trans_lf {x y z : pgame} (h₁ : x y) (h₂ : y.lf z) :
x.lf z

Alias of pgame.lf_of_le_of_lf.

theorem pgame.lf.trans_le {x y z : pgame} (h₁ : x.lf y) (h₂ : y z) :
x.lf z

Alias of pgame.lf_of_lf_of_le.

@[trans]
theorem pgame.lf_of_lt_of_lf {x y z : pgame} (h₁ : x < y) (h₂ : y.lf z) :
x.lf z
@[trans]
theorem pgame.lf_of_lf_of_lt {x y z : pgame} (h₁ : x.lf y) (h₂ : y < z) :
x.lf z
theorem has_lt.lt.trans_lf {x y z : pgame} (h₁ : x < y) (h₂ : y.lf z) :
x.lf z

Alias of pgame.lf_of_lt_of_lf.

theorem pgame.lf.trans_lt {x y z : pgame} (h₁ : x.lf y) (h₂ : y < z) :
x.lf z

Alias of pgame.lf_of_lf_of_lt.

theorem pgame.move_left_lf {x : pgame} (i : x.left_moves) :
(x.move_left i).lf x
theorem pgame.lf_move_right {x : pgame} (j : x.right_moves) :
x.lf (x.move_right j)
theorem pgame.lf_mk {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) (i : xl) :
(xL i).lf (pgame.mk xl xr xL xR)
theorem pgame.mk_lf {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) (j : xr) :
(pgame.mk xl xr xL xR).lf (xR j)
theorem pgame.le_of_forall_lt {x y : pgame} (h₁ : ∀ (i : x.left_moves), x.move_left i < y) (h₂ : ∀ (j : y.right_moves), x < y.move_right j) :
x y

This special case of pgame.le_of_forall_lf is useful when dealing with surreals, where < is preferred over .

theorem pgame.le_def {x y : pgame} :
x y (∀ (i : x.left_moves), (∃ (i' : y.left_moves), x.move_left i y.move_left i') ∃ (j : (x.move_left i).right_moves), (x.move_left i).move_right j y) ∀ (j : y.right_moves), (∃ (i : (y.move_right j).left_moves), x (y.move_right j).move_left i) ∃ (j' : x.right_moves), x.move_right j' y.move_right j

The definition of x ≤ y on pre-games, in terms of two moves later.

theorem pgame.lf_def {x y : pgame} :
x.lf y (∃ (i : y.left_moves), (∀ (i' : x.left_moves), (x.move_left i').lf (y.move_left i)) ∀ (j : (y.move_left i).right_moves), x.lf ((y.move_left i).move_right j)) ∃ (j : x.right_moves), (∀ (i : (x.move_right j).left_moves), ((x.move_right j).move_left i).lf y) ∀ (j' : y.right_moves), (x.move_right j).lf (y.move_right j')

The definition of x ⧏ y on pre-games, in terms of two moves later.

theorem pgame.zero_le_lf {x : pgame} :
0 x ∀ (j : x.right_moves), 0.lf (x.move_right j)

The definition of 0 ≤ x on pre-games, in terms of 0 ⧏.

theorem pgame.le_zero_lf {x : pgame} :
x 0 ∀ (i : x.left_moves), (x.move_left i).lf 0

The definition of x ≤ 0 on pre-games, in terms of ⧏ 0.

theorem pgame.zero_lf_le {x : pgame} :
0.lf x ∃ (i : x.left_moves), 0 x.move_left i

The definition of 0 ⧏ x on pre-games, in terms of 0 ≤.

theorem pgame.lf_zero_le {x : pgame} :
x.lf 0 ∃ (j : x.right_moves), x.move_right j 0

The definition of x ⧏ 0 on pre-games, in terms of ≤ 0.

theorem pgame.zero_le {x : pgame} :
0 x ∀ (j : x.right_moves), ∃ (i : (x.move_right j).left_moves), 0 (x.move_right j).move_left i

The definition of 0 ≤ x on pre-games, in terms of 0 ≤ two moves later.

theorem pgame.le_zero {x : pgame} :
x 0 ∀ (i : x.left_moves), ∃ (j : (x.move_left i).right_moves), (x.move_left i).move_right j 0

The definition of x ≤ 0 on pre-games, in terms of ≤ 0 two moves later.

theorem pgame.zero_lf {x : pgame} :
0.lf x ∃ (i : x.left_moves), ∀ (j : (x.move_left i).right_moves), 0.lf ((x.move_left i).move_right j)

The definition of 0 ⧏ x on pre-games, in terms of 0 ⧏ two moves later.

theorem pgame.lf_zero {x : pgame} :
x.lf 0 ∃ (j : x.right_moves), ∀ (i : (x.move_right j).left_moves), ((x.move_right j).move_left i).lf 0

The definition of x ⧏ 0 on pre-games, in terms of ⧏ 0 two moves later.

noncomputable def pgame.right_response {x : pgame} (h : x 0) (i : x.left_moves) :

Given a game won by the right player when they play second, provide a response to any move by left.

Equations
theorem pgame.right_response_spec {x : pgame} (h : x 0) (i : x.left_moves) :

Show that the response for right provided by right_response preserves the right-player-wins condition.

noncomputable def pgame.left_response {x : pgame} (h : 0 x) (j : x.right_moves) :

Given a game won by the left player when they play second, provide a response to any move by right.

Equations
theorem pgame.left_response_spec {x : pgame} (h : 0 x) (j : x.right_moves) :

Show that the response for left provided by left_response preserves the left-player-wins condition.

def pgame.equiv (x y : pgame) :
Prop

The equivalence relation on pre-games. Two pre-games x, y are equivalent if x ≤ y and y ≤ x.

If x ≈ 0, then the second player can always win x.

Equations
Instances for pgame.equiv
@[protected, instance]
theorem pgame.equiv.le {x y : pgame} (h : x.equiv y) :
x y
theorem pgame.equiv.ge {x y : pgame} (h : x.equiv y) :
y x
@[simp, refl]
theorem pgame.equiv_rfl {x : pgame} :
x.equiv x
theorem pgame.equiv_refl (x : pgame) :
x.equiv x
@[protected, symm]
theorem pgame.equiv.symm {x y : pgame} :
x.equiv yy.equiv x
@[protected, trans]
theorem pgame.equiv.trans {x y z : pgame} :
x.equiv yy.equiv zx.equiv z
@[protected]
theorem pgame.equiv_comm {x y : pgame} :
x.equiv y y.equiv x
theorem pgame.equiv_of_eq {x y : pgame} (h : x = y) :
x.equiv y
@[trans]
theorem pgame.le_of_le_of_equiv {x y z : pgame} (h₁ : x y) (h₂ : y.equiv z) :
x z
@[trans]
theorem pgame.le_of_equiv_of_le {x y z : pgame} (h₁ : x.equiv y) :
y zx z
theorem pgame.lf.not_equiv {x y : pgame} (h : x.lf y) :
theorem pgame.lf.not_equiv' {x y : pgame} (h : x.lf y) :
theorem pgame.lf.not_gt {x y : pgame} (h : x.lf y) :
¬y < x
theorem pgame.le_congr_imp {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) (h : x₁ y₁) :
x₂ y₂
theorem pgame.le_congr {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁ y₁ x₂ y₂
theorem pgame.le_congr_left {x₁ x₂ y : pgame} (hx : x₁.equiv x₂) :
x₁ y x₂ y
theorem pgame.le_congr_right {x y₁ y₂ : pgame} (hy : y₁.equiv y₂) :
x y₁ x y₂
theorem pgame.lf_congr {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁.lf y₁ x₂.lf y₂
theorem pgame.lf_congr_imp {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁.lf y₁x₂.lf y₂
theorem pgame.lf_congr_left {x₁ x₂ y : pgame} (hx : x₁.equiv x₂) :
x₁.lf y x₂.lf y
theorem pgame.lf_congr_right {x y₁ y₂ : pgame} (hy : y₁.equiv y₂) :
x.lf y₁ x.lf y₂
@[trans]
theorem pgame.lf_of_lf_of_equiv {x y z : pgame} (h₁ : x.lf y) (h₂ : y.equiv z) :
x.lf z
@[trans]
theorem pgame.lf_of_equiv_of_lf {x y z : pgame} (h₁ : x.equiv y) :
y.lf zx.lf z
@[trans]
theorem pgame.lt_of_lt_of_equiv {x y z : pgame} (h₁ : x < y) (h₂ : y.equiv z) :
x < z
@[trans]
theorem pgame.lt_of_equiv_of_lt {x y z : pgame} (h₁ : x.equiv y) :
y < zx < z
theorem pgame.lt_congr_imp {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) (h : x₁ < y₁) :
x₂ < y₂
theorem pgame.lt_congr {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁ < y₁ x₂ < y₂
theorem pgame.lt_congr_left {x₁ x₂ y : pgame} (hx : x₁.equiv x₂) :
x₁ < y x₂ < y
theorem pgame.lt_congr_right {x y₁ y₂ : pgame} (hy : y₁.equiv y₂) :
x < y₁ x < y₂
theorem pgame.lt_or_equiv_of_le {x y : pgame} (h : x y) :
x < y x.equiv y
theorem pgame.lf_or_equiv_or_gf (x y : pgame) :
x.lf y x.equiv y y.lf x
theorem pgame.equiv_congr_left {y₁ y₂ : pgame} :
y₁.equiv y₂ ∀ (x₁ : pgame), x₁.equiv y₁ x₁.equiv y₂
theorem pgame.equiv_congr_right {x₁ x₂ : pgame} :
x₁.equiv x₂ ∀ (y₁ : pgame), x₁.equiv y₁ x₂.equiv y₁
theorem pgame.equiv_of_mk_equiv {x y : pgame} (L : x.left_moves y.left_moves) (R : x.right_moves y.right_moves) (hl : ∀ (i : x.left_moves), (x.move_left i).equiv (y.move_left (L i))) (hr : ∀ (j : x.right_moves), (x.move_right j).equiv (y.move_right (R j))) :
x.equiv y
def pgame.fuzzy (x y : pgame) :
Prop

The fuzzy, confused, or incomparable relation on pre-games.

If x ∥ 0, then the first player can always win x.

Equations
Instances for pgame.fuzzy
@[symm]
theorem pgame.fuzzy.swap {x y : pgame} :
x.fuzzy yy.fuzzy x
@[protected, instance]
theorem pgame.fuzzy.swap_iff {x y : pgame} :
x.fuzzy y y.fuzzy x
theorem pgame.fuzzy_irrefl (x : pgame) :
@[protected, instance]
theorem pgame.lf_iff_lt_or_fuzzy {x y : pgame} :
x.lf y x < y x.fuzzy y
theorem pgame.lf_of_fuzzy {x y : pgame} (h : x.fuzzy y) :
x.lf y
theorem pgame.fuzzy.lf {x y : pgame} (h : x.fuzzy y) :
x.lf y

Alias of pgame.lf_of_fuzzy.

theorem pgame.lt_or_fuzzy_of_lf {x y : pgame} :
x.lf yx < y x.fuzzy y
theorem pgame.fuzzy.not_equiv {x y : pgame} (h : x.fuzzy y) :
theorem pgame.fuzzy.not_equiv' {x y : pgame} (h : x.fuzzy y) :
theorem pgame.not_fuzzy_of_le {x y : pgame} (h : x y) :
theorem pgame.not_fuzzy_of_ge {x y : pgame} (h : y x) :
theorem pgame.equiv.not_fuzzy {x y : pgame} (h : x.equiv y) :
theorem pgame.equiv.not_fuzzy' {x y : pgame} (h : x.equiv y) :
theorem pgame.fuzzy_congr {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁.fuzzy y₁ x₂.fuzzy y₂
theorem pgame.fuzzy_congr_imp {x₁ y₁ x₂ y₂ : pgame} (hx : x₁.equiv x₂) (hy : y₁.equiv y₂) :
x₁.fuzzy y₁x₂.fuzzy y₂
theorem pgame.fuzzy_congr_left {x₁ x₂ y : pgame} (hx : x₁.equiv x₂) :
x₁.fuzzy y x₂.fuzzy y
theorem pgame.fuzzy_congr_right {x y₁ y₂ : pgame} (hy : y₁.equiv y₂) :
x.fuzzy y₁ x.fuzzy y₂
@[trans]
theorem pgame.fuzzy_of_fuzzy_of_equiv {x y z : pgame} (h₁ : x.fuzzy y) (h₂ : y.equiv z) :
x.fuzzy z
@[trans]
theorem pgame.fuzzy_of_equiv_of_fuzzy {x y z : pgame} (h₁ : x.equiv y) (h₂ : y.fuzzy z) :
x.fuzzy z
theorem pgame.lt_or_equiv_or_gt_or_fuzzy (x y : pgame) :
x < y x.equiv y y < x x.fuzzy y

Exactly one of the following is true (although we don't prove this here).

theorem pgame.lt_or_equiv_or_gf (x y : pgame) :
x < y x.equiv y y.lf x

Relabellings #

inductive pgame.restricted  :
pgamepgameType (u+1)

restricted x y says that Left always has no more moves in x than in y, and Right always has no more moves in y than in x

Instances for pgame.restricted
@[refl]

The identity restriction.

Equations
def pgame.restricted.trans {x y z : pgame} (r : x.restricted y) (s : y.restricted z) :

Transitivity of restriction.

Equations
theorem pgame.restricted.le {x y : pgame} (r : x.restricted y) :
x y
inductive pgame.relabelling  :
pgamepgameType (u+1)

relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have relabellings for the consequent games.

Instances for pgame.relabelling
def pgame.relabelling.mk' {x y : pgame} (L : y.left_moves x.left_moves) (R : y.right_moves x.right_moves) (hL : Π (i : y.left_moves), (x.move_left (L i)).relabelling (y.move_left i)) (hR : Π (j : y.right_moves), (x.move_right (R j)).relabelling (y.move_right j)) :

A constructor for relabellings swapping the equivalences.

Equations

The equivalence between left moves of x and y given by the relabelling.

Equations
@[simp]
theorem pgame.relabelling.mk_left_moves_equiv {x y : pgame} {L : x.left_moves y.left_moves} {R : x.right_moves y.right_moves} {hL : Π (i : x.left_moves), (x.move_left i).relabelling (y.move_left (L i))} {hR : Π (j : x.right_moves), (x.move_right j).relabelling (y.move_right (R j))} :
@[simp]

The equivalence between right moves of x and y given by the relabelling.

Equations
@[simp]
@[simp]

A left move of x is a relabelling of a left move of y.

Equations

A left move of y is a relabelling of a left move of x.

Equations

A right move of x is a relabelling of a right move of y.

Equations

A right move of y is a relabelling of a right move of x.

Equations

If x is a relabelling of y, then x is a restriction of y.

Equations

It's not the case that restricted x y → restricted y x → x ≡r y, but if we insisted that the maps in a restriction were injective, then one could use Schröder-Bernstein for do this.

@[symm]

Flip a relabelling.

Equations
theorem pgame.relabelling.le {x y : pgame} (r : x.relabelling y) :
x y
theorem pgame.relabelling.ge {x y : pgame} (r : x.relabelling y) :
y x
theorem pgame.relabelling.equiv {x y : pgame} (r : x.relabelling y) :
x.equiv y

A relabelling lets us prove equivalence of games.

@[trans]
def pgame.relabelling.trans {x y z : pgame} :
x.relabelling yy.relabelling zx.relabelling z

Transitivity of relabelling.

Equations
@[protected, instance]
def pgame.equiv.has_coe {x y : pgame} :
Equations
def pgame.relabel {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) :

Replace the types indexing the next moves for Left and Right by equivalent types.

Equations
@[simp]
theorem pgame.relabel_move_left' {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) (i : xl') :
@[simp]
theorem pgame.relabel_move_left {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) (i : x.left_moves) :
@[simp]
theorem pgame.relabel_move_right' {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) (j : xr') :
@[simp]
theorem pgame.relabel_move_right {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) (j : x.right_moves) :
def pgame.relabel_relabelling {x : pgame} {xl' xr' : Type u_1} (el : xl' x.left_moves) (er : xr' x.right_moves) :

The game obtained by relabelling the next moves is a relabelling of the original game.

Equations

Negation #

def pgame.neg  :

The negation of {L | R} is {-R | -L}.

Equations
@[protected, instance]
Equations
@[simp]
theorem pgame.neg_def {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
-pgame.mk xl xr xL xR = pgame.mk xr xl (λ (j : xr), -xR j) (λ (i : xl), -xL i)
@[protected, instance]
Equations
@[protected, simp]
theorem pgame.neg_zero  :
-0 = 0
@[simp]
theorem pgame.neg_of_lists (L R : list pgame) :
-pgame.of_lists L R = pgame.of_lists (list.map (λ (x : pgame), -x) R) (list.map (λ (x : pgame), -x) L)
theorem pgame.is_option_neg {x y : pgame} :
@[simp]
theorem pgame.is_option_neg_neg {x y : pgame} :

Turns a right move for x into a left move for -x and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations

Turns a left move for x into a right move for -x and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations

If x has the same moves as y, then -x has the sames moves as -y.

Equations
@[simp]
theorem pgame.neg_le_neg_iff {x y : pgame} :
-y -x x y
@[simp]
theorem pgame.neg_lf_neg_iff {x y : pgame} :
(-y).lf (-x) x.lf y
@[simp]
theorem pgame.neg_lt_neg_iff {x y : pgame} :
-y < -x x < y
@[simp]
theorem pgame.neg_equiv_neg_iff {x y : pgame} :
(-x).equiv (-y) x.equiv y
@[simp]
theorem pgame.neg_fuzzy_neg_iff {x y : pgame} :
(-x).fuzzy (-y) x.fuzzy y
theorem pgame.neg_le_iff {x y : pgame} :
-y x -x y
theorem pgame.neg_lf_iff {x y : pgame} :
(-y).lf x (-x).lf y
theorem pgame.neg_lt_iff {x y : pgame} :
-y < x -x < y
theorem pgame.neg_equiv_iff {x y : pgame} :
(-x).equiv y x.equiv (-y)
theorem pgame.neg_fuzzy_iff {x y : pgame} :
(-x).fuzzy y x.fuzzy (-y)
theorem pgame.le_neg_iff {x y : pgame} :
y -x x -y
theorem pgame.lf_neg_iff {x y : pgame} :
y.lf (-x) x.lf (-y)
theorem pgame.lt_neg_iff {x y : pgame} :
y < -x x < -y
@[simp]
theorem pgame.neg_le_zero_iff {x : pgame} :
-x 0 0 x
@[simp]
theorem pgame.zero_le_neg_iff {x : pgame} :
0 -x x 0
@[simp]
theorem pgame.neg_lf_zero_iff {x : pgame} :
(-x).lf 0 0.lf x
@[simp]
theorem pgame.zero_lf_neg_iff {x : pgame} :
0.lf (-x) x.lf 0
@[simp]
theorem pgame.neg_lt_zero_iff {x : pgame} :
-x < 0 0 < x
@[simp]
theorem pgame.zero_lt_neg_iff {x : pgame} :
0 < -x x < 0
@[simp]
theorem pgame.neg_equiv_zero_iff {x : pgame} :
(-x).equiv 0 x.equiv 0
@[simp]
theorem pgame.neg_fuzzy_zero_iff {x : pgame} :
(-x).fuzzy 0 x.fuzzy 0
@[simp]
theorem pgame.zero_equiv_neg_iff {x : pgame} :
0.equiv (-x) 0.equiv x
@[simp]
theorem pgame.zero_fuzzy_neg_iff {x : pgame} :
0.fuzzy (-x) 0.fuzzy x

Addition and subtraction #

@[protected, instance]

The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations
@[protected, instance]

The pre-game ((0+1)+⋯)+1.

Equations
@[protected, simp]
theorem pgame.nat_succ (n : ) :
(n + 1) = n + 1

x + 0 has exactly the same moves as x.

Equations
theorem pgame.add_zero_equiv (x : pgame) :
(x + 0).equiv x

x + 0 is equivalent to x.

0 + x has exactly the same moves as x.

Equations
theorem pgame.zero_add_equiv (x : pgame) :
(0 + x).equiv x

0 + x is equivalent to x.

Converts a left move for x or y into a left move for x + y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations

Converts a right move for x or y into a right move for x + y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations
@[simp]
theorem pgame.mk_add_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_left (sum.inl i) = (pgame.mk xl xr xL xR).move_left i + pgame.mk yl yr yL yR
@[simp]
@[simp]
theorem pgame.mk_add_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_right (sum.inl i) = (pgame.mk xl xr xL xR).move_right i + pgame.mk yl yr yL yR
@[simp]
theorem pgame.mk_add_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : yl} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_left (sum.inr i) = pgame.mk xl xr xL xR + (pgame.mk yl yr yL yR).move_left i
@[simp]
@[simp]
theorem pgame.mk_add_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : yr} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_right (sum.inr i) = pgame.mk xl xr xL xR + (pgame.mk yl yr yL yR).move_right i
theorem pgame.left_moves_add_cases {x y : pgame} (k : (x + y).left_moves) {P : (x + y).left_moves → Prop} (hl : ∀ (i : x.left_moves), P (pgame.to_left_moves_add (sum.inl i))) (hr : ∀ (i : y.left_moves), P (pgame.to_left_moves_add (sum.inr i))) :
P k
theorem pgame.right_moves_add_cases {x y : pgame} (k : (x + y).right_moves) {P : (x + y).right_moves → Prop} (hl : ∀ (j : x.right_moves), P (pgame.to_right_moves_add (sum.inl j))) (hr : ∀ (j : y.right_moves), P (pgame.to_right_moves_add (sum.inr j))) :
P k
@[protected, instance]
def pgame.relabelling.add_congr {w x y z : pgame} :
w.relabelling xy.relabelling z(w + y).relabelling (x + z)

If w has the same moves as x and y has the same moves as z, then w + y has the same moves as x + z.

Equations
@[protected, instance]
Equations
@[simp]
theorem pgame.sub_zero (x : pgame) :
x - 0 = x + 0
def pgame.relabelling.sub_congr {w x y z : pgame} (h₁ : w.relabelling x) (h₂ : y.relabelling z) :
(w - y).relabelling (x - z)

If w has the same moves as x and y has the same moves as z, then w - y has the same moves as x - z.

Equations
def pgame.neg_add_relabelling (x y : pgame) :
(-(x + y)).relabelling (-x + -y)

-(x + y) has exactly the same moves as -x + -y.

Equations
theorem pgame.neg_add_le {x y : pgame} :
-(x + y) -x + -y
def pgame.add_comm_relabelling (x y : pgame) :
(x + y).relabelling (y + x)

x + y has exactly the same moves as y + x.

Equations
theorem pgame.add_comm_le {x y : pgame} :
x + y y + x
theorem pgame.add_comm_equiv {x y : pgame} :
(x + y).equiv (y + x)
def pgame.add_assoc_relabelling (x y z : pgame) :
(x + y + z).relabelling (x + (y + z))

(x + y) + z has exactly the same moves as x + (y + z).

Equations
theorem pgame.add_assoc_equiv {x y z : pgame} :
(x + y + z).equiv (x + (y + z))
theorem pgame.add_left_neg_le_zero (x : pgame) :
-x + x 0
theorem pgame.zero_le_add_left_neg (x : pgame) :
0 -x + x
theorem pgame.add_left_neg_equiv (x : pgame) :
(-x + x).equiv 0
theorem pgame.add_right_neg_le_zero (x : pgame) :
x + -x 0
theorem pgame.zero_le_add_right_neg (x : pgame) :
0 x + -x
theorem pgame.add_right_neg_equiv (x : pgame) :
(x + -x).equiv 0
theorem pgame.sub_self_equiv (x : pgame) :
(x - x).equiv 0
theorem pgame.add_lf_add_right {y z : pgame} (h : y.lf z) (x : pgame) :
(y + x).lf (z + x)
theorem pgame.add_lf_add_left {y z : pgame} (h : y.lf z) (x : pgame) :
(x + y).lf (x + z)
theorem pgame.add_lf_add_of_lf_of_le {w x y z : pgame} (hwx : w.lf x) (hyz : y z) :
(w + y).lf (x + z)
theorem pgame.add_lf_add_of_le_of_lf {w x y z : pgame} (hwx : w x) (hyz : y.lf z) :
(w + y).lf (x + z)
theorem pgame.add_congr {w x y z : pgame} (h₁ : w.equiv x) (h₂ : y.equiv z) :
(w + y).equiv (x + z)
theorem pgame.add_congr_left {x y z : pgame} (h : x.equiv y) :
(x + z).equiv (y + z)
theorem pgame.add_congr_right {x y z : pgame} :
y.equiv z(x + y).equiv (x + z)
theorem pgame.sub_congr {w x y z : pgame} (h₁ : w.equiv x) (h₂ : y.equiv z) :
(w - y).equiv (x - z)
theorem pgame.sub_congr_left {x y z : pgame} (h : x.equiv y) :
(x - z).equiv (y - z)
theorem pgame.sub_congr_right {x y z : pgame} :
y.equiv z(x - y).equiv (x - z)
theorem pgame.le_iff_sub_nonneg {x y : pgame} :
x y 0 y - x
theorem pgame.lf_iff_sub_zero_lf {x y : pgame} :
x.lf y 0.lf (y - x)
theorem pgame.lt_iff_sub_pos {x y : pgame} :
x < y 0 < y - x

Special pre-games #

def pgame.star  :

The pre-game star, which is fuzzy with zero.

Equations
Instances for pgame.star
@[simp]
theorem pgame.zero_lt_one  :
0 < 1
@[protected, instance]
Equations
@[simp]
theorem pgame.zero_lf_one  :
0.lf 1