Construct an explicit type of positions for multiplication of combinatorial games; construct a game from left and right options.

graph_mul.lean

import data.multiset.basic

universe u 

instance {α : Type*} : has_union (α → α → Prop) := ⟨λ p q x y, p x y ∨ q x y⟩
 
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)

section tree3
variable (α : Type*)

/-- Very much like `free_add_magma` but ternary instead of binary for convenience.
  Not to be confused with TREE(3). -/
inductive tree3
| single (a : α) : tree3
/- a single position in a game -/
| jux : tree3 → tree3 → tree3 → tree3
/- juxtaposition of three positions: in multiplication of pgames, the ternary juxtaposition
  xL y + x yL - xL yL is a left option of `x y`, and the three subgames correspond to
  moving in the first, second, and both games respectively. The other left and right options
  have the same form. This explains the naming `mfst, msnd, both` in `tree3.closure` below. -/

namespace tree3
variable {α}
inductive closure (r : tree3 α → tree3 α → Prop) : tree3 α → tree3 α → Prop
| move {a a'} : r a a' → closure a a'
| mfst {a a' a₂ a₃} : closure a a' → closure (jux a a₂ a₃) (jux a' a₂ a₃)
| msnd {a₁ a a' a₃} : closure a a' → closure (jux a₁ a a₃) (jux a₁ a' a₃)
| both {a₁ a₂ a a'} : closure a a' → closure (jux a₁ a₂ a) (jux a₁ a₂ a')

end tree3
end tree3

open tree3
instance (α : Type*) : has_coe α (tree3 α) := { coe := single }

inductive mul_rel (s : bool) {α β : Type*} (rα : α → α → Prop) (rβ : β → β → Prop) :
  tree3 (bool × α × β) → tree3 (bool × α × β) → Prop
/- The `bool` is the sign in front of the multiplication of two positions,
   with the convention tt = positive, ff = negative. -/
| mk {a' a b' b} : rα a' a → rβ b' b → mul_rel (jux (s,a',b) (s,a,b') (bnot s,a',b')) (s,a,b)

instance : has_mul pgame :=
{ mul := λ g₁ g₂,
  { pos := tree3 (bool × g₁.pos × g₂.pos),
    /- could potentially also work with `multiset α` or `α →₀ ℤ`
       (`multiset.to_finsupp : multiset α ≃+ (α →₀ ℕ)`)
       which may or may not be more convenient
       (ℕ doesn't have nice subtraction, ℤ needs to restrict to ≥ 0;
        counting multiplicity and forgetting the order will collapse certain moves). -/
    L := closure (mul_rel tt g₁.L g₂.L ∪ mul_rel ff g₁.L g₂.R ∪
                  mul_rel ff g₁.R g₂.L ∪ mul_rel tt g₁.R g₂.R),
    R := closure (mul_rel ff g₁.L g₂.L ∪ mul_rel tt g₁.L g₂.R ∪
                  mul_rel tt g₁.R g₂.L ∪ mul_rel ff g₁.R g₂.R),
    wf := sorry,
    start := (tt, g₁.start, g₂.start) } }


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

lemma downward_closed.acc (dc : ∀ {a b}, r b (f a) → b ∈ set.range f)
  (a : α) (ha : acc (inv_image r f) a) : acc r (f a) :=
begin
  induction ha with a ha ih,
  refine acc.intro (f a) (λ b hr, _),
  obtain ⟨a',rfl⟩ := dc hr,
  exact ih a' hr,
end

lemma inv_image_union : inv_image (r ∪ r') f = inv_image r f ∪ inv_image r' f :=
by { ext, exact iff.rfl }

end inv_image

namespace pgame
section of_L_R
variables {α β : Type u}

inductive pos_of (L : α → Type u) (R : β → Type u) : Type u
| root : pos_of
| pL {a} : L a → pos_of
| pR {b} : R b → pos_of

open pos_of

def exchange_pos_of (L : α → Type u) (R : β → Type u) :
  pos_of L R ≃ pos_of R L := by
{ iterate 2 { use λ p, pos_of.rec root (λ _, pR) (λ _, pL) p },
  iterate 2 { rintro (_|_); refl } }

variables (L : α → pgame.{u}) (R : β → pgame.{u})
abbreviation pos_of' := pos_of (pos ∘ L) (pos ∘ R)

inductive L_of : pos_of' L R → pos_of' L R → Prop
| mroot (a) : L_of (pL (L a).start) root
| mL {a p p'} : (L a).L p p' → L_of (pL p) (pL p')
| mR {b p p'} : (R b).L p p' → L_of (pR p) (pR p')

inductive R_of : pos_of' L R → pos_of' L R → Prop
| mroot (b) : R_of (pR (R b).start) root
| mL {a p p'} : (L a).R p p' → R_of (pL p) (pL p')
| mR {b p p'} : (R b).R p p' → R_of (pR p) (pR p')

lemma inv_image_L_pL (a : α) : inv_image (L_of L R) pL = (L a).L :=
by { ext, split, rintro (_|⟨_,_,_,h⟩|_), exacts [h, L_of.mL] }
lemma inv_image_L_pR (b : β) : inv_image (L_of L R) pR = (R b).L :=
by { ext, split, rintro (_|_|⟨_,_,_,h⟩), exacts [h, L_of.mR] }
lemma inv_image_R_pL (a : α) : inv_image (R_of L R) pL = (L a).R :=
by { ext, split, rintro (_|⟨_,_,_,h⟩|_), exacts [h, R_of.mL] }
lemma inv_image_R_pR (b : β) : inv_image (R_of L R) pR = (R b).R :=
by { ext, split, rintro (_|_|⟨_,_,_,h⟩), exacts [h, R_of.mR] }
lemma inv_image_pL (a : α) : inv_image (L_of L R ∪ R_of L R) pL = (L a).L ∪ (L a).R :=
by rw [inv_image_union, inv_image_L_pL, inv_image_R_pL]
lemma inv_image_pR (b : β) : inv_image (L_of L R ∪ R_of L R) pR = (R b).L ∪ (R b).R :=
by rw [inv_image_union, inv_image_L_pR, inv_image_R_pR]

def of : pgame.{u} :=
{ pos := pos_of' L R,
  start := root,
  L := L_of L R,
  R := R_of L R,
  wf := let r := L_of L R ∪ R_of L R in
  begin
    suffices accL : ∀ {a} {p : (L a).pos}, acc r (pL p),
    suffices accR : ∀ {b} {p : (R b).pos}, acc r (pR p),
    { refine ⟨λ p, acc.intro p $ _⟩, rintro (_|_),
      { rintro ((_|_)|(_|_)) }, exacts [λ _, accL, λ _, accR] },
    all_goals { intros, apply downward_closed.acc,
      { rintro _ _ ((_|_)|(_|_)); exact ⟨_, rfl⟩ } },
    { rw inv_image_pR, apply (R b).wf.apply },
    { rw inv_image_pL, apply (L a).wf.apply },
  end }

end of_L_R
end pgame