Combinatorial games. #
In this file we construct an instance OrderedAddCommGroup SetTheory.Game.
Multiplication on pre-games #
We define the operations of multiplication and inverse on pre-games, and prove a few basic theorems
about them. Multiplication is not well-behaved under equivalence of pre-games i.e. x ≈ y does not
imply x * z ≈ y * z. Hence, multiplication is not a well-defined operation on games. Nevertheless,
the abelian group structure on games allows us to simplify many proofs for pre-games.
The type of combinatorial games. 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 combinatorial pre-game is built
inductively from two families of combinatorial 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.
A combinatorial game is then constructed by quotienting by the equivalence
x ≈ y ↔ x ≤ y ∧ y ≤ x.
Equations
Instances For
Negation of games.
Equations
- SetTheory.Game.instNeg = { neg := Quot.map Neg.neg SetTheory.Game.instNeg.proof_1 }
Equations
- SetTheory.Game.instZero = { zero := ⟦0⟧ }
Equations
- SetTheory.Game.instAdd = { add := Quotient.map₂ HAdd.hAdd ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- SetTheory.Game.instInhabited = { default := 0 }
The less or fuzzy relation on games.
If 0 ⧏ x (less or fuzzy with), then Left can win x as the first player.
Instances For
On Game, simp-normal inequalities should use as few negations as possible.
On Game, simp-normal inequalities should use as few negations as possible.
The fuzzy, confused, or incomparable relation on games.
If x ‖ 0, then the first player can always win x.
Instances For
It can be useful to use these lemmas to turn PGame inequalities into Game inequalities, as
the AddCommGroup structure on Game often simplifies many proofs.
Alias of the forward direction of SetTheory.PGame.equiv_iff_game_eq.
A small family of games is bounded above.
A small set of games is bounded above.
A small family of games is bounded below.
A small set of games is bounded below.
Multiplicative operations can be defined at the level of pre-games, but to prove their properties we need to use the abelian group structure of games. Hence we define them here.
The product of x = {xL | xR} and y = {yL | yR} is
{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL}.
Equations
- One or more equations did not get rendered due to their size.
Turns two left or right moves for x and 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
- SetTheory.PGame.toLeftMovesMul = Equiv.cast ⋯
Instances For
Turns a left and a right move for x and 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
- SetTheory.PGame.toRightMovesMul = Equiv.cast ⋯
Instances For
x * y and y * x have the same moves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
x * y is equivalent to y * x.
x * 0 has exactly the same moves as 0.
Equations
- x.mulZeroRelabelling = SetTheory.PGame.Relabelling.isEmpty (x * 0)
Instances For
x * 0 is equivalent to 0.
0 * x has exactly the same moves as 0.
Equations
- x.zeroMulRelabelling = SetTheory.PGame.Relabelling.isEmpty (0 * x)
Instances For
0 * x is equivalent to 0.
-x * y and -(x * y) have the same moves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
x * -y and -(x * y) have the same moves.
Equations
Instances For
x * (y + z) is equivalent to x * y + x * z.
(x + y) * z is equivalent to x * z + y * z.
x * 1 has the same moves as x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
x * 1 is equivalent to x.
1 * x has the same moves as x.
Equations
- x.oneMulRelabelling = (SetTheory.PGame.mulCommRelabelling 1 x).trans x.mulOneRelabelling
Instances For
1 * x is equivalent to x.
x * y * z is equivalent to x * (y * z).
The left options of x * y of the first kind, i.e. of the form xL * y + x * yL - xL * yL.
Instances For
Any left option of x * y of the first kind is also a left option of x * -(-y) of
the first kind.
The left options of x * y agree with that of y * x up to equivalence.
The left options of x * y of the second kind are the left options of (-x) * (-y) of the
first kind, up to equivalence.
The right options of x * y are the left options of x * (-y) and of (-x) * y of the first
kind, up to equivalence.
Because the two halves of the definition of inv produce more elements
on each side, we have to define the two families inductively.
This is the indexing set for the function, and invVal is the function part.
- zero {l r : Type u} : SetTheory.PGame.InvTy l r false
- left₁ {l r : Type u} : r → SetTheory.PGame.InvTy l r false → SetTheory.PGame.InvTy l r false
- left₂ {l r : Type u} : l → SetTheory.PGame.InvTy l r true → SetTheory.PGame.InvTy l r false
- right₁ {l r : Type u} : l → SetTheory.PGame.InvTy l r false → SetTheory.PGame.InvTy l r true
- right₂ {l r : Type u} : r → SetTheory.PGame.InvTy l r true → SetTheory.PGame.InvTy l r true
Instances For
Equations
- SetTheory.PGame.InvTy.instInhabited l r = { default := SetTheory.PGame.InvTy.zero }
Equations
- SetTheory.PGame.uniqueInvTy l r = { toInhabited := SetTheory.PGame.InvTy.instInhabited l r, uniq := ⋯ }
Because the two halves of the definition of inv produce more elements
of each side, we have to define the two families inductively.
This is the function part, defined by recursion on InvTy.
Equations
- SetTheory.PGame.invVal L R IHl IHr x SetTheory.PGame.InvTy.zero = 0
- SetTheory.PGame.invVal L R IHl IHr x (SetTheory.PGame.InvTy.left₁ i j) = (1 + (R i - x) * SetTheory.PGame.invVal L R IHl IHr x j) * IHr i
- SetTheory.PGame.invVal L R IHl IHr x (SetTheory.PGame.InvTy.left₂ i j) = (1 + (L i - x) * SetTheory.PGame.invVal L R IHl IHr x j) * IHl i
- SetTheory.PGame.invVal L R IHl IHr x (SetTheory.PGame.InvTy.right₁ i j) = (1 + (L i - x) * SetTheory.PGame.invVal L R IHl IHr x j) * IHl i
- SetTheory.PGame.invVal L R IHl IHr x (SetTheory.PGame.InvTy.right₂ i j) = (1 + (R i - x) * SetTheory.PGame.invVal L R IHl IHr x j) * IHr i
Instances For
The inverse of a positive surreal number x = {L | R} is
given by x⁻¹ = {0, (1 + (R - x) * x⁻¹L) * R, (1 + (L - x) * x⁻¹R) * L | (1 + (L - x) * x⁻¹L) * L, (1 + (R - x) * x⁻¹R) * R}.
Because the two halves x⁻¹L, x⁻¹R of x⁻¹ are used in their own
definition, the sets and elements are inductively generated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
inv' 0 has exactly the same moves as 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
inv' 1 has exactly the same moves as 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of a pre-game in terms of the inverse on positive pre-games.
Equations
- SetTheory.PGame.instInv = { inv := fun (x : SetTheory.PGame) => if x ≈ 0 then 0 else if 0 < x then x.inv' else -(-x).inv' }
Equations
- SetTheory.PGame.instDiv = { div := fun (x y : SetTheory.PGame) => x * y⁻¹ }
1⁻¹ has exactly the same moves as 1.