Define combinatorial games as well-founded bi-labelled directed graphs of positions and moves.

graph_game.lean

import order.antisymmetrization
import algebra.order.group

universe u

section union
variables {α : Type*} (p q : α → α → Prop)
instance : has_union (α → α → Prop) := ⟨λ p q x y, p x y ∨ q x y⟩
instance : has_emptyc (α → α → Prop) := ⟨empty_relation⟩
lemma union_comm : p ∪ q = q ∪ p := by { ext, exact or.comm }
lemma empty_union_empty : (∅ : α → α → Prop) ∪ ∅ = ∅ := by { ext, apply or_false }
end union

structure pgame :=
(pos : Type u)
(L R : pos → pos → Prop) /- L x y means x is a option at position y for left -/
(wf : well_founded (L ∪ R))
(start : pos)

namespace pgame

/- Change the start position to `p` in a game `g`. -/
def pos.game {g : pgame} (p : g.pos) : pgame := { start := p .. g }
lemma game_start (g : pgame) : g.start.game = g := by { cases g, refl }
/- involves type equality, not recommended? -/

/-- Negation of game. -/
instance : has_neg pgame :=
{ neg := λ g,
  { pos := g.pos,
    L := g.R,
    R := g.L,
    wf := union_comm g.L g.R ▸ g.wf,
    start := g.start } }

/-- The zero game. -/
instance : has_zero pgame.{u} :=
{ zero :=
  { pos := punit,
    L := ∅,
    R := ∅,
    wf := empty_union_empty.substr empty_wf,
    start := punit.star } }

/-! Addition of games. -/

section relation
variables {α β : Type*} (rα rα' : α → α → Prop) (rβ rβ' : β → β → Prop)

inductive add_rel : α × β → α × β → Prop
| fst : ∀ {a a'} b, rα a a' → add_rel (a,b) (a',b)
| snd : ∀ a {b b'}, rβ b b' → add_rel (a,b) (a,b')

namespace add_rel

section symm_assoc
variables {γ δ : Type*} {rα rβ} {rγ : γ → γ → Prop} {rδ : δ → δ → Prop}
variables {a a' : α} {b b' : β} {c c' : γ} {d d' : δ}

lemma empty : add_rel rα ∅ (a, b) (a', b') ↔ rα a a' ∧ b = b' :=
⟨by { rintro (⟨_,_,_,h⟩|⟨_,_,_,h⟩), exacts [⟨h, rfl⟩, h.elim] }, λ ⟨h,he⟩, he ▸ fst b h⟩

lemma punit {b b' : punit} : add_rel rα ∅ (a, b) (a', b') ↔ rα a a' :=
empty.trans ⟨λ h, h.1, λ h, ⟨h, by ext⟩⟩

lemma symm_aux : ∀ {a a' : α} {b b' : β},
  add_rel rα rβ (a, b) (a', b') → add_rel rβ rα (b, a) (b', a')
| _ _ _ _ (fst b h) := snd b h
| _ _ _ _ (snd a h) := fst a h

lemma symm : add_rel rα rβ (a, b) (a', b') ↔ add_rel rβ rα (b, a) (b', a') :=
⟨symm_aux, symm_aux⟩

lemma assoc :
  add_rel (add_rel rα rβ) rγ ((a, b), c) ((a', b'), c') ↔
  add_rel rα (add_rel rβ rγ) (a, b, c) (a', b', c') :=
⟨ by { rintro (⟨_,_,_,(⟨_,_,_,h⟩|⟨_,_,_,h⟩)⟩|⟨_,_,_,h⟩),
    exacts [fst (b, c) h, snd a (fst c h), snd a (snd b h)] },
  by { rintro (⟨_,_,_,h⟩|⟨_,_,_,(⟨_,_,_,h⟩|⟨_,_,_,h⟩)⟩),
    exacts [fst c (fst b h), fst c (snd a h), snd (a, b) h] } ⟩
/- Is there a way to assign a name to `h` without writing the annoying `⟨_,_,_,h⟩`?
  Assign a name to `rα a a'` in `add_rel` doesn't work. -/

/-- Cyclic permutation of order 3 in the last three coordinates in (α × β) × (γ × δ).
  Allows us to freely switch between the three 2x2 partitions of the four types. -/
lemma cycperm :
  add_rel (add_rel rα rβ) (add_rel rγ rδ) ((a,b),c,d) ((a',b'),c',d') →
  add_rel (add_rel rα rγ) (add_rel rδ rβ) ((a,c),d,b) ((a',c'),d',b') := by
{ rintro (⟨_,_,_,(⟨_,_,_,h⟩|⟨_,_,_,h⟩)⟩|⟨_,_,_,(⟨_,_,_,h⟩|⟨_,_,_,h⟩)⟩),
  exacts [fst _ (fst _ h), snd _ (snd _ h), fst _ (snd _ h), snd _ (fst _ h)] }

lemma cycperm_iff :
  add_rel (add_rel rα rβ) (add_rel rγ rδ) ((a,b),c,d) ((a',b'),c',d') ↔
  add_rel (add_rel rα rγ) (add_rel rδ rβ) ((a,c),d,b) ((a',c'),d',b') :=
⟨cycperm, cycperm ∘ cycperm⟩

end symm_assoc

lemma subrelation_lex : subrelation (add_rel rα rβ) (prod.lex rα rβ)
| _ _ (fst b h) := prod.lex.left b b h
| _ _ (snd a h) := prod.lex.right a h

open or
lemma union : add_rel (rα ∪ rα') (rβ ∪ rβ') = add_rel rα rβ ∪ add_rel rα' rβ' :=
begin
  ext c₁ c₂, split,
  { rintro (⟨_,_,b,(h|h)⟩|⟨a,_,_,(h|h)⟩),
    exacts [inl (fst b h), inr (fst b h), inl (snd a h), inr (snd a h)] },
  { rintro ((⟨_,_,b,h⟩|⟨a,_,_,h⟩)|⟨_,_,b,h⟩|⟨a,_,_,h⟩),
    exacts [fst b (inl h), snd a (inl h), fst b (inr h), snd a (inr h)] },
end

end add_rel

variables {rα rα'} {a a₁ a₂ : α}
lemma tc_L_R (h₁ : rα a a₁) (h₂ : rα' a₁ a₂) : tc (rα ∪ rα') a a₂ :=
tc.trans a a₁ a₂ (tc.base a a₁ $ or.inl h₁) (tc.base a₁ a₂ $ or.inr h₂)
lemma tc_R_L (h₁ : rα' a a₁) (h₂ : rα a₁ a₂) : tc (rα ∪ rα') a a₂ :=
tc.trans a a₁ a₂ (tc.base a a₁ $ or.inr h₁) (tc.base a₁ a₂ $ or.inl h₂)

end relation

/-- Addition of games. -/
instance : has_add pgame.{u} :=
{ add := λ g₁ g₂,
  { pos := g₁.pos × g₂.pos,
    L := add_rel g₁.L g₂.L,
    R := add_rel g₁.R g₂.R,
    wf := add_rel.union g₁.L g₁.R g₂.L g₂.R ▸
      (add_rel.subrelation_lex _ _).wf (prod.lex_wf g₁.wf g₂.wf),
    start := (g₁.start, g₂.start) } }

instance : has_sub pgame.{u} := { sub := λ g₁ g₂, g₁ + (-g₂) }

lemma neg_zero : -(0 : pgame) = 0 := rfl
lemma neg_neg {g : pgame} : -(-g) = g := by { cases g, refl }
lemma neg_add {g₁ g₂ : pgame} : -(g₁ + g₂) = -g₁ + -g₂ := rfl

variables {g : pgame.{u}} (p : g.pos)
section win_lose
/-- L wins position p (playing first) iff there exists a move to some position p' such that
    R loses p'; R loses p iff for all moves, L wins the resulting position p'. -/
def Lwin_Rlose_pos : g.pos → Prop × Prop :=
g.wf.fix $ λ p f, (∃ p' h, (f p' $ or.inl h).2, ∀ p' h, (f p' $ or.inr h).1)
def Lwin_pos := (Lwin_Rlose_pos p).1
def Rlose_pos := (Lwin_Rlose_pos p).2
/- TODO : could carry the data/"certificate" of a winning strategy: many implications
   between `Rlose` below are actually explicit maps between winning stratagies. -/

variable {p}
lemma Lwin_Rlose_pos_iff : Lwin_Rlose_pos p =
  (∃ p', g.L p' p ∧ (Lwin_Rlose_pos p').2, ∀ p', g.R p' p → (Lwin_Rlose_pos p').1) :=
by { convert g.wf.fix_eq _ p, ext, split; exact λ ⟨h,h'⟩, ⟨h,h'⟩ }

lemma Lwin_pos_iff : Lwin_pos p ↔ ∃ p', g.L p' p ∧ Rlose_pos p' :=
(prod.ext_iff.1 Lwin_Rlose_pos_iff).1.to_iff
lemma Rlose_pos_iff : Rlose_pos p ↔ ∀ p', g.R p' p → Lwin_pos p' :=
(prod.ext_iff.1 Lwin_Rlose_pos_iff).2.to_iff
lemma Lwin_pos_iff₂ : Lwin_pos p ↔ ∃ p₁, g.L p₁ p ∧ ∀ p₂, g.R p₂ p₁ → Lwin_pos p₂ :=
by { rw Lwin_pos_iff, simp_rw Rlose_pos_iff }
lemma Rlose_pos_iff₂ : Rlose_pos p ↔ ∀ p₁, g.R p₁ p → ∃ p₂, g.L p₂ p₁ ∧ Rlose_pos p₂ :=
by { rw Rlose_pos_iff, simp_rw Lwin_pos_iff }

def Lwin (g : pgame) : Prop := Lwin_pos g.start
def Rlose (g : pgame) : Prop := Rlose_pos g.start
lemma Rlose_pos_iff_Rlose_game : Rlose_pos p ↔ Rlose p.game := iff.rfl

/-- g₁ ≤ g₂ iff 0 ≤ g₂ - g₁, i.e. R loses when moving first. -/
instance : has_le pgame.{u} := { le := λ g₁ g₂, Rlose (g₂ - g₁) }

variable (p)
open add_rel
/- TODO : Rlose / Rlose_pos namespace? `↔` not conducive to dot notation. -/
/- Rlose g iff not Lwin (-g) .. Rlose (-g) iff not Lwin g -/
/- connect not_le with Lwin .. connect < with Lwin + Rlose  -/

lemma Rlose_diag : @Rlose_pos (g - g) (p, p) :=
begin
  refine g.wf.induction p (λ p ih, _),
  rw Rlose_pos_iff₂, rintro ⟨p₁,p₂⟩ (⟨_,_,_,h⟩|⟨_,_,_,h⟩),
  exacts [⟨(p₁,p₁), snd _ h, ih _ (or.inr h)⟩,
          ⟨(p₂,p₂), fst _ h, ih _ (or.inl h)⟩],
end

variables {p} {g' : pgame.{u}}
lemma Rlose_prod :
  Rlose_pos p → ∀ {p' : g'.pos}, Rlose_pos p' → @Rlose_pos (g + g') (p, p') :=
begin
  refine (tc.wf g.wf).induction p (λ p ih, _),
  refine λ hp p', (tc.wf g'.wf).induction p' (λ p' ih', _),
  intros hp', rw Rlose_pos_iff₂,
  rintro ⟨p₁,p₁'⟩ (⟨_,_,_,h⟩|⟨_,_,_,h⟩),
  { obtain ⟨p₂,hL,hl⟩ := Rlose_pos_iff₂.1 hp p₁ h,
    exact ⟨(p₂, p'), fst p' hL, ih p₂ (tc_L_R hL h) hl hp'⟩ },
  { obtain ⟨p₂,hL,hl⟩ := Rlose_pos_iff₂.1 hp' p₁' h,
    exact ⟨(p, p₂), snd p hL, ih' p₂ (tc_L_R hL h) hl⟩ },
end

variable (p)
lemma Lwin_cancel_diag : ∀ p' : g'.pos, @Lwin_pos (g' + (g - g)) (p', p, p) → Lwin_pos p' :=
begin
  refine g.wf.induction p (λ p ih, _),
  refine λ p', (tc.wf g'.wf).induction p' (λ p' ih', _),
  rw Lwin_pos_iff₂,
  rintro ⟨⟨p₁,p₂,p₃⟩,(⟨_,_,_,h⟩|⟨_,_,_,(⟨_,_,_,h⟩|⟨_,_,_,h⟩)⟩),hw⟩,
  { rw Lwin_pos_iff₂, use [p₁, h], intros p₂ h₂, apply ih',
    exacts [tc_R_L h₂ h, hw _ (fst (p, p) h₂)] },
  exacts [ih p₂ (or.inl h) p' (hw _ $ snd _ $ snd _ h),
          ih p₃ (or.inr h) p' (hw _ $ snd _ $ fst _ h)],
end

lemma Rlose_cancel_diag (p' : g'.pos) : @Rlose_pos (g' + (g - g)) (p', p, p) ↔ Rlose_pos p' :=
⟨ by { rw [Rlose_pos_iff, Rlose_pos_iff],
    exact λ h p'' h', Lwin_cancel_diag p p'' $ h (p'', p, p) (fst (p, p) h') },
  λ h, Rlose_prod h (Rlose_diag p) ⟩

end win_lose

section map
lemma comap_Rlose {g' : pgame} (f : g.pos → g'.pos)
  (hL : ∀ {p' p₂}, g'.L p' (f p₂) → ∃ p₁, p' = f p₁ ∧ g.L p₁ p₂)
  (hR : ∀ {p₁ p₂}, g.R p₁ p₂ → g'.R (f p₁) (f p₂))
  (p : g.pos) : Rlose_pos (f p) → Rlose_pos p :=
begin
  refine (tc.wf g.wf).induction p (λ p ih, _),
  rw [Rlose_pos_iff₂, Rlose_pos_iff₂],
  intros h p₂ h₂,
  obtain ⟨_, h₁, hl⟩ := h (f p₂) (hR h₂),
  obtain ⟨p₁, rfl, h⟩ := hL h₁,
  exact ⟨p₁, h, ih _ (tc_L_R h h₂) hl⟩,
end

lemma map_iso_Rlose_iff {g' : pgame} (e : g.pos ≃ g'.pos)
  (hL : ∀ {p₁ p₂}, g'.L (e p₁) (e p₂) ↔ g.L p₁ p₂)
  (hR : ∀ {p₁ p₂}, g'.R (e p₁) (e p₂) ↔ g.R p₁ p₂)
  (p : g.pos) : Rlose_pos (e p) ↔ Rlose_pos p :=
let h₁ := e.symm_apply_apply, h₂ := e.apply_symm_apply in
⟨ comap_Rlose e (λ p' _ h, ⟨e.symm p', (h₂ p').symm, hL.1 $ (h₂ p').symm ▸ h⟩) (λ _ _, hR.2) p,
  λ h, comap_Rlose e.symm (λ p' p₂ h, ⟨e p', (h₁ p').symm, (h₂ p₂).subst $ hL.2 h⟩)
    (λ p₁ p₂ h, hR.1 $ (h₂ p₂).substr $ (h₂ p₁).substr h) (e p) $ (h₁ p).symm ▸ h ⟩

end map

variables {g' g₁ g₂ : pgame.{u}} (p' : g'.pos) (p₁ : g₁.pos) (p₂ : g₂.pos)

lemma Rlose_pos_add_zero (p' : punit) : @Rlose_pos (g + 0) (p, p') ↔ Rlose_pos p :=
begin
  convert map_iso_Rlose_iff _ _ _ _,
  swap, exact (equiv.prod_punit _).symm, { ext, refl },
  iterate 2 { exact λ _ _, add_rel.punit },
end

lemma Rlose_pos_add_comm : @Rlose_pos (g + g') (p, p') ↔ @Rlose_pos (g' + g) (p', p) :=
begin
  convert map_iso_Rlose_iff _ _ _ _,
  swap, apply equiv.prod_comm, refl,
  iterate 2 { rintro ⟨_,_⟩ ⟨_,_⟩, exact add_rel.symm },
end

lemma Rlose_pos_add_assoc :
  @Rlose_pos (g + g₁ + g₂) ((p, p₁), p₂) ↔ @Rlose_pos (g + (g₁ + g₂)) (p, p₁, p₂) :=
begin
  convert map_iso_Rlose_iff _ _ _ _,
  swap, symmetry, apply equiv.prod_assoc, refl,
  iterate 2 { rintro ⟨_,_,_⟩ ⟨_,_,_⟩, exact add_rel.assoc },
end

lemma Rlose_pos_add_cycperm :
  @Rlose_pos (g + g' + (g₁ + g₂)) ((p, p'), p₁, p₂) ↔
  @Rlose_pos (g + g₁ + (g₂ + g')) ((p, p₁), p₂, p') :=
begin
  convert map_iso_Rlose_iff _ _ _ _, swap,
  { use [λ ⟨⟨a,b⟩,c,d⟩, ⟨⟨a,d⟩,b,c⟩, λ ⟨⟨a,b⟩,c,d⟩, ⟨⟨a,c⟩,d,b⟩],
    iterate 2 { exact λ ⟨⟨_,_⟩,_,_⟩, rfl } }, refl,
  iterate 2 { rintro ⟨⟨_,_⟩,_,_⟩ ⟨⟨_,_⟩,_,_⟩, exact add_rel.cycperm_iff },
end

lemma Rlose_zero : Rlose 0 := Rlose_pos_iff.2 $ λ _ h, h.elim
lemma Rlose_add (h : Rlose g) : Rlose g' → Rlose (g + g') := Rlose_prod h
lemma Rlose_sub_self : Rlose (g - g) := Rlose_diag _
lemma Rlose_cancel (g : pgame) : Rlose (g' + (g - g)) ↔ Rlose g' := Rlose_cancel_diag _ _
lemma Rlose_add_zero : Rlose (g + 0) ↔ Rlose g := Rlose_pos_add_zero _ _
lemma nonneg_iff_Rlose : 0 ≤ g ↔ Rlose g := Rlose_add_zero
lemma Rlose_add_comm : Rlose (g + g') ↔ Rlose (g' + g) := Rlose_pos_add_comm _ _
lemma Rlose_add_assoc : Rlose (g + g₁ + g₂) ↔ Rlose (g + (g₁ + g₂)) := Rlose_pos_add_assoc _ _ _
lemma Rlose_add_cycperm : Rlose (g + g' + (g₁ + g₂)) ↔ Rlose (g + g₁ + (g₂ + g')) :=
Rlose_pos_add_cycperm _ _ _ _
lemma add_le_add_iff_Rlose : g + g' ≤ g₁ + g₂ ↔ @Rlose (g₁ + g₂ + (-g + -g')) := iff.rfl

lemma neg_le_neg : -g₁ ≤ -g₂ ↔ g₂ ≤ g₁ := Rlose_add_comm
lemma neg_nonneg : 0 ≤ -g ↔ g ≤ 0 := @neg_le_neg 0 g
lemma neg_nonpos : -g ≤ 0 ↔ 0 ≤ g := @neg_le_neg _ 0
lemma sub_nonneg : 0 ≤ g - g' ↔ g' ≤ g := nonneg_iff_Rlose
lemma nonpos_iff_Rlose_neg : g ≤ 0 ↔ Rlose (-g) := neg_nonneg.symm.trans nonneg_iff_Rlose
lemma nonneg_sub_self : 0 ≤ g - g := nonneg_iff_Rlose.2 Rlose_sub_self
lemma nonpos_sub_self : g - g ≤ 0 := nonpos_iff_Rlose_neg.2 $ Rlose_add_comm.1 Rlose_sub_self

lemma le_add_Rlose (h : Rlose g') : g ≤ g' + g := Rlose_add_assoc.2 $ (Rlose_cancel g).2 h
lemma le_zero_add : g ≤ 0 + g := le_add_Rlose Rlose_zero
lemma zero_add_le : 0 + g ≤ g :=
Rlose_add_comm.1 $ Rlose_add_assoc.2 $ (Rlose_cancel (-g)).2 Rlose_zero

lemma Rlose_mono (hl : g ≤ g') (hg : Rlose g) : Rlose g' :=
(Rlose_cancel (-g)).1 $ Rlose_add_assoc.1 $ Rlose_add hl hg

lemma Rlose_add_mono (hl : g₁ ≤ g₂) (h : Rlose (g + g₁)) : Rlose (g + g₂) :=
(Rlose_cancel (-g₁)).1 $ Rlose_add_cycperm.1 $ Rlose_add h hl

lemma add_le_add_left : g + g₁ ≤ g + g₂ ↔ g₁ ≤ g₂ := add_le_add_iff_Rlose.trans $
Rlose_add_cycperm.trans $ Rlose_add_comm.trans $ (Rlose_cancel g).trans $ Rlose_add_comm

lemma le_comm : g₁ + g₂ ≤ g₂ + g₁ := Rlose_add_cycperm.1 $ (Rlose_cancel g₁).2 $ Rlose_sub_self
lemma le_assoc : g + (g₁ + g₂) ≤ g + g₁ + g₂ ∧ g + g₁ + g₂ ≤ g + (g₁ + g₂) :=
begin
  split; rw [add_le_add_iff_Rlose, Rlose_add_cycperm],
  { fapply Rlose_add_mono, exacts [-g₁,
      Rlose_add_assoc.2 $ Rlose_add_comm.1 le_comm,
      Rlose_add_assoc.2 Rlose_sub_self] },
  { exact Rlose_add_mono
      (Rlose_add_comm.1 $ Rlose_add_assoc.1 Rlose_sub_self)
      (Rlose_add_comm.1 $ Rlose_add_assoc.1 le_comm) },
end

instance : preorder pgame :=
{ le := (≤),
  le_refl := λ g, Rlose_sub_self,
  le_trans := λ _ g _ h₁ h₂,
    (Rlose_cancel g).1 $ Rlose_add_cycperm.1 $ Rlose_add h₂ $ Rlose_add_comm.1 h₁ }

/-- CGT equivalence on games. -/
instance : setoid pgame := antisymm_rel.setoid pgame (≤)

section congr

lemma neg_congr (h : g₁ ≈ g₂) : -g₁ ≈ -g₂ := ⟨neg_le_neg.2 h.2, neg_le_neg.2 h.1⟩
lemma le_congr (h₁ : g ≈ g₁) (h₂ : g' ≈ g₂) : g ≤ g' ↔ g₁ ≤ g₂ :=
⟨λ h, h₁.2.trans $ h.trans h₂.1, λ h, h₁.1.trans $ h.trans h₂.2⟩

lemma add_comm : g₁ + g₂ ≈ g₂ + g₁ := ⟨le_comm, le_comm⟩
lemma zero_add : 0 + g ≈ g := ⟨zero_add_le, le_zero_add⟩
lemma add_zero : g + 0 ≈ g := add_comm.trans zero_add
lemma add_left_neg : -g + g ≈ 0 := ⟨nonpos_sub_self, nonneg_sub_self⟩
lemma add_assoc : g + (g₁ + g₂) ≈ g + g₁ + g₂ := le_assoc
lemma add_le_add_right : g₁ + g ≤ g₂ + g ↔ g₁ ≤ g₂ :=
(le_congr add_comm add_comm).trans add_le_add_left
/- TODO : (+) and swap (+) are instances of covariant and contravariant class. -/
lemma add_left_congr : g + g₁ ≈ g + g₂ ↔ g₁ ≈ g₂ := and_congr add_le_add_left add_le_add_left
lemma add_right_congr : g₁ + g ≈ g₂ + g ↔ g₁ ≈ g₂ := and_congr add_le_add_right add_le_add_right
lemma add_congr (h₁ : g ≈ g₁) (h₂ : g' ≈ g₂) : g + g' ≈ g₁ + g₂ :=
(add_left_congr.2 h₂).trans $ add_right_congr.2 h₁

end congr

end pgame

def game := @antisymmetrization pgame (≤) _

namespace game
open quotient pgame
section
instance : ordered_add_comm_group game :=
{ zero := ⟦0⟧, 
  neg := quotient.lift (λ g, ⟦-g⟧) $ λ _ _ h, sound $ neg_congr h,
  add := quotient.lift₂ (λ g g', ⟦g + g'⟧) $ λ _ _ _ _ h₁ h₂, sound $ add_congr h₁ h₂,
  add_assoc := by { rintro ⟨⟩ ⟨⟩ ⟨⟩, exact sound pgame.add_assoc.symm },
  zero_add := by { rintro ⟨⟩, exact sound zero_add },
  add_zero := by { rintro ⟨⟩, exact sound add_zero },
  add_left_neg := by { rintro ⟨⟩, exact sound add_left_neg },
  add_comm := by { rintro ⟨⟩ ⟨⟩, exact sound add_comm },
  add_le_add_left := by { rintro ⟨⟩ ⟨⟩ h ⟨⟩, exact pgame.add_le_add_left.2 h },
  .. antisymmetrization.partial_order }
end

end game