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

We also define sym2.game_add, which is the unordered pair analog of prod.game_add.

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.
sym2.game_add: the game addition relation on unordered pairs.
well_founded.sym2_game_add: formalizes induction on unordered pairs, where exactly one entry decreases at a time.

`prod.game_add` #

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

α × β → α × β → Prop

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.

See sym2.game_add for the unordered pair analog.

theorem prod.game_add_iff {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {x y : α × β} :

prod.game_add rα rβ 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 rα rβ (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 rβ rα a.swap b.swap ↔ prod.game_add rα rβ a b

theorem prod.game_add_swap_swap_mk {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (a₁ a₂ : α) (b₁ b₂ : β) :

prod.game_add rα rβ (a₁, b₁) (a₂, b₂) ↔ prod.game_add rβ rα (b₁, a₁) (b₂, a₂)

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

prod.game_add rα rβ ≤ prod.lex rα rβ

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 rα rβ ≤ relation.trans_gen (prod.game_add rα rβ)

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 rα a) (hb : acc rβ b) :

acc (prod.game_add rα rβ) (a, b)

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.

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

well_founded (prod.game_add rα 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 rα rβ (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 hα hβ 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 rα rβ 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 rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α) (b : β) :

prod.game_add.fix hα hβ IH a b = IH a b (λ (a' : α) (b' : β) (h : prod.game_add rα rβ (a', b') (a, b)), prod.game_add.fix hα hβ IH a' b')

theorem prod.game_add.induction {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Prop} :

well_founded rα → well_founded rβ → (∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), prod.game_add rα rβ (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.

`sym2.game_add` #

def sym2.game_add {α : Type u_1} (rα : α → α → Prop) :

sym2 α → sym2 α → Prop

sym2.game_add rα x y means that x can be reached from y by decreasing either entry with respect to the relation rα.

See prod.game_add for the ordered pair analog.

Equations

sym2.game_add rα = ⇑sym2.lift₂ ⟨λ (a₁ b₁ a₂ b₂ : α), prod.game_add rα rα (a₁, b₁) (a₂, b₂) ∨ prod.game_add rα rα (b₁, a₁) (a₂, b₂), _⟩

theorem sym2.game_add_iff {α : Type u_1} {rα : α → α → Prop} {x y : α × α} :

sym2.game_add rα ⟦x⟧ ⟦y⟧ ↔ prod.game_add rα rα x y ∨ prod.game_add rα rα x.swap y

theorem sym2.game_add_mk_iff {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α} :

sym2.game_add rα ⟦(a₁, b₁)⟧ ⟦(a₂, b₂)⟧ ↔ prod.game_add rα rα (a₁, b₁) (a₂, b₂) ∨ prod.game_add rα rα (b₁, a₁) (a₂, b₂)

theorem prod.game_add.to_sym2 {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α} (h : prod.game_add rα rα (a₁, b₁) (a₂, b₂)) :

sym2.game_add rα ⟦(a₁, b₁)⟧ ⟦(a₂, b₂)⟧

theorem sym2.game_add.fst {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) :

sym2.game_add rα ⟦(a₁, b)⟧ ⟦(a₂, b)⟧

theorem sym2.game_add.snd {α : Type u_1} {rα : α → α → Prop} {a b₁ b₂ : α} (h : rα b₁ b₂) :

sym2.game_add rα ⟦(a, b₁)⟧ ⟦(a, b₂)⟧

theorem sym2.game_add.fst_snd {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) :

sym2.game_add rα ⟦(a₁, b)⟧ ⟦(b, a₂)⟧

theorem sym2.game_add.snd_fst {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) :

sym2.game_add rα ⟦(b, a₁)⟧ ⟦(a₂, b)⟧

theorem acc.sym2_game_add {α : Type u_1} {rα : α → α → Prop} {a b : α} (ha : acc rα a) (hb : acc rα b) :

acc (sym2.game_add rα) ⟦(a, b)⟧

theorem well_founded.sym2_game_add {α : Type u_1} {rα : α → α → Prop} (h : well_founded rα) :

well_founded (sym2.game_add rα)

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

def sym2.game_add.fix {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_2} (hr : well_founded rα) (IH : Π (a₁ b₁ : α), (Π (a₂ b₂ : α), sym2.game_add rα ⟦(a₂, b₂)⟧ ⟦(a₁, b₁)⟧ → C a₂ b₂) → C a₁ b₁) (a b : α) :

C a b

Recursion on the well-founded sym2.game_add relation.

Equations

sym2.game_add.fix hr IH a b = _.fix (λ (_x : α × α), sym2.game_add.fix._match_1 IH _x) (a, b)
sym2.game_add.fix._match_1 IH (x₁, x₂) = λ (IH' : Π (y : α × α), (λ (a b : α × α), ⟨λ (a₁ b₁ a₂ b₂ : α), prod.game_add rα rα (a₁, b₁) (a₂, b₂) ∨ prod.game_add rα rα (b₁, a₁) (a₂, b₂), _⟩.val a.fst a.snd b.fst b.snd) y (x₁, x₂) → (λ (x : α × α), C x.fst x.snd) y), IH x₁ x₂ (λ (a' b' : α), IH' (a', b'))

theorem sym2.game_add.fix_eq {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_2} (hr : well_founded rα) (IH : Π (a₁ b₁ : α), (Π (a₂ b₂ : α), sym2.game_add rα ⟦(a₂, b₂)⟧ ⟦(a₁, b₁)⟧ → C a₂ b₂) → C a₁ b₁) (a b : α) :

sym2.game_add.fix hr IH a b = IH a b (λ (a' b' : α) (h : sym2.game_add rα ⟦(a', b')⟧ ⟦(a, b)⟧), sym2.game_add.fix hr IH a' b')

theorem sym2.game_add.induction {α : Type u_1} {rα C : α → α → Prop} :

well_founded rα → (∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), sym2.game_add rα ⟦(a₂, b₂)⟧ ⟦(a₁, b₁)⟧ → C a₂ b₂) → C a₁ b₁) → ∀ (a b : α), C a b

Induction on the well-founded sym2.game_add relation.