mathlib documentation

order.game_add

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 and ). It is so called since it models the subsequency relation on the addition of combinatorial games.

Main definitions and results #

Todo #

inductive prod.game_add {α : Type u_1} {β : Type u_2} (rα : α α Prop) (rβ : β β Prop) :
α × β α × β Prop

prod.game_add rα rβ x y means that x can be reached from y by decreasing either entry with respect to the relations and .

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.

theorem prod.game_add_iff {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {x y : α × β} :
prod.game_add x y rα x.fst y.fst x.snd = y.snd rβ x.snd y.snd x.fst = y.fst
theorem prod.game_add_mk_iff {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {a₁ a₂ : α} {b₁ b₂ : β} :
prod.game_add (a₁, b₁) (a₂, b₂) rα a₁ a₂ b₁ = b₂ rβ b₁ b₂ a₁ = a₂
@[simp]
theorem prod.game_add_swap_swap {α : Type u_1} {β : Type u_2} (rα : α α Prop) (rβ : β β Prop) (a b : α × β) :
prod.game_add a.swap b.swap prod.game_add a b
theorem prod.game_add_le_lex {α : Type u_1} {β : Type u_2} (rα : α α Prop) (rβ : β β Prop) :
prod.game_add prod.lex

prod.game_add is a subrelation of prod.lex.

theorem prod.rprod_le_trans_gen_game_add {α : Type u_1} {β : Type u_2} (rα : α α Prop) (rβ : β β Prop) :

prod.rprod is a subrelation of the transitive closure of prod.game_add.

theorem acc.prod_game_add {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {a : α} {b : β} (ha : acc a) (hb : acc b) :
acc (prod.game_add rβ) (a, b)

If a is accessible under and b is accessible under , then (a, b) is accessible under prod.game_add rα rβ. Notice that prod.lex_accessible requires the stronger condition ∀ b, acc rβ b.

theorem well_founded.prod_game_add {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} (hα : well_founded rα) (hβ : well_founded rβ) :

The prod.game_add relation on well-founded inputs is well-founded.

In particular, the sum of two well-founded games is well-founded.

def prod.game_add.fix {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {C : α β Sort u_3} (hα : well_founded rα) (hβ : well_founded rβ) (IH : Π (a₁ : α) (b₁ : β), (Π (a₂ : α) (b₂ : β), prod.game_add (a₂, b₂) (a₁, b₁) C a₂ b₂) C a₁ b₁) (a : α) (b : β) :
C a b

Recursion on the well-founded prod.game_add relation.

Note that it's strictly more general to recurse on the lexicographic order instead.

Equations
  • prod.game_add.fix IH a b = _.fix (λ (_x : α × β), prod.game_add.fix._match_1 IH _x) (a, b)
  • prod.game_add.fix._match_1 IH (x₁, x₂) = λ (IH' : Π (y : α × β), prod.game_add y (x₁, x₂) (λ (x : α × β), C x.fst x.snd) y), IH x₁ x₂ (λ (a' : α) (b' : β), IH' (a', b'))
theorem prod.game_add.fix_eq {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {C : α β Sort u_3} (hα : well_founded rα) (hβ : well_founded rβ) (IH : Π (a₁ : α) (b₁ : β), (Π (a₂ : α) (b₂ : β), prod.game_add (a₂, b₂) (a₁, b₁) C a₂ b₂) C a₁ b₁) (a : α) (b : β) :
prod.game_add.fix IH a b = IH a b (λ (a' : α) (b' : β) (h : prod.game_add (a', b') (a, b)), prod.game_add.fix IH a' b')
theorem prod.game_add.induction {α : Type u_1} {β : Type u_2} {rα : α α Prop} {rβ : β β Prop} {C : α β Prop} :
well_founded well_founded ( (a₁ : α) (b₁ : β), ( (a₂ : α) (b₂ : β), prod.game_add (a₂, b₂) (a₁, b₁) C a₂ b₂) C a₁ b₁) (a : α) (b : β), C a b

Induction on the well-founded prod.game_add relation.

Note that it's strictly more general to induct on the lexicographic order instead.