Game addition relation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.prod_game_add
: formalizes induction on ordered pairs, where exactly one entry decreases at a time.
Todo #
- 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₂)
prod.game_add rα rβ x y
means that x
can be reached from y
by decreasing either entry with
respect to the relations rα
and rβ
.
It is so called, as it models game addition within combinatorial game theory. 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.
prod.game_add
is a subrelation
of prod.lex
.
prod.rprod
is a subrelation of the transitive closure of prod.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 prod.game_add
relation on well-founded inputs is well-founded.
In particular, the sum of two well-founded games is well-founded.
Recursion on the well-founded prod.game_add
relation.
Note that it's strictly more general to recurse on the lexicographic order instead.
Induction on the well-founded prod.game_add
relation.
Note that it's strictly more general to induct on the lexicographic order instead.