# mathlib3documentation

set_theory.game.pgame

# Combinatorial (pre-)games. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• The theory of dominated and reversible positions, and unique normal form for short games.
• Analysis of basic domineering positions.
• Hex.
• Temperature.
• The development of surreal numbers, based on this development of combinatorial games, is still quite incomplete.

## 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`

The indexing type for allowable moves by Left.

Equations
Instances for `pgame.left_moves`

The indexing type for allowable moves by Right.

Equations
Instances for `pgame.right_moves`
def pgame.move_left (g : pgame) :

The new game after Left makes an allowed move.

Equations
Instances for `pgame.move_left`
def pgame.move_right (g : pgame) :

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
theorem pgame.of_lists_move_left {L R : list pgame} (i : fin L.length) :
= L.nth_le i _
@[simp]
theorem pgame.of_lists_move_left' {L R : list pgame} (i : R).left_moves) :
R).move_left i = _
theorem pgame.of_lists_move_right {L R : list pgame} (i : fin R.length) :
= R.nth_le i _
@[simp]
theorem pgame.of_lists_move_right' {L R : list pgame} (i : R).right_moves) :
R).move_right i = _
def pgame.move_rec_on {C : pgame Sort 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  :

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

`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`
@[protected, instance]
@[trans]
@[protected, instance]
Equations
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)
meta def pgame.pgame_wf_tac  :

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
@[simp]
theorem pgame.zero_left_moves  :
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]

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

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

### Pre-game order relations #

@[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`
@[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_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 `⧏`.

The ordering here is chosen so that `and.left` refer to moves by Left, and `and.right` refer to moves by Right.

@[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_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
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 `≤`.

The ordering here is chosen so that `or.inl` refer to moves by Left, and `or.inr` refer to moves by Right.

@[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.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 i x.lf (pgame.mk yl yr yL yR)
@[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.

@[simp]
@[simp]
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.upper_bound {ι : Type u} (f : ι pgame) :

An explicit upper bound for a family of pre-games, whose left moves are the union of the left moves of all the pre-games in the family.

Equations
@[protected, instance]
theorem pgame.le_upper_bound {ι : Type u} (f : ι pgame) (i : ι) :
f i

A small set `s` of pre-games is bounded above.

def pgame.lower_bound {ι : Type u} (f : ι pgame) :

An explicit lower bound for a family of pre-games, whose right moves are the union of the right moves of all the pre-games in the family.

Equations
@[protected, instance]
theorem pgame.lower_bound_le {ι : Type u} (f : ι pgame) (i : ι) :
f i

A small set `s` of pre-games is bounded below.

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 y y.equiv x
@[protected, trans]
theorem pgame.equiv.trans {x y z : pgame} :
x.equiv y y.equiv z x.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 z x 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 z x.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 < z x < 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 y y.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 y x < 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.relabelling  :

`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 `relabelling`s 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
@[refl]

The identity relabelling.

Equations
@[protected, instance]
Equations
@[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]

Transitivity of relabelling.

Equations

Any game without left or right moves is a relabelling of 0.

Equations
theorem pgame.equiv.is_empty (x : pgame)  :
x.equiv 0
@[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') :
er).move_left i = x.move_left (el i)
@[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) :
er).move_left ((el.symm) i) = x.move_left i
@[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') :
er).move_right j = x.move_right (er j)
@[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) :
er).move_right ((er.symm) j) = x.move_right j
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, instance]
Equations
@[simp]
theorem pgame.neg_of_lists (L R : list pgame) :
- = 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
theorem pgame.move_left_neg {x : pgame} (i : x.right_moves) :
@[simp]
theorem pgame.move_left_neg' {x : pgame} (i : (-x).left_moves) :
(-x).move_left i = -
theorem pgame.move_right_neg {x : pgame} (i : x.left_moves) :
@[simp]
theorem pgame.move_right_neg' {x : pgame} (i : (-x).right_moves) :
theorem pgame.move_left_neg_symm {x : pgame} (i : (-x).right_moves) :
theorem pgame.move_right_neg_symm {x : pgame} (i : (-x).left_moves) :
= -(-x).move_left i

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

@[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
@[protected, instance]
@[protected, instance]

`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]
theorem pgame.add_move_left_inl {x : pgame} (y : pgame) (i : x.left_moves) :
(x + y).move_left = x.move_left i + y
@[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.add_move_right_inl {x : pgame} (y : pgame) (i : x.right_moves) :
(x + y).move_right = x.move_right i + y
@[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]
theorem pgame.add_move_left_inr (x : pgame) {y : pgame} (i : y.left_moves) :
(x + y).move_left = x + y.move_left i
@[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
@[simp]
theorem pgame.add_move_right_inr (x : pgame) {y : pgame} (i : y.right_moves) :
(x + y).move_right = x + y.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 ) (hr : (i : y.left_moves), P ) :
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 ) (hr : (j : y.right_moves), P ) :
P k
@[protected, instance]
def pgame.relabelling.add_congr {w x y z : pgame} :

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
@[protected, instance]
@[protected, instance]
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)
@[protected, instance]
@[protected, instance]
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]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem pgame.neg_star  :
@[protected, simp]
theorem pgame.zero_lt_one  :
0 < 1
@[protected, instance]
Equations
@[simp]
theorem pgame.zero_lf_one  :
0.lf 1