Documentation

LeanPool.ConwayRefinement.CombinatorialGames.Game.Basic

Combinatorial games #

In this file we construct the quotient of games IGame under equivalence, and prove that it forms an OrderedAddCommGroup. We take advantage of this structure to prove two particularly tedious theorems on IGame, namely IGame.mul_add_equiv and IGame.mul_assoc_equiv.

It might be tempting to write mk (x * y) as mk x * mk y, but the latter is not well-defined, as there exist x₁ ≈ x₂ and y₁ ≈ y₂ with x₁ * y₁ ≉ x₂ * y₂. See CombinatorialGames.Counterexamples.Multiplication for a proof.

def ConwayGame :

Type (u + 1)

Games up to equivalence.

If x and y are combinatorial games (IGame), we say that x ≈ y when both x ≤ y and y ≤ x. Broadly, this means neither player has a preference in playing either game, as a component of a larger game. This is the standard meaning of x = y in the literature, though it is not a strict equality, e.g. {0, 1 | 0} and {1 | 0} are equivalent, but not identical as the former has an extra move for Left.

In particular, note that a ConwayGame has no well-defined notion of left and right options. This means you should prefer IGame when analyzing specific games.

Equations

ConwayGame = Antisymmetrization IGame fun (x1 x2 : IGame) => x1 ≤ x2

Instances For

def ConwayGame.mk (x : IGame) :

The quotient map from IGame into ConwayGame.

Equations

ConwayGame.mk x = ⟦x⟧

Instances For

theorem ConwayGame.mk_eq_mk {x y : IGame} :

mk x = mk y ↔ x ≈ y

theorem ConwayGame.mk_eq {x y : IGame} :

x ≈ y → mk x = mk y

Alias of the reverse direction of ConwayGame.mk_eq_mk.

theorem ConwayGame.ind {motive : ConwayGame → Prop} (mk : ∀ (y : IGame), motive (mk y)) (x : ConwayGame) :

motive x

noncomputable def ConwayGame.out (x : ConwayGame) :

Choose an element of the equivalence class using the axiom of choice.

Equations

x.out = Quotient.out x

Instances For

@[simp]

theorem ConwayGame.out_eq (x : ConwayGame) :

mk x.out = x

theorem ConwayGame.mk_out_equiv (x : IGame) :

(mk x).out ≈ x

theorem ConwayGame.equiv_mk_out (x : IGame) :

x ≈ (mk x).out

@[instance_reducible]

noncomputable instance ConwayGame.instOfSetsTrue :

OfSets ConwayGame fun (x : Player → Set ConwayGame) => True

Construct a ConwayGame from its left and right sets.

Note that although this function is well-defined, this function isn't injective, nor do equivalence classes in ConwayGame have a canonical representative.

Equations

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

theorem ConwayGame.mk_ofSets' (st : Player → Set IGame) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] :

mk !{st} = !{fun (p : Player) => mk '' st p}

@[simp]

theorem ConwayGame.mk_ofSets (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] :

mk !{s | t} = !{mk '' s | mk '' t}

@[instance_reducible]

noncomputable instance ConwayGame.instZero :

Zero ConwayGame

Equations

ConwayGame.instZero = { zero := ConwayGame.mk 0 }

@[instance_reducible]

noncomputable instance ConwayGame.instOne :

Equations

ConwayGame.instOne = { one := ConwayGame.mk 1 }

@[instance_reducible]

noncomputable instance ConwayGame.instAdd :

Equations

ConwayGame.instAdd = { add := Quotient.map₂ HAdd.hAdd @IGame.add_congr }

@[instance_reducible]

noncomputable instance ConwayGame.instNeg :

Equations

ConwayGame.instNeg = { neg := Quotient.map Neg.neg @IGame.neg_congr }

@[instance_reducible]

instance ConwayGame.instPartialOrder :

PartialOrder ConwayGame

Equations

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

@[instance_reducible]

noncomputable instance ConwayGame.instInhabited :

Inhabited ConwayGame

Equations

ConwayGame.instInhabited = { default := 0 }

@[instance_reducible]

noncomputable instance ConwayGame.instAddCommGroupWithOne :

AddCommGroupWithOne ConwayGame

Equations

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

instance ConwayGame.instIsOrderedAddMonoid :

IsOrderedAddMonoid ConwayGame

@[instance_reducible]

noncomputable instance ConwayGame.instRatCast :

RatCast ConwayGame

Equations

ConwayGame.instRatCast = { ratCast := fun (q : ℚ) => ConwayGame.mk ↑q }

@[simp]

theorem ConwayGame.mk_zero :

mk 0 = 0

@[simp]

theorem ConwayGame.mk_one :

mk 1 = 1

@[simp]

theorem ConwayGame.mk_add (x y : IGame) :

mk (x + y) = mk x + mk y

@[simp]

theorem ConwayGame.mk_neg (x : IGame) :

mk (-x) = -mk x

@[simp]

theorem ConwayGame.mk_sub (x y : IGame) :

mk (x - y) = mk x - mk y

theorem ConwayGame.mk_mulOption (x y a b : IGame) :

mk (IGame.mulOption x y a b) = mk (a * y) + mk (x * b) - mk (a * b)

@[simp]

theorem ConwayGame.mk_le_mk {x y : IGame} :

mk x ≤ mk y ↔ x ≤ y

@[simp]

theorem ConwayGame.mk_lt_mk {x y : IGame} :

mk x < mk y ↔ x < y

@[simp]

theorem ConwayGame.mk_fuzzy_mk {x y : IGame} :

mk x ‖ mk y ↔ x ‖ y

@[simp]

theorem ConwayGame.mk_natCast (n : ℕ) :

mk ↑n = ↑n

@[simp]

theorem ConwayGame.mk_intCast (n : ℤ) :

mk ↑n = ↑n

@[simp]

theorem ConwayGame.mk_ratCast (q : ℚ) :

mk ↑q = ↑q

@[simp]

theorem ConwayGame.ratCast_neg (q : ℚ) :

↑(-q) = -↑q

theorem ConwayGame.zero_def :

0 = !{fun (x : Player) => ∅}

theorem ConwayGame.one_def :

1 = !{{0} | ∅}

instance ConwayGame.instZeroLEOneClass :

ZeroLEOneClass ConwayGame

instance ConwayGame.instNeZeroOfNat :

instance ConwayGame.instNontrivial :

Nontrivial ConwayGame

instance ConwayGame.instCharZero :

CharZero ConwayGame

theorem ConwayGame.mk_mul_add (x y z : IGame) :

mk (x * (y + z)) = mk (x * y) + mk (x * z)

theorem ConwayGame.mk_mul_sub (x y z : IGame) :

mk (x * (y - z)) = mk (x * y) - mk (x * z)

theorem ConwayGame.mk_add_mul (x y z : IGame) :

mk ((x + y) * z) = mk (x * z) + mk (y * z)

theorem ConwayGame.mk_sub_mul (x y z : IGame) :

mk ((x - y) * z) = mk (x * z) - mk (y * z)

theorem ConwayGame.mk_mul_assoc (x y z : IGame) :

mk (x * y * z) = mk (x * (y * z))

theorem ConwayGame.lf_ofSets_of_mem_left {s t : Set ConwayGame} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {x : ConwayGame} (h : x ∈ s) :

¬!{s | t} ≤ x

theorem ConwayGame.ofSets_lf_of_mem_right {s t : Set ConwayGame} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {x : ConwayGame} (h : x ∈ t) :

¬x ≤ !{s | t}

theorem IGame.sub_le_iff_le_add {x y z : IGame} :

x - z ≤ y ↔ x ≤ y + z

theorem IGame.le_sub_iff_add_le {x y z : IGame} :

x ≤ z - y ↔ x + y ≤ z

theorem IGame.sub_lt_iff_lt_add {x y z : IGame} :

x - z < y ↔ x < y + z

theorem IGame.lt_sub_iff_add_lt {x y z : IGame} :

x < z - y ↔ x + y < z

theorem IGame.sub_nonneg {x y : IGame} :

0 ≤ x - y ↔ y ≤ x

theorem IGame.sub_nonpos {x y : IGame} :

x - y ≤ 0 ↔ x ≤ y

theorem IGame.sub_pos {x y : IGame} :

0 < x - y ↔ y < x

theorem IGame.sub_neg {x y : IGame} :

x - y < 0 ↔ x < y

theorem IGame.mul_add_equiv (x y z : IGame) :

x * (y + z) ≈ x * y + x * z

theorem IGame.mul_sub_equiv (x y z : IGame) :

x * (y - z) ≈ x * y - x * z

theorem IGame.add_mul_equiv (x y z : IGame) :

(x + y) * z ≈ x * z + y * z

theorem IGame.sub_mul_equiv (x y z : IGame) :

(x - y) * z ≈ x * z - y * z

theorem IGame.mul_assoc_equiv (x y z : IGame) :

x * y * z ≈ x * (y * z)

@[simp]

theorem IGame.natCast_le {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem IGame.natCast_lt {m n : ℕ} :

↑m < ↑n ↔ m < n

@[simp]

theorem IGame.natCast_nonneg (n : ℕ) :

0 ≤ ↑n

theorem IGame.natCast_strictMono :

StrictMono Nat.cast

instance IGame.instCharZero :

@[simp]

theorem IGame.natCast_equiv {m n : ℕ} :

↑m ≈ ↑n ↔ m = n

@[simp]

theorem IGame.intCast_le {m n : ℤ} :

↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem IGame.intCast_lt {m n : ℤ} :

↑m < ↑n ↔ m < n

theorem IGame.intCast_strictMono :

StrictMono Int.cast

@[simp]

theorem IGame.intCast_inj {m n : ℤ} :

↑m = ↑n ↔ m = n

@[simp]

theorem IGame.intCast_equiv {m n : ℤ} :

↑m ≈ ↑n ↔ m = n

theorem IGame.intCast_add_equiv (m n : ℤ) :

↑(m + n) ≈ ↑m + ↑n

theorem IGame.intCast_sub_equiv (m n : ℤ) :

↑(m - n) ≈ ↑m - ↑n

@[simp]

theorem IGame.zero_lt_intCast {n : ℤ} :

0 < ↑n ↔ 0 < n

@[simp]

theorem IGame.intCast_lt_zero {n : ℤ} :

↑n < 0 ↔ n < 0

@[simp]

theorem IGame.zero_le_intCast {n : ℤ} :

0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem IGame.intCast_le_zero {n : ℤ} :

↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem IGame.Impartial.neg_mk (x : IGame) [hx : x.Impartial] :

-ConwayGame.mk x = ConwayGame.mk x

@[simp]

theorem IGame.Impartial.sub_mk (y : IGame) [hy : y.Impartial] (x : ConwayGame) :

x - ConwayGame.mk y = x + ConwayGame.mk y

@[simp]

theorem IGame.Impartial.mk_add_self (x : IGame) [hx : x.Impartial] :

ConwayGame.mk x + ConwayGame.mk x = 0

theorem IGame.Impartial.add_self_equiv (x : IGame) [x.Impartial] :

x + x ≈ 0

theorem IGame.Impartial.equiv_iff_add_equiv_zero {x y : IGame} [hy : y.Impartial] :

x ≈ y ↔ x + y ≈ 0

This lemma doesn't require x to be impartial.

theorem IGame.Impartial.equiv_iff_add_equiv_zero' {x y : IGame} [hx : x.Impartial] :

x ≈ y ↔ x + y ≈ 0

This lemma doesn't require y to be impartial.

theorem IGame.Impartial.fuzzy_iff_add_fuzzy_zero {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :

x ‖ y ↔ x + y ‖ 0