Game addition relation #
This file defines, given relations rα : α → α → Prop
and rβ : β → β → Prop
, a relation
prod.game_add
on pairs, such that game_add rα rβ x y
iff x
can be reached from y
by
decreasing either entry (with respect to rα
and rβ
). It is so called since it models the
subsequency relation on the addition of combinatorial games.
Main definitions and results #
prod.game_add
: the game addition relation on ordered pairs.well_founded.game_add
: formalizes induction on ordered pairs, where exactly one entry decreases at a time.
Todo #
- Add custom
induction
andfix
lemmas. - Define
sym2.game_add
.
- fst : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a' a : α} {b : β}, rα a' a → prod.game_add rα rβ (a', b) (a, b)
- snd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b' b : β}, rβ b' b → prod.game_add rα rβ (a, b') (a, b)
The "addition of games" relation in combinatorial game theory, on the product type: if
rα a' a
means that a ⟶ a'
is a valid move in game α
, and rβ b' b
means that b ⟶ b'
is a valid move in game β
, then game_add rα rβ
specifies the valid moves in the juxtaposition
of α
and β
: the player is free to choose one of the games and make a move in it,
while leaving the other game unchanged.
game_add
is a subrelation
of prod.lex
.
prod.rprod
is a subrelation of the transitive closure of game_add
.
If a
is accessible under rα
and b
is accessible under rβ
, then (a, b)
is
accessible under prod.game_add rα rβ
. Notice that prod.lex_accessible
requires the
stronger condition ∀ b, acc rβ b
.
The sum of two well-founded games is well-founded.