Combinatorial games.
In this file we define the quotient of pre-games by the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤
p, and construct an instance add_comm_group game, as well as an instance partial_order game
(although note carefully the warning that the < field in this instance is not the usual relation
on combinatorial 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
Equations
Equations
- game.add_monoid = {add := add_semigroup.add game.add_semigroup, add_assoc := _, zero := 0, zero_add := game.zero_add, add_zero := game.add_zero}
Equations
- game.add_group = {add := add_monoid.add game.add_monoid, add_assoc := _, zero := add_monoid.zero game.add_monoid, zero_add := _, add_zero := _, neg := has_neg.neg game.has_neg, add_left_neg := game.add_left_neg}
Equations
Equations
- game.add_comm_group = {add := add_comm_semigroup.add game.add_comm_semigroup, add_assoc := _, zero := add_group.zero game.add_group, zero_add := _, add_zero := _, neg := add_group.neg game.add_group, add_left_neg := _, add_comm := _}
The < operation provided by this partial order is not the usual < on games!
Equations
- game.game_partial_order = {le := has_le.le game.has_le, lt := preorder.lt._default has_le.le, le_refl := game.le_refl, le_trans := game.le_trans, lt_iff_le_not_le := game.game_partial_order._proof_1, le_antisymm := game.le_antisymm}
The < operation provided by this ordered_add_comm_group is not the usual < on games!