Loopy games

Stream: combinatorial-games

[Violeta Hernández]

Aaron Liu said:

Django Peeters said:

Violeta Hernández said:

(something similar applies to loopy games, we'll eventually have to define a new data type to represent those as well!)

How about a pointed, directed graph where the directed edges can only have 1 of 2 colours, where the chosen point is a vertex representing the starting position.

I have a work in progress definition of loopy games as a subquotient of countably deep u-small branching trees

[Violeta Hernández]

Do you have any Lean code? I'm interested to see how this looks.

[Aaron Liu]

I have some code

[Aaron Liu]

It's only on my local device at the moment

[Aaron Liu]

Since the class field theory workshop is over now I can start working on this again

[Aaron Liu]

So after IGame is constructed there is some API, some of which I will list out here

• IGame.leftMoves
• IGame.rightMoves
• IGame.ext
• IGame.IsOption
• IGame.IsOption.of_mem_leftMoves
• IGame.IsOption.of_mem_rightMoves
• IGame.instSmallSubtypeIsOption
• IGame.isOption_wf
• IGame.ofSets
• IGame.leftMoves_ofSets
• IGame.rightMoves_ofSets

This list of API is sufficient to characterize IGame, so that you never have to touch PGame ever again. This is because between any two types which both implement this API there exists a unique API-preserving isomorphism between them.

[Aaron Liu]

So after I make loopy games, what API should I provide which uniquely characterizes them? I'm thinking of providing a destructor and some corecursion, but this is not sufficient since you can prove an isomorphism but not the fact that it's unique.

[Violeta Hernández]

I'm still having a hard time figuring out what a loopy game even is, as a mathematical structure.

[Violeta Hernández]

The literature seems to define them in terms of graphs, but I can get not wanting to do that since it leads to some degenerate cases, such as a game 0 -> 1 -> ... -> infty where the last node isn't even accessible in finitely many moves

[Aaron Liu]

It's like a game but coinductive, right?

[Violeta Hernández]

I think so, but I don't really know how that translates in Lean

[Aaron Liu]

However it translates into Lean doesn't matter as long as you have all the API

[Aaron Liu]

The question is, what should the API be?

[Violeta Hernández]

Well, I presume we should still have left and right move sets, which should still be small, and should still satisfy extentionality

[Violeta Hernández]

I presume we would also have an ofSets constructor

[Violeta Hernández]

But we'd also need some other way to construct games which are subsequent to themselves

[Aaron Liu]

some sort of fixpoint combinator, then?

[Aaron Liu]

or corecursion like I mentioned

[Violeta Hernández]

I still don't quite understand how to construct terms in a coinductive type

[Aaron Liu]

you do it with corecursion

[Aaron Liu]

in mathlib for example we have docs#Computation.corec docs#Stream'.corec' docs#Stream'.Seq.corec docs#PFunctor.M.corec

[Aaron Liu]

oh if this is a polynomial functor then we can use what's in mathlib already

[Violeta Hernández]

I'll go take a look at that, Wikipedia really isn't helping me much

[Aaron Liu]

hold on I'm unpacking what it means to be a final coalgebra

[Aaron Liu]

maybe if this is correct we can use docs#PFunctor.M

[Aaron Liu]

I think what we actually need is M-types for quotients of polynomial functors

[Aaron Liu]

oh it's docs#QPF.Cofix

[Aaron Liu]

amazing

[Django Peeters]

Violeta Hernández said:

The literature seems to define them in terms of graphs, but I can get not wanting to do that since it leads to some degenerate cases, such as a game 0 -> 1 -> ... -> infty where the last node isn't even accessible in finitely many moves

How does it lead to that degenerate case?

[Violeta Hernández]

Well, the graph I describe is simple enough to define.

[Aaron Liu]

you have to quotient to get the right notion of equality

[Aaron Liu]

I have a half-working definition using docs#QPF.Cofix

here it is

/-
Copyright (c) 2025 Aaron Liu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Liu
-/
import Mathlib.Data.QPF.Univariate.Basic
import Mathlib.Logic.Small.Set
import Mathlib.SetTheory.Cardinal.Defs
import Mathlib.Data.Setoid.Basic

/-!
# Loopy Games

We define loopy games and prove some basic properties.
-/

universe u v

-- mathlib4 PR #27541
instance small_plift (α : Type u) [Small.{v} α] : Small.{v} (PLift α) :=
  small_map Equiv.plift

-- mathlib4 PR #27546
instance small_quot {α : Type u} [Small.{v} α] (r : α → α → Prop) : Small.{v} (Quot r) :=
  small_of_surjective Quot.mk_surjective
instance small_quotient {α : Type u} [Small.{v} α] (s : Setoid α) : Small.{v} (Quotient s) :=
  small_of_surjective Quotient.mk_surjective

instance small_succ' (α : Type u) [Small.{v} α] : Small.{v + 1} α :=
  small_lift.{u, v + 1, v} α

section

private def F : Type (u + 1) → Type (u + 1) :=
  fun X => { s : Set X × Set X // Small.{u} s.1 ∧ Small.{u} s.2 }

private local instance {α} (x : F.{u} α) : Small.{u} x.1.1 := x.2.1
private local instance {α} (x : F.{u} α) : Small.{u} x.1.2 := x.2.2

private noncomputable local instance : QPF.{u + 1, u + 1, u + 1} F where
  map f s := ⟨(f '' s.1.1, f '' s.1.2), inferInstance, inferInstance⟩
  P := {
    A := Cardinal.{u} × Cardinal.{u}
    B c := PLift c.1.out ⊕ PLift c.2.out
  }
  abs x := ⟨(Set.range (x.2 ∘ Sum.inl), Set.range (x.2 ∘ Sum.inr)), inferInstance, inferInstance⟩
  repr x := ⟨(.mk (Shrink x.1.1), .mk (Shrink x.1.2)),
    (Equiv.sumArrowEquivProdArrow _ _ _).symm
    (fun i => ((equivShrink _).symm (Cardinal.outMkEquiv i.down) :),
    fun i => ((equivShrink _).symm (Cardinal.outMkEquiv i.down) :))⟩
  abs_repr _ := Subtype.ext (Prod.ext
    ((((Equiv.plift.trans Cardinal.outMkEquiv).trans
      (equivShrink _).symm).surjective.range_comp _).trans Subtype.range_coe)
    ((((Equiv.plift.trans Cardinal.outMkEquiv).trans
      (equivShrink _).symm).surjective.range_comp _).trans Subtype.range_coe))
  abs_map f x := Subtype.ext (Prod.ext
    (Set.range_comp f (x.2 ∘ Sum.inl)) (Set.range_comp f (x.2 ∘ Sum.inr)))

def LGame := QPF.Cofix F.{u}

namespace LGame

def leftMoves (x : LGame.{u}) : Set LGame.{u} := x.dest.1.1
def rightMoves (x : LGame.{u}) : Set LGame.{u} := x.dest.1.2
instance small_leftMoves (x : LGame.{u}) : Small.{u} (leftMoves x) := x.dest.2.1
instance small_rightMoves (x : LGame.{u}) : Small.{u} (rightMoves x) := x.dest.2.2

theorem eq_of_bisim (r : LGame → LGame → Prop)
    (leftMoves : ∀ x y, r x y → ∃ e : leftMoves x ≃ leftMoves y, ∀ i, r i.1 (e i).1)
    (rightMoves : ∀ x y, r x y → ∃ e : rightMoves x ≃ rightMoves y, ∀ i, r i.1 (e i).1)
    (x y : LGame.{u}) (hxy : r x y) : x = y := by
  refine QPF.Cofix.bisim r (fun x y hxy => ?_) x y hxy
  obtain ⟨el, hel⟩ := leftMoves x y hxy
  obtain ⟨er, her⟩ := rightMoves x y hxy
  refine ⟨⟨(Set.range fun i => ⟨(i.1, (el i).1), hel i⟩,
    Set.range fun i => ⟨(i.1, (er i).1), her i⟩), inferInstance, inferInstance⟩, ?_, ?_⟩
  · apply Subtype.ext
    apply Prod.ext
    · apply (Set.range_comp _ _).symm.trans
      simp [Function.comp_def, LGame.leftMoves]
    · apply (Set.range_comp _ _).symm.trans
      simp [Function.comp_def, LGame.rightMoves]
  · apply Subtype.ext
    apply Prod.ext
    · apply (Set.range_comp _ _).symm.trans
      apply (Set.range_comp Subtype.val el).trans
      simp [LGame.leftMoves]
    · apply (Set.range_comp _ _).symm.trans
      apply (Set.range_comp Subtype.val er).trans
      simp [LGame.rightMoves]

@[ext]
protected theorem ext {x y : LGame.{u}}
    (leftMoves : x.leftMoves = y.leftMoves)
    (rightMoves : x.rightMoves = y.rightMoves) : x = y :=
  eq_of_bisim
    (fun i j => i.leftMoves = j.leftMoves ∧ i.rightMoves = j.rightMoves)
    (fun _ _ hij => hij.left ▸ ⟨.refl _, fun _ => ⟨rfl, rfl⟩⟩)
    (fun _ _ hij => hij.right ▸ ⟨.refl _, fun _ => ⟨rfl, rfl⟩⟩)
    x y ⟨leftMoves, rightMoves⟩

section corec
variable {α : Type v} (leftMoves : α → Set α) (rightMoves : α → Set α)
  [∀ a, Small.{u} (leftMoves a)] [∀ a, Small.{u} (rightMoves a)] (init : α)

private inductive reachable : Nat → α → Type v where
  | init : reachable 0 init
  | ofLeftMoves (x y : α) {n : Nat}
    (hx : x ∈ leftMoves y) (hy : reachable n y) : reachable (n + 1) x
  | ofRightMoves (x y : α) {n : Nat}
    (hx : x ∈ rightMoves y) (hy : reachable n y) : reachable (n + 1) x

private def T : Type v := { a : α // ∃ n, Nonempty (reachable leftMoves rightMoves init n a) }

private local instance small_reachable (n : Nat) :
    Small.{u} (Sigma (reachable leftMoves rightMoves init n)) := by
  induction n with
  | zero =>
    suffices _ : Subsingleton (Sigma (reachable leftMoves rightMoves init 0)) from inferInstance
    constructor
    intro ⟨la, ra⟩ ⟨lb, rb⟩
    cases ra
    cases rb
    rfl
  | succ n ih =>
    suffices equiv : Sigma (reachable leftMoves rightMoves init (n + 1)) ≃
      (s : Sigma (reachable leftMoves rightMoves init n)) ×
        (leftMoves s.1 ⊕ rightMoves s.1) from small_map equiv
    exact {
      toFun
      | ⟨.(x), .ofLeftMoves x y hx hy⟩ => ⟨⟨y, hy⟩, .inl ⟨x, hx⟩⟩
      | ⟨.(x), .ofRightMoves x y hx hy⟩ => ⟨⟨y, hy⟩, .inr ⟨x, hx⟩⟩
      invFun
      | ⟨⟨y, hy⟩, .inl ⟨x, hx⟩⟩ => ⟨x, .ofLeftMoves x y hx hy⟩
      | ⟨⟨y, hy⟩, .inr ⟨x, hx⟩⟩ => ⟨x, .ofRightMoves x y hx hy⟩
      left_inv
      | ⟨.(x), .ofLeftMoves x y hx hy⟩ => rfl
      | ⟨.(x), .ofRightMoves x y hx hy⟩ => rfl
      right_inv
      | ⟨⟨y, hy⟩, .inl ⟨x, hx⟩⟩ => rfl
      | ⟨⟨y, hy⟩, .inr ⟨x, hx⟩⟩ => rfl
    }

private local instance small_T : Small.{u} (T leftMoves rightMoves init) := by
  suffices equiv : T leftMoves rightMoves init ≃
    @Quotient ((n : Nat) × Sigma (reachable leftMoves rightMoves init n))
      (Setoid.comap (fun i => i.snd.fst) ⊥) from small_map equiv
  refine Equiv.trans ?_ (Setoid.comapQuotientEquiv _ ⊥).symm
  refine Equiv.trans ?_ (Equiv.setCongr (Set.range_comp Quotient.mk'' _)).symm
  refine Equiv.trans ?_ (Equiv.Set.image Quotient.mk'' _ fun _ _ => Quotient.exact)
  exact Equiv.subtypeEquivRight (by simp)

section
omit [∀ a, Small.{u, v} (leftMoves a)] [∀ a, Small.{u, v} (rightMoves a)]

private theorem left_map (x : T leftMoves rightMoves init) (i : α) (hi : i ∈ leftMoves x.1) :
    ∃ n, Nonempty (reachable leftMoves rightMoves init n i) :=
  x.2.elim fun n hn => hn.elim fun r =>
      ⟨n + 1, ⟨.ofLeftMoves i x.1 hi r⟩⟩

private theorem right_map (x : T leftMoves rightMoves init) (i : α) (hi : i ∈ rightMoves x.1) :
    ∃ n, Nonempty (reachable leftMoves rightMoves init n i) :=
  x.2.elim fun n hn => hn.elim fun r =>
      ⟨n + 1, ⟨.ofRightMoves i x.1 hi r⟩⟩
end

private def T_coeval (x : Shrink.{u + 1} (T leftMoves rightMoves init)) :
    F (Shrink.{u + 1} (T leftMoves rightMoves init)) :=
  have x := (equivShrink _).symm x
  ⟨(equivShrink _ '' (Subtype.map id (left_map leftMoves rightMoves init x) ''
      @Set.univ (leftMoves x.1)),
    (equivShrink _ '' (Subtype.map id (right_map leftMoves rightMoves init x) ''
      @Set.univ (rightMoves x.1)))),
    inferInstance, inferInstance⟩

private noncomputable def T_initi {n : Nat} {i : α} (r : reachable leftMoves rightMoves init n i) :
    Shrink.{u + 1} (T leftMoves rightMoves init) :=
  equivShrink _ ⟨i, n, ⟨r⟩⟩

private noncomputable def T_init : Shrink.{u + 1} (T leftMoves rightMoves init) :=
  T_initi leftMoves rightMoves init .init

noncomputable def coreci (i : Shrink.{u + 1} (T leftMoves rightMoves init)) : LGame.{u} :=
  QPF.Cofix.corec (T_coeval leftMoves rightMoves init) i

noncomputable def corec : LGame :=
  coreci leftMoves rightMoves init (T_init leftMoves rightMoves init)

private theorem coreci_initi_irrel {n m : Nat} {i j : α}
    (r : reachable leftMoves rightMoves i n init)
    (s : reachable leftMoves rightMoves j m init):
    coreci leftMoves rightMoves i (T_initi leftMoves rightMoves i r) =
      coreci leftMoves rightMoves j (T_initi leftMoves rightMoves j s) := by
  refine eq_of_bisim
    (fun x y => ∃ n m o,
      ∃ (r : reachable leftMoves rightMoves i n o)
        (s : reachable leftMoves rightMoves j m o),
      coreci leftMoves rightMoves i (T_initi leftMoves rightMoves i r) = x ∧
      coreci leftMoves rightMoves j (T_initi leftMoves rightMoves j s) = y)
    (fun x y hxy => ?_)
    (fun x y hxy => ?_)
    (coreci leftMoves rightMoves i (T_initi leftMoves rightMoves i r))
    (coreci leftMoves rightMoves j (T_initi leftMoves rightMoves j s))
    ⟨n, m, init, r, s, rfl, rfl⟩ <;> obtain ⟨n, m, o, r, s, rfl, rfl⟩ := hxy
  · rw [coreci, coreci, LGame.leftMoves, LGame.leftMoves,
      QPF.Cofix.dest_corec, QPF.Cofix.dest_corec]
    dsimp only [Functor.map]
    sorry
  · sorry

[Violeta Hernández]

I'm still struggling to understand what a "polynomial functor" is

[Aaron Liu]

it's a sum of products

[Violeta Hernández]

Aaron Liu said:

you have to quotient to get the right notion of equality

Oh you're right, the graph I describe would just be equivalent to the game x = {x | x}, right? I think the magic word is bisimulation?

[Aaron Liu]

yes that's the word

[Aaron Liu]

Violeta Hernández said:

I'm still struggling to understand what a "polynomial functor" is

The example I gave to Jovan Gerbscheid is the list functor, it looks like () ⊕ α ⊕ α × α ⊕ α × α × α ⊕ ... where the nth component of the sum is n-length lists

[Aaron Liu]

this is the same as Fin 0 → α ⊕ Fin 1 → α ⊕ Fin 2 → α ⊕ ..., which is (n : Nat) × (Fin n → α)

[Aaron Liu]

polynomial functors are ones that look like P α = (a : A) × (B a → α)

[Aaron Liu]

for lists you have A := Nat and B := Fin

[Violeta Hernández]

Well, in that case, I think the simplest way to construct an arbitrary loopy game is something like

def mk {a : Type u} (l : a -> a -> Prop) (r : a -> a -> Prop) (x : a) : LGame.{u} :=
  sorry

theorem leftMoves_mk {a l r x} : (mk l r a).leftMoves = leftMoves '' {y | l y x} :=
  sorry

theorem rightMoves_mk {a l r x} : (mk l r a).rightMoves = rightMoves '' {y | r y x} :=
  sorry

[Aaron Liu]

90% sure this allows you to construct the loopy game with options all loopy games not subsequent to themselves

[Violeta Hernández]

LGame.{u} : Type (u + 1) so there shouldn't be any Bertrand nonsense

[Aaron Liu]

oh you're taking a : Type u

[Aaron Liu]

not sure that's a good idea but it does make everything a lot simpler

[Violeta Hernández]

I think the correct thing to do is take Small.{u} a

[Aaron Liu]

that also works

[Aaron Liu]

neither of those lets you define ofSets very easily though

[Aaron Liu]

I'm trying to do a version where you have

variable {α : Type v} (leftMoves : α → Set α) (rightMoves : α → Set α)
  [∀ a, Small.{u} (leftMoves a)] [∀ a, Small.{u} (rightMoves a)] (init : α)

[Aaron Liu]

it's a bit tricky

[Aaron Liu]

I think the problem is not enough stuff in mathlib

[Violeta Hernández]

Take two small sets, build the sigma type of subpositions, and I think that should work?

[Aaron Liu]

explain "the sigma type of subpositions"

[Violeta Hernández]

Not a sigma type, sorry. Let me write this down.

[Aaron Liu]

good luck

[Violeta Hernández]

Take s and t small. The type Option (Subpositions s U Subpositions t) is small, and you can define left move and right move relations on some x in the obvious way, and on none so that it relates to the games in s and t. Then mk l r none should be what you want.

[Aaron Liu]

you will have to be a bit more explicit than that

[Aaron Liu]

how do I get s and t

[Aaron Liu]

how do I prove the left and right moves of this is correct

[Violeta Hernández]

Those are the sets you input into ofSets

[Violeta Hernández]

I'm struggling to write on my cellphone, let me go to my laptop

[Django Peeters]

Violeta Hernández said:

Well, the graph I describe is simple enough to define.

I'm not sure how to make a graph from this. What game do you mean?

[Aaron Liu]

Violeta Hernández said:

The literature seems to define them in terms of graphs, but I can get not wanting to do that since it leads to some degenerate cases, such as a game 0 -> 1 -> ... -> infty where the last node isn't even accessible in finitely many moves

I think infty is actually isolated here

[Django Peeters]

Also, do you mean degenerate because a normal game is also a loopy game? Or do we want those to be disjoint?

[Violeta Hernández]

def Subposition (x y : LGame.{u}) : Prop := sorry
private def Subpositions (x : LGame.{u}) : Set LGame.{u} := insert x {y | Subposition y x}
instance (x : LGame.{u}) : Small.{u} (Subpositions x) := sorry

def ofSets (s t : Set LGame.{u}) [Small.{u} s] [Small.{u} t] : LGame.{u} :=
  let α := Option (⋃₀ (Subpositions '' (s ∪ t)))
  have : Small.{u} α := sorry
  let l : α → α → Prop := fun x y ↦ match x y with
  | _, none => False
  | none, some x => x ∈ s
  | some x, some y => x ∈ y.leftMoves
  let r : α → α → Prop := fun x y ↦ match x y with
  | _, none => False
  | none, some x => x ∈ t
  | some x, some y => x ∈ y.rightMoves
  mk l r none

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

The literature seems to define them in terms of graphs, but I can get not wanting to do that since it leads to some degenerate cases, such as a game 0 -> 1 -> ... -> infty where the last node isn't even accessible in finitely many moves

I think infty is actually isolated here

You're right, it is. I should be more careful with notation!

[Violeta Hernández]

Or in other words, the directed graph on ENat relating n with n + 1 for n : ℕ has no incoming edges on ⊤.

[Aaron Liu]

Violeta Hernández said:

def Subposition (x y : LGame.{u}) : Prop := sorry
private def Subpositions (x : LGame.{u}) : Set LGame.{u} := insert x {y | Subposition y x}
instance (x : LGame.{u}) : Small.{u} (Subpositions x) := sorry

def ofSets (s t : Set LGame.{u}) [Small.{u} s] [Small.{u} t] : LGame.{u} :=
  let α := Option (⋃₀ (Subpositions '' (s ∪ t)))
  have : Small.{u} α := sorry
  let l : α → α → Prop := fun x y ↦ match x y with
  | _, none => False
  | none, some x => x ∈ s
  | some x, some y => x ∈ y.leftMoves
  let r : α → α → Prop := fun x y ↦ match x y with
  | _, none => False
  | none, some x => x ∈ t
  | some x, some y => x ∈ y.rightMoves
  mk l r none

this looks like it might actually work

[Violeta Hernández]

Aaron Liu said:

I'm trying to do a version where you have

variable {α : Type v} (leftMoves : α → Set α) (rightMoves : α → Set α)
  [∀ a, Small.{u} (leftMoves a)] [∀ a, Small.{u} (rightMoves a)] (init : α)

This is a generalization of what I'm doing, but I'm a bit skeptical that we'll ever have a situation where we want to construct a small game tree out of a type that isn't.

[Aaron Liu]

I will use it to define mk

[Aaron Liu]

and ofSets

[Violeta Hernández]

I think you might be able to do it the other way around

[Violeta Hernández]

Given these functions, you can construct the set of all games accessible from init from leftMoves and rightMoves, and it should be Small

[Violeta Hernández]

Then you can just use mk on that subtype

[Aaron Liu]

yes but I haven't defined mk yet so I'm using to corecursor directly

[Aaron Liu]

now I'm thinking maybe not the best idea

[Violeta Hernández]

I was thinking mk might be a bit easier to define than your map

[Aaron Liu]

but I can still see the same problem

[Aaron Liu]

that is proving that mk on the subtype corresponds to mk on the other subtype

[Violeta Hernández]

What do you mean?

[Aaron Liu]

when you do the thing where you restrict to the subtype of games accessible from init

[Aaron Liu]

you would like to prove that mk on the subtype of elements accessible from init fed with a l is the same as mk on the subtype of elements accessible from l fed with a l

[Aaron Liu]

I'm currently trying to figure out the best generality to state this in that makes it the easiest to prove

[Violeta Hernández]

I don't think you actually need to prove that?

[Violeta Hernández]

You should have extensionality on LGame

[Aaron Liu]

the extensionality is stated in terms of bisimulation

[Violeta Hernández]

If x.leftMoves = y.leftMoves and x.rightMoves = y.rightMoves then x = y

[Violeta Hernández]

I mean, this is true, as is the bisimulation thing

[Aaron Liu]

I do have that version

[Aaron Liu]

but you can't prove x.leftMoves = y.leftMoves

[Aaron Liu]

unless you have a way?

[Violeta Hernández]

So if you can prove leftMoves (ofSets s t) = s and rightMoves (ofSets s t) = t then that should be enough to prove the definition is correct

[Violeta Hernández]

Or do I misunderstand the issue?

[Aaron Liu]

the issue is that you can't use ofSets to construct loopy games that are subpositions of themselves

[Aaron Liu]

you need another constructor

[Violeta Hernández]

Oh yeah, I know that

[Violeta Hernández]

These are two separate constructors

[Aaron Liu]

what's the other constructor

[Violeta Hernández]

Either (or both!) versions of mk

[Aaron Liu]

the issue is proving the defining equations for mk

[Violeta Hernández]

ofSets is a convenience constructor built on top of it

[Violeta Hernández]

In practice I imagine ofSets as well as dud, on, off can already describe most games of interest

[Violeta Hernández]

Aaron Liu said:

the issue is proving the defining equations for mk

I think there's two different types at play here. We should first define some auxiliary type (PLGame?) as the coinductive type with constructor mk (a : Type u) (f : a -> PLGame) : PLGame. Then you can quotient over identity to get LGame, which should satisfy extentionality as well as a coinduction principle.

[Aaron Liu]

that's a bad idea

[Aaron Liu]

well, not a bad idea but inefficient since I can directly go to LGame without having to pass through PLGame

[Aaron Liu]

and I've proved extensionality and bisimulation but coinduction is tricky

[Aaron Liu]

and it won't get any easier if I go to PLGame since I don't get anything new there

[Violeta Hernández]

How did you define LGame without PLGame?

[Aaron Liu]

Using QPF.Cofix

[Violeta Hernández]

Huh, now I'm wondering if there's some way to define IGame without PGame using functor shenanigans

[Aaron Liu]

I prove that fun X => { s : Set X × Set X // Small.{u} s.1 ∧ Small.{u} s.2 } with the obvious map is the quotient of a polynomial functor

[Aaron Liu]

Violeta Hernández said:

Huh, now I'm wondering if there's some way to define IGame without PGame using functor shenanigans

it's almost certainly just the dual (fixpoint instead of cofixpoint)

[Violeta Hernández]

Add that to do the TODO list!

[Violeta Hernández]

Aaron Liu said:

I prove that fun X => { s : Set X × Set X // Small.{u} s.1 ∧ Small.{u} s.2 } with the obvious map is the quotient of a polynomial functor

Does quotient here mean the type has the extensional form of equality?

[Aaron Liu]

actually not quite

[Aaron Liu]

the polynomial functor in question is (c : Cardinal.{u} × Cardinal.{u}) × ((PLift c.1.out ⊕ PLift c.2.out) → α) with the obvious map

[Aaron Liu]

and the quotient part mean that tuples are identified when they have all the same entries, and you ignore the order and multiplicity of the entries

[Aaron Liu]

it does turn out to give you the correct extensionality

[Violeta Hernández]

Interesting!

[Aaron Liu]

it has occurred to me that I could do this without Cardinal

[Aaron Liu]

and just use types

[Aaron Liu]

and then the polynomial functor will be the same as the one defining PGame and the quotient will be the same as PGame.Identical

[Violeta Hernández]

So just to conceptualize this, the functor Finset would be the quotient of the polynomial functor (a : Nat) x Fin a, right?

[Aaron Liu]

that's not a functor

[Aaron Liu]

that's just a type

[Aaron Liu]

I've been making my types into functors by abstracting over α in a covariant way

[Aaron Liu]

you don't have an α

[Violeta Hernández]

Oh yeah would it be (n : Nat) x Fin n -> a then

[Aaron Liu]

yes that's correct

[Aaron Liu]

it's a quotient of lists by the relation "contains all the same elements"

[Aaron Liu]

so you've built lists

[Violeta Hernández]

Isn't it finsets, rather?

[Aaron Liu]

well fun α => (n : ℕ) × (Fin n → α) looks like the list functor to me

[Violeta Hernández]

Oh yeah, I mean that lists quotiented by containing the same elements are what finsets are

[Aaron Liu]

yes that's correct

[Violeta Hernández]

Interesting! So then you can define inductive and coinductive types from this polynomial functor, right?

[Aaron Liu]

if you take the fixpoint you get hereditarily finite sets

[Violeta Hernández]

And the cofixpoint would be... hereditarily finite non-well-founded sets?

[Aaron Liu]

I guess that's one way to think about it

[Aaron Liu]

they're not really finite anymore

[Aaron Liu]

they're finitely branching

[Violeta Hernández]

I think they should still be finite, though

[Aaron Liu]

they be related to infinitely many distinct elements under the relation "transitive closure of membership"

[Violeta Hernández]

A quine a = {a} would only be related to itself

[Violeta Hernández]

(deleted)

[Aaron Liu]

use a = {0, {1, {2, {3, {4, {5, ...

[Aaron Liu]

a tower of pairs

[Aaron Liu]

but all distinct

[Violeta Hernández]

Whoa

[Violeta Hernández]

Wait, follow-up question

[Violeta Hernández]

Say you defined the coinductive type of the functor fun a => (n : ENat) x (toType n -> a) where ENat.toType is Fin n for a natural and Nat for top

[Violeta Hernández]

Would it be correct to call these sets hereditarily countable?

[Violeta Hernández]

Or do you run into the same issue?

[Aaron Liu]

since the cofinality of ℵ₁ is ω₁ which is uncountable

[Aaron Liu]

I think these are "hereditarily countable"

[Violeta Hernández]

Basically I'm just trying to tune my intuition for the case fun a => (b : Type u) x (b -> a)

[Django Peeters]

Violeta Hernández said:

Or in other words, the directed graph on ENat relating n with n + 1 for n : ℕ has no incoming edges on ⊤.

Thank you very much! That is indeed a clear degenerate case... I'm gonna try to refine my definition.

[Aaron Liu]

have you seen docs#WType

[Violeta Hernández]

And by extension fun a => (b c : Type u) x (b -> c -> a) which is I think what games are

[Violeta Hernández]

I've worked with W-types, yes

[Violeta Hernández]

I haven't worked with the dual M types though

[Violeta Hernández]

Django Peeters said:

Violeta Hernández said:

Or in other words, the directed graph on ENat relating n with n + 1 for n : ℕ has no incoming edges on ⊤.

Thank you very much! That is indeed a clear degenerate case... I'm gonna try to regine my definition.

I'm pretty sure the game I describe is equivalent (through bisimulation) to the game where top doesn't exist at all

[Violeta Hernández]

So it's not really a degenerate case at all

[Violeta Hernández]

I might be getting ahead of myself, but I'd love to see a Functor file in the repository, where we prove that fun α ↦ {s : Set α × Set α // Small.{u} s.1 ∧ Small.{u} s.2} is a QPF. Then we could define IGame := QPF.fix and LGame := QPF.cofix and hopefully skip a lot of setup in both cases!

[Aaron Liu]

we could try that

[Violeta Hernández]

(I imagine a similar approach might be helpful for docs#ZFSet but I also imagine there are other computability concerns in that case)

[Violeta Hernández]

I'll try to reprove QPF F as a bit of a personal excercise

[Violeta Hernández]

How's this?

def GameFunctor : Type (u + 1) → Type (u + 1) :=
  fun α => {s : Set α × Set α // Small.{u} s.1 ∧ Small.{u} s.2}

namespace GameFunctor

@[ext] theorem ext {α : Type (u + 1)} {x y : GameFunctor α} : x.1 = y.1 → x = y := Subtype.ext

instance {α : Type (u + 1)} (x : GameFunctor α) : Small.{u} x.1.1 := x.2.1
instance {α : Type (u + 1)} (x : GameFunctor α) : Small.{u} x.1.2 := x.2.2

instance : Functor GameFunctor where
  map f s := ⟨⟨f '' s.1.1, f '' s.1.2⟩, ⟨inferInstance, inferInstance⟩⟩

noncomputable instance : QPF GameFunctor where
  P := ⟨Type u × Type u, fun x ↦ PLift x.1 ⊕ PLift x.2⟩
  abs x := ⟨⟨Set.range (x.2 ∘ .inl ∘ PLift.up), Set.range (x.2 ∘ .inr ∘ PLift.up)⟩,
    ⟨inferInstance, inferInstance⟩⟩
  repr x := ⟨⟨Shrink x.1.1, Shrink x.1.2⟩,
    Sum.rec (fun y ↦ ((equivShrink _).symm y.1).1) (fun y ↦ ((equivShrink _).symm y.1).1)⟩
  abs_repr x := by ext <;> simp [← (equivShrink _).exists_congr_right]
  abs_map f := by intro ⟨x, f⟩; ext <;> simp [PFunctor.map, Functor.map]
  __ := instFunctor

end GameFunctor

[Violeta Hernández]

I think this golfs your code a bit :slight_smile:

[Aaron Liu]

It golfs it quite a lot

[Aaron Liu]

never mind it's barely shorter

[Aaron Liu]

since you made it structured

[Violeta Hernández]

I would not like to see this written down using only angle brackets

[Violeta Hernández]

A few thoughts in my head:

• It would be nice if someone went through the QPF file and added private to everything that isn't the inductive/coinductive principles, it would really cut down on noise.
• Apparently the notion of a QPF was introduced by members of the Zulip at a conference in 2019? That's awesome.

[Violeta Hernández]

I'll give this a read: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.6

[Violeta Hernández]

You never never in a million years would I have guessed that I'd be reading category theory in order to formalize game theory of all things

[Aaron Liu]

it's the initial and final algebras

[Violeta Hernández]

I'm flabbergasted to learn that inductive types boil down to a commutative square

[Violeta Hernández]

I've been staring at commutative diagrams for about half an hour I think I finally get this

[Violeta Hernández]

So IGame is the initial algebra of the functor F(α) = SmallSet α × SmallSet α and LGame is the terminal coalgebra of the same functor

[Violeta Hernández]

The QPF machinery is really only there to guarantee that these algebras/coalgebras exist and to construct them

[Violeta Hernández]

On a related note, surely docs#PFunctor.Approx.Agree.continu is a typo

[Aaron Liu]

Well I've proved the left and right moves of corec are correct

[Aaron Liu]

now I guess I build ofSets?

[Violeta Hernández]

That makes sense

[Aaron Liu]

ok ofSets is done

[Aaron Liu]

is there anything else I might be missing

[Violeta Hernández]

Did you manage to build anything similar to the mk graph constructor from earlier?

[Aaron Liu]

yeah

[Aaron Liu]

it's corec

[Aaron Liu]

if you abuse the defeq between Set X and X → Prop

[Violeta Hernández]

We should maybe not do that

[Violeta Hernández]

But if you have some version of that then it's fine

[Violeta Hernández]

Btw, I'm currently working on redefining IGame as a QPF.Fix. I think we could start there, then PR the definition of LGame as QPF.Cofix.

[Violeta Hernández]

It would inform the API a bit better

[Aaron Liu]

I made vihdzp/combinatorial-games#156 so you can see my code

[Violeta Hernández]

Something I find peculiar is that the recursor for IGame seems... not very useful? This is what you get if you directly use docs#QPF.Fix.rec

def rec {α : Type (u + 1)}
    (g : ∀ (s t : Set α) [Small.{u} s] [Small.{u} t], α) : IGame → α :=
  QPF.Fix.rec fun x ↦ g x.1.1 x.1.2

The fact that α is limited to Type (u + 1) really limits what you can do with this. I found it easier to instead go the long way around and prove WellFounded IsOption, at which point well-founded recursion gives you a much better recursor.

[Aaron Liu]

yeah I'm pretty sure those can be generalized to arbitrary universes

[Violeta Hernández]

Aaron Liu said:

I made vihdzp/combinatorial-games#156 so you can see my code

I just opened https://github.com/vihdzp/combinatorial-games/pull/157 which defines GameFunctor and uses it to completely get rid of PGame.

[Violeta Hernández]

I think you should merge my PR into yours

[Violeta Hernández]

@Aaron Liu Is there ever a circumstance where you'd use eq_of_bisim over the extensionality principle? Like, what kind of a relation r could you put into the theorem that isn't just equality?

[Violeta Hernández]

I might be misunderstanding how bisimulations are used

[Aaron Liu]

How would you prove that forall f : α → α and x : α, corec (fun i => {f i}) (fun i => {f i}) x is equal to corec (fun _ => {()}) (fun _ => {()}) ()

[Violeta Hernández]

Oh I see, extensionality alone doesn't cut it

[Violeta Hernández]

Wait, let me translate into plaintext. Does that mean that the game x = {x | x} is equal to every game yᵢ where yᵢ = {y₁, ... yₙ | y₁, ... yₙ}?

[Aaron Liu]

I am 70% sure that out of the two theorems eq_of_bisim and hom_unique in my PR, they are both enough for extensionality and you can prove either one from the other

[Aaron Liu]

Violeta Hernández said:

Wait, let me translate into plaintext. Does that mean that the game x = {x | x} is equal to every game yᵢ where yᵢ = {y₁, ... yₙ | y₁, ... yₙ}?

I think so? If I'm understanding what you mean correctly

[Aaron Liu]

both of those play out as $\bold{dud}$

[Violeta Hernández]

Yeah, and if you tried to prove it with extensionality you'd get the exact same result you're trying to prove!

[Violeta Hernández]

But how do you prove this using a bisimulation?

[Aaron Liu]

you have to encode "this game is dud" into a relation

[Violeta Hernández]

Let me try

[Violeta Hernández]

Wait

[Violeta Hernández]

If you assume yᵢ = {y₁, ... yₙ | y₁, ... yₙ} for all i then yᵢ = yⱼ by extensionality

[Aaron Liu]

yes

[Violeta Hernández]

So really all you're trying to prove is that any two games with x = {x | x} are equal

[Aaron Liu]

yes

[Violeta Hernández]

But I can see how that can't be proven by extensionality

[Violeta Hernández]

I still don't quite see how to prove it by bisimulation, though.

[Aaron Liu]

theorem dud_eq (x y : LGame.{u})
    (hx : x = .ofSets {x} {x}) (hy : y = .ofSets {y} {y}) : x = y := by
  refine LGame.eq_of_bisim
    (fun i j => i = LGame.ofSets.{u} {i} {i} ∧ j = LGame.ofSets.{u} {j} {j})
    (fun x y hxy => ?_) (fun x y hxy => ?_) x y ⟨hx, hy⟩
  · rw [hxy.left, hxy.right, LGame.leftMoves_ofSets, LGame.leftMoves_ofSets]
    refine ⟨(Equiv.Set.singleton.{0} x).trans (Equiv.Set.singleton.{0} y).symm, fun i => ?_⟩
    obtain ⟨x, rfl⟩ := i
    simpa [Equiv.Set.singleton] using hxy
  · rw [hxy.left, hxy.right, LGame.rightMoves_ofSets, LGame.rightMoves_ofSets]
    refine ⟨(Equiv.Set.singleton.{0} x).trans (Equiv.Set.singleton.{0} y).symm, fun i => ?_⟩
    obtain ⟨x, rfl⟩ := i
    simpa [Equiv.Set.singleton] using hxy

[Aaron Liu]

tada

[Aaron Liu]

bisimulation

[Violeta Hernández]

Ohhh wait I get my confusion

[Violeta Hernández]

I was reading the definition of coinduction rather than bisimulation

[Violeta Hernández]

No wonder I was confused

[Violeta Hernández]

So bisimulation for loopy games tells you that if you have a relation on loopy games such that when x and y are related... There's a pairing between left options of x and left options of y so that every pair is related, and likewise for right options? Then r x y implies x = y.

[Violeta Hernández]

I guess one way to think about this is that the existence of such a relation allows you to build an isomorphism between game trees

[Violeta Hernández]

If r x y then there's a pairing between options of x and y, which means the game trees up to depth one are isomorphic. Then there must also be a pairing between the corresponding options of those options, which means the game tree up to depth two are isomorphic. And so on.

[Violeta Hernández]

Aaron Liu said:

theorem dud_eq (x y : LGame.{u})
    (hx : x = .ofSets {x} {x}) (hy : y = .ofSets {y} {y}) : x = y := by
  refine LGame.eq_of_bisim
    (fun i j => i = LGame.ofSets.{u} {i} {i} ∧ j = LGame.ofSets.{u} {j} {j})
    (fun x y hxy => ?_) (fun x y hxy => ?_) x y ⟨hx, hy⟩
  · rw [hxy.left, hxy.right, LGame.leftMoves_ofSets, LGame.leftMoves_ofSets]
    refine ⟨(Equiv.Set.singleton.{0} x).trans (Equiv.Set.singleton.{0} y).symm, fun i => ?_⟩
    obtain ⟨x, rfl⟩ := i
    simpa [Equiv.Set.singleton] using hxy
  · rw [hxy.left, hxy.right, LGame.rightMoves_ofSets, LGame.rightMoves_ofSets]
    refine ⟨(Equiv.Set.singleton.{0} x).trans (Equiv.Set.singleton.{0} y).symm, fun i => ?_⟩
    obtain ⟨x, rfl⟩ := i
    simpa [Equiv.Set.singleton] using hxy

Can't you do this more directly by defining r a b as a = x and b = y?

[Violeta Hernández]

@Aaron Liu I think all the stuff you did with reachable can be done much more simply using Relation.ReflTransGen.

[Violeta Hernández]

I just PR'd the theorem that subpositions of an IGame are a small set in #159. As a corollary, we can do this:

private def T : Type v :=
  {a : α // Relation.ReflTransGen (fun x y ↦ x ∈ leftMoves y ∪ rightMoves y) a init}

private local instance small_T : Small.{u} (T leftMoves rightMoves init) :=
  small_setOf_reflTransGen' ..

[Violeta Hernández]

I'll rebuild the coinduction principle with this, I think it should be quite a bit easier

[Violeta Hernández]

This is going well. I'll continue golfing tomorrow.

[Aaron Liu]

are you done for today?

[Violeta Hernández]

Yeah

[Violeta Hernández]

@Aaron Liu Hi! Just finished refactoring your PR. I think I did a pretty decent job at cleaning up the definition of corecursion; I also added some basic results on on, off, and dud to test out our new definitions.

https://github.com/vihdzp/combinatorial-games/pull/160

[Aaron Liu]

I guess if you do it for me then I don't have to do it myself

[Aaron Liu]

thanks

[Aaron Liu]

it feels like my PRs are only there so you can golf them and open another one

[Violeta Hernández]

I think we make a good team

[Violeta Hernández]

Aaron Liu said:

So after I make loopy games, what API should I provide which uniquely characterizes them? I'm thinking of providing a destructor and some corecursion, but this is not sufficient since you can prove an isomorphism but not the fact that it's unique.

It's a bit late, but I think I have an answer to this:

• LGame.leftMoves
• LGame.rightMoves
• LGame.instSmallLeftMoves
• LGame.instSmallRightMoves
• LGame.ofSets
• LGame.leftMoves_ofSets
• LGame.rightMoves_ofSets
• LGame.eq_of_bisim
• LGame.corec
• LGame.leftMoves_corec
• LGame.rightMoves_corec

[Violeta Hernández]

And perhaps LGame.hom_unique too, I'm not sure if it can be proven from the others

[Aaron Liu]

It can probably be proved by bisimulation

[Aaron Liu]

bisimulation is what you get from constructing approximations that agree and hom_unique is what category theory says you should get for a final coalgebra

[Aaron Liu]

the hom in the theorem name refers to coalgebra homomorphisms

[Violeta Hernández]

I figured as much, as soon as I saw the compositions in the theorem statement I knew there was some commutative diagram at play

[Aaron Liu]

I considered making them the applied version but decided against it

[Violeta Hernández]

I like the unapplied version better, aesthetically speaking

[Violeta Hernández]

If we need the applied version we can add it later

[Violeta Hernández]

Well, we've discussed a lot about the implementation details of loopy games, but what about their actual theory? What can we do with our new toy?

[Aaron Liu]

we can start by defining addition corecursively

[Aaron Liu]

or maybe the map from games to loopy games

[Aaron Liu]

show that they commute

[Violeta Hernández]

Here's a rough to-do from things I have in mind

• Define other basic games like 0 and 1
• Define the embedding IGame ↪ LGame
• Define negation and addition of loopy games
• Define... multiplication? Can you do that? Does it satisfy anything interesting?
• Define outcome classes
• Build some "real life" games like Tic-tac-toe or chess; you can't really define them within IGame because there's ties, but I hear dud can be used to represent a tied state?

[Violeta Hernández]

@Aaron Liu I think the bisimulation principle you defined might not be the most general one. What do you think about this?

theorem eq_of_bisim (r : LGame → LGame → Prop)
    (hl : ∀ x y, r x y → ∃ s : Set (LGame × LGame),
      Prod.fst '' s = x.leftMoves ∧ Prod.snd '' s = y.leftMoves ∧ ∀ z ∈ s, r z.1 z.2)
    (hr : ∀ x y, r x y → ∃ t : Set (LGame × LGame),
      Prod.fst '' t = x.rightMoves ∧ Prod.snd '' t = y.rightMoves ∧ ∀ z ∈ t, r z.1 z.2)
    (x y : LGame.{u}) (hxy : r x y) : x = y := sorry

[Violeta Hernández]

This generalizes the principle stated with equivalences, since the pairings specified by s and t are not a priori one to one. For instance, to prove that a + dud = dud, you need to use the bisimulation r x y ↔ (∃ b, x = b + dud) ∧ y = dud. Then assuming r x y, the set s is x.leftMoves ×ˢ {dud} and the set t is x.rightMoves ×ˢ {dud}. You don't know that these are singleton sets until you prove the theorem!

[Violeta Hernández]

Oh and also we don't have to deal with equivalences on subtypes, thank goodness

[Violeta Hernández]

PGame PTSD

[Violeta Hernández]

I replaced the old form of bisimulation by this. I'm not a fan of having complicated theorems that end up being weaker than other theorems in nontrivial ways. (Not fun being halfway through a proof when you realize you're using the wrong result!)

[Violeta Hernández]

I feel like working on loopy arithmetic

[Violeta Hernández]

I find this immensely satisfying:

instance : Neg LGame where
  neg := corec rightMoves leftMoves

[Violeta Hernández]

Hmm, I think I've hit somewhat of a wall. How do you prove this?

instance : Add LGame where
  add x y := corec
    (fun x ↦ (fun y ↦ (y, x.2)) '' leftMoves x.1 ∪ (fun y ↦ (x.1, y)) '' leftMoves x.2)
    (fun x ↦ (fun y ↦ (y, x.2)) '' rightMoves x.1 ∪ (fun y ↦ (x.1, y)) '' rightMoves x.2)
    (x, y)

theorem corec_add_corec
    {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β}
    [∀ x, Small.{u} (leftMovesα x)] [∀ x, Small.{u} (rightMovesα x)]
    [∀ x, Small.{u} (leftMovesβ x)] [∀ x, Small.{u} (rightMovesβ x)] (initα : α) (initβ : β) :
    corec leftMovesα rightMovesα initα + corec leftMovesβ rightMovesβ initβ =
    corec
      (fun x ↦ (fun y ↦ (y, x.2)) '' leftMovesα x.1 ∪ (fun y ↦ (x.1, y)) '' leftMovesβ x.2)
      (fun x ↦ (fun y ↦ (y, x.2)) '' rightMovesα x.1 ∪ (fun y ↦ (x.1, y)) '' rightMovesβ x.2)
      (initα, initβ) := by
  sorry

[Violeta Hernández]

The analogous theorem on negation was really easy, it was an immediate application of corec_comp_hom

[Violeta Hernández]

I'm not really sure how to do this one, though

[Violeta Hernández]

It's probably doable with a bisimulation but I'd love if there was a more direct argument through the universal property

[Aaron Liu]

Violeta Hernández said:

This generalizes the principle stated with equivalences, since the pairings specified by s and t are not a priori one to one. For instance, to prove that a + dud = dud, you need to use the bisimulation r x y ↔ (∃ b, x = b + dud) ∧ y = dud. Then assuming r x y, the set s is x.leftMoves ×ˢ {dud} and the set t is x.rightMoves ×ˢ {dud}. You don't know that these are singleton sets until you prove the theorem!

This is great but I was having trouble proving this version

[Aaron Liu]

Violeta Hernández said:

I'm not really sure how to do this one, though

Just ext, their left and right moves are the same

[Aaron Liu]

Hmm I'm not actually 100% sure that that works

[Aaron Liu]

oh I think this is a case of corec_comp_hom where you set (f := Prod.map (corec leftMovesα rightMovesα) (corec leftMovesβ rightMovesβ))

[Aaron Liu]

theorem corec_add_corec
    {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β}
    [∀ x, Small.{u} (leftMovesα x)] [∀ x, Small.{u} (rightMovesα x)]
    [∀ x, Small.{u} (leftMovesβ x)] [∀ x, Small.{u} (rightMovesβ x)] (initα : α) (initβ : β) :
    corec leftMovesα rightMovesα initα + corec leftMovesβ rightMovesβ initβ =
    corec
      (fun x ↦ (fun y ↦ (y, x.2)) '' leftMovesα x.1 ∪ (fun y ↦ (x.1, y)) '' leftMovesβ x.2)
      (fun x ↦ (fun y ↦ (y, x.2)) '' rightMovesα x.1 ∪ (fun y ↦ (x.1, y)) '' rightMovesβ x.2)
      (initα, initβ) := by
  refine congrFun (corec_comp_hom
    (f := Prod.map (corec leftMovesα rightMovesα) (corec leftMovesβ rightMovesβ))
    _ _ _ _ ?_ ?_) (initα, initβ)
  · refine funext fun ⟨a, b⟩ => ?_
    simp [Set.image_image, Set.image_union, leftMoves_corec]
  · refine funext fun ⟨a, b⟩ => ?_
    simp [Set.image_image, Set.image_union, rightMoves_corec]

[Aaron Liu]

Aaron Liu said:

Violeta Hernández said:

This generalizes the principle stated with equivalences, since the pairings specified by s and t are not a priori one to one. For instance, to prove that a + dud = dud, you need to use the bisimulation r x y ↔ (∃ b, x = b + dud) ∧ y = dud. Then assuming r x y, the set s is x.leftMoves ×ˢ {dud} and the set t is x.rightMoves ×ˢ {dud}. You don't know that these are singleton sets until you prove the theorem!

This is great but I was having trouble proving this version

I just realized it's actually very easy to prove this version and I was just being stupid

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

This generalizes the principle stated with equivalences, since the pairings specified by s and t are not a priori one to one. For instance, to prove that a + dud = dud, you need to use the bisimulation r x y ↔ (∃ b, x = b + dud) ∧ y = dud. Then assuming r x y, the set s is x.leftMoves ×ˢ {dud} and the set t is x.rightMoves ×ˢ {dud}. You don't know that these are singleton sets until you prove the theorem!

This is great but I was having trouble proving this version

You can prove the equivalence version in terms of the more general principle I gave, the sets s and t you take are range fun x => (x, el x) and range fun x => (x, er x)

[Violeta Hernández]

But given how much I was able to golf using the non-equiv version I really doubt we want the equiv version

[Aaron Liu]

The reason I didn't use the non-equiv version is that I thought it was very hard to prove

[Aaron Liu]

it turns out it's just not hard at all

[Violeta Hernández]

Yeah, the proof mostly boils down to unfolding Functor.Liftr

[Aaron Liu]

Could the bisimulation theorem be stated using docs#Relator.BiTotal

[Violeta Hernández]

It could. A bisimulation is relation when r x y implies that r is bitotal when restricted to the left resp. right options of x and y.

[Violeta Hernández]

That needlessly introduces subtypes though, so I'm not sure it's better than what I wrote down.

[Violeta Hernández]

It might be worth adding that to the docstring, though.

[Violeta Hernández]

Actually, it's a bit more subtle than that. A bisimulation requires that some subrelation of r is bitotal on the left resp. right sets, not necessarily that the entire thing is.

[Bhavik Mehta]

just mentioning #computer science > Bisimulation @ 💬, in case there's opportunity for code reuse here

[Violeta Hernández]

The problem isn't really defining bisimulations, but rather how to best convert the horrible functorial mess docs#Functor.Liftr gives you into something nice for our specific case.

[Violeta Hernández]

Bisimulation proofs are so funny, as soon as you finish them you go back and realize "hey the clever bisimulation i built is literally just an equality"

[Violeta Hernández]

I've been pretty successful with my lemma eq_of_bisim. Check this out:

private theorem add_assoc' (x y z : LGame) : x + y + z = x + (y + z) := by
  apply eq_of_bisim (fun x y ↦ ∃ a b c, x = a + b + c ∧ y = a + (b + c)) ?_ ⟨x, y, z, rfl, rfl⟩
  rintro _ _ ⟨a, b, c, rfl, rfl⟩
  refine
    ⟨⟨(fun x ↦ (x + b + c, x + (b + c))) '' a.leftMoves ∪
    (fun x ↦ (a + x + c, a + (x + c))) '' b.leftMoves ∪
    (fun x ↦ (a + b + x, a + (b + x))) '' c.leftMoves, ?_, ?_⟩,
    ⟨(fun x ↦ (x + b + c, x + (b + c))) '' a.rightMoves ∪
    (fun x ↦ (a + x + c, a + (x + c))) '' b.rightMoves ∪
    (fun x ↦ (a + b + x, a + (b + x))) '' c.rightMoves, ?_, ?_⟩⟩
  all_goals aesop (add simp [image_union])

[Violeta Hernández]

I managed to prove the SubtractionCommMonoidstructure on LGame, and prove a few simple equations like on + off = dud and x + dud = dud.
https://github.com/vihdzp/combinatorial-games/pull/166

[Aaron Liu]

If you think of equality in QPF.Cofix as a coinductive type with destructor

theorem eq_liftr_dest {F : Type u → Type u} [QPF F] {x y : QPF.Cofix F} (h : x = y) :
    Functor.Liftr Eq x.dest y.dest := by
  subst h
  refine ⟨(fun x => ⟨(x, x), rfl⟩) <$> x.dest, ?_, ?_⟩
  · simp_rw [← QPF.comp_map, Function.comp_def]
    exact QPF.id_map x.dest
  · simp_rw [← QPF.comp_map, Function.comp_def]
    exact QPF.id_map x.dest

then bisimulation provides a corecursion principle for equality

[Violeta Hernández]

Interesting! I hadn't really understood that link between corecursion and bisimulations.

[Violeta Hernández]

Is it possible to define multiplication of loopy games?

[Violeta Hernández]

In some "natural" way that gives you the theorem toLGame (x * y) = toLGame x * toLGame y

[Violeta Hernández]

Or perhaps more explicitly. Say that you have two games corec α lα rα x and corec β lβ rβ y. If you wanted to multiply them as corec γ lγ rγ z, what would the type γ be?

[Violeta Hernández]

For addition, γ = α × β, representing that a state in the addition is a pair of states, one in α, one in β.

[Violeta Hernández]

I guess you could define γ as some appropriate inductive type. Wouldn't be pretty, though.

[Violeta Hernández]

Oh actually, it might work to define γ = Multiset (α × β).

[Violeta Hernández]

No, it's worse than that.

[Violeta Hernández]

Correct me if I'm wrong but, every subposition of x * y looks like a finite sum of ± a_i * b_i for a_i a subposition of x and b_i a subposition of y

[Violeta Hernández]

(deleted)

[Violeta Hernández]

So my idea is, define x * y as corec (Multiset (Bool × LGame × LGame)) lγ rγ (true, x, y), where lγ and rγ are the bespoke functions that assign a multiset (interpreted as a game Σ ±aᵢ × bᵢ) to the other multisets for their left and right options.

[Violeta Hernández]

This is an awful definition, and it will be awful to prove that the left and right moves of x * y are what we expect, but hopefully once we do that we never have to work with the multiset definition again.

[Violeta Hernández]

Lmk if you have simpler ideas

[Violeta Hernández]

I honestly doubt there's much to say about multiplication of loopy games in general. But at the very least we should still be able to prove the basic stuff like 0 * x = 0 and 1 * x = 1.

[Violeta Hernández]

Question, is this true?

proof_wanted eq_iGame_of_not_subposition {x : LGame}
    (h : ∀ y, Subposition y x, ¬ Subposition y y) : ∃ z : IGame, x = z.toLGame

[Aaron Liu]

no

[Violeta Hernández]

Is anything similar to this true?

[Violeta Hernández]

Basically I'm trying to find the conditions for a loopy game to not be loopy

[Aaron Liu]

the condition is that the subpositions are well founded

[Violeta Hernández]

Oh, you're right. It is possible for a game to go on forever without repeating subpositions

[Aaron Liu]

Violeta Hernández said:

Is anything similar to this true?

the counterexample is #combinatorial-games > Loopy games @ 💬 but two sided

[Aaron Liu]

I think it's the same as Acc Subposition x

[Violeta Hernández]

That's a very elegant way to put it. So IGame is in a sense the subtype of accessible LGames

[Violeta Hernández]

I gave a definition of multiplication. But I'm having a really hard time proving corec_mul_corec and leftMoves_mul: https://github.com/vihdzp/combinatorial-games/blob/a60241d87afbc07c390c9b0b19ba38937e766c28/CombinatorialGames/Game/Loopy/Basic.lean#L576

[Aaron Liu]

it can't be that hard right

[Aaron Liu]

I'll try

[Violeta Hernández]

It may be that I'm not using the simplest/nicest definition for it, if you can find any improvements please push them to the branch!

[Aaron Liu]

I have an aversion to changing definitions even if it makes everything better

[Aaron Liu]

also I'm 90% sure that I don't have push access

[Violeta Hernández]

Oh yeah you're right

[Violeta Hernández]

uhhh you can clone my branch ig

[Aaron Liu]

try doing something simpler first

[Aaron Liu]

can you prove leftMovesAux commutes with the map

[Violeta Hernández]

Can you write the type signature for that?

[Violeta Hernández]

It would look like

leftMovesAux lα rα lβ rβ (map f g x) = map f g '' leftMovesAux lα' rα' lβ' rβ' x

but I don't know what the relation between lα and lα' etc would be

[Aaron Liu]

the goal is to show that leftMovesAux is a natural transformation of functors

[Aaron Liu]

I'm currently trying to figure out what that translates to in Lean

[Aaron Liu]

I think this is correct

/--
If `f : α₁ → α₂` and `g : β₁ → β₂` are morphisms in the category of `GameFunctor`-coalgebras then
the diagram
```
               leftMovesAux
    (Bool × α₁ × β₁) → Set (MulTy α₁ β₁)
 (id, f, g) ↓                   ↓ Set.image (MulTy.map f g)
    (Bool × α₂ × β₂) → Set (MulTy α₂ β₂)
               leftMovesAux
```
commutes
-/
theorem leftMovesAux_comp_prodMap {α₁ α₂ β₁ β₂ : Type*}
    (leftMovesα₁ rightMovesα₁ : α₁ → Set α₁)
    (leftMovesβ₁ rightMovesβ₁ : β₁ → Set β₁)
    (leftMovesα₂ rightMovesα₂ : α₂ → Set α₂)
    (leftMovesβ₂ rightMovesβ₂ : β₂ → Set β₂)
    (f : α₁ → α₂) (g : β₁ → β₂)
    (fl : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁)
    (fr : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁)
    (gl : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁)
    (gr : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) :
    MulTy.leftMovesAux leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘
      Prod.map id (Prod.map f g) =
    Set.image (MulTy.map f g) ∘
      MulTy.leftMovesAux leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁ := by
  sorry

[Violeta Hernández]

wow, and yikes

[Aaron Liu]

the diagram makes it easy to understand

[Violeta Hernández]

That's appreciated

[Violeta Hernández]

Here you go!

@[simp]
theorem map_mulOption (b x y) :
    map f g (mulOption b x y) = mulOption b (Prod.map f g x) (Prod.map f g y) := by
  simp [mulOption, map, Prod.map]

set_option maxHeartBeats 500000 in
theorem leftMovesAux'_comp_prodMap
    (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁)
    (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁)
    (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁)
    (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) :
    MulTy.leftMovesAux' leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘
      Prod.map id (Prod.map f g) =
    Set.image (MulTy.map f g) ∘
      MulTy.leftMovesAux' leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁ := by
  simp_rw [funext_iff, Function.comp_apply, leftMovesAux'] at *
  aesop

[Violeta Hernández]

God bless aesop

[Aaron Liu]

500000???

[Aaron Liu]

wow

[Violeta Hernández]

that's for the primed version but the unprimed version should follow directly from this and the analogous result for right moves

[Aaron Liu]

great

[Violeta Hernández]

Aaron Liu said:

500000???

Not even the highest number in our repo :sob:

[Aaron Liu]

It seems you have already done the appropriate square for split so next is leftMoves and rightMoves

[Violeta Hernández]

theorem leftMovesAux_comp_prodMap
    (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁)
    (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁)
    (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁)
    (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) :
    MulTy.leftMovesAux leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘
      Prod.map id (Prod.map f g) =
    image (MulTy.map f g) ∘
      MulTy.leftMovesAux leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁ := by
  apply funext
  rintro ⟨(_ | _), x⟩
  · exact congrFun (rightMovesAux'_comp_prodMap hlf hrf hlg hrg) (false, x)
  · exact congrFun (leftMovesAux'_comp_prodMap hlf hrf hlg hrg) (true, x)

[Violeta Hernández]

Yeah this one was easy

[Violeta Hernández]

I should be able to prove the actual result now maybe?

[Aaron Liu]

that's the idea

[Violeta Hernández]

Awesome!

theorem leftMoves_comp_map
    (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁)
    (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁)
    (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁)
    (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) :
    leftMoves leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘ map f g =
    image (map f g) ∘ leftMoves leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁ := by
  apply funext fun x ↦ ?_
  simp_rw [Function.comp_apply, leftMoves, image_sUnion, split_map, Finset.coe_image, image_image,
    Prod.map_fst, Prod.map_snd, ← Function.comp_apply (g := Prod.map id (Prod.map f g)),
    leftMovesAux_comp_prodMap hlf hrf hlg hrg]
  aesop

[Violeta Hernández]

Just managed to prove corec_mul_corec too! Pushed it to the branch.

[Aaron Liu]

yay

[Aaron Liu]

leftMoves_mul should follow then I think

[Violeta Hernández]

On a related note. I'm a bit unsure about how much of MulTy should be private API and how much should be public.

[Aaron Liu]

I think to prove leftMoves_mul you might have to use hom_unique again

[Violeta Hernández]

Oh oops turns out my definition of leftMovesAuxis wrong :frown:

[Aaron Liu]

:(

[Violeta Hernández]

It should be

def leftMovesAux (x : Bool × α × β) : Set (MulTy α β) :=
  x.1.rec
    (rightMovesAux' leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2))
    (leftMovesAux' leftMovesα rightMovesα leftMovesβ rightMovesβ x)

(the (!x.1, x.2) bit was just an x previously)

[Violeta Hernández]

Since left moves of -x * y are negatives of right moves of x * y

[Violeta Hernández]

thankfully all the other proofs compile with minimal changes

[Aaron Liu]

I'm glad I don't have to think about this

[Violeta Hernández]

I'm thinking about the privacy thing still. What do you think about making leftMovesAux' private, but making leftMovesAux public (with a better name) as well as leftMoves?

[Aaron Liu]

no idea

[Violeta Hernández]

Specifically, we'd make this public API:

theorem leftMovesSingle_def (x : Bool × α × β) :
    leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x = x.1.rec
      ((mulOption (!x.1) x.2) ''
        (leftMovesα x.2.1 ×ˢ rightMovesβ x.2.2 ∪ rightMovesα x.2.1 ×ˢ leftMovesβ x.2.2))
      (mulOption x.1 x.2 ''
        (leftMovesα x.2.1 ×ˢ leftMovesβ x.2.2 ∪ rightMovesα x.2.1 ×ˢ rightMovesβ x.2.2)) := by
  obtain ⟨(_ | _), _⟩ := x <;> rfl

[Violeta Hernández]

(leftMovesAux → leftMovesSingle)

[Aaron Liu]

sure I guess

[Violeta Hernández]

Wait I'm realizing something isn't

Violeta Hernández said:

Since left moves of -x * y are negatives of right moves of x * y

oh also nvm about this I just realized that I don't have to negate x.1 like that since that's already the case where it's false

[Violeta Hernández]

you can tell I barely have a grasp on this

[Aaron Liu]

I might understand it if you translate it into category theory

[Violeta Hernández]

I've no idea how to do that

[Violeta Hernández]

I think this makes more sense if you think of MulTy α β as the type of formal signed sums of products in α × β

[Aaron Liu]

so it's the free something on α × β

[Violeta Hernández]

Multiset α is the free commutative monoid on α I believe

[Violeta Hernández]

so MulTy α β is the free commutative monoid on Bool × α × β

[Aaron Liu]

...sure

[Violeta Hernández]

Aaron Liu said:

I think to prove leftMoves_mul you might have to use hom_unique again

Yeah, I think I need to prove that mulOption commutes with corec

[Violeta Hernández]

More specifically this (I think h is redundant here)
image.png

[Violeta Hernández]

Actually this looks more like corec_comp_hom.

[Violeta Hernández]

In either case I have no idea what the map is supposed to be

[Violeta Hernández]

help welcome

[Violeta Hernández]

Oh NVM I get it

[Violeta Hernández]

I have to define the function MulTy LGame LGame -> LGame in the obvious way

[Violeta Hernández]

And use that in corec_comp_hom

[Violeta Hernández]

I've kept deliberating on this. I really think MulTy should be public API. There's a sort of naturality here: addition of two games is described by a pair of states from both games. Multiplication of two games is described by a signed finite sum of pairs of states of both games.

[Violeta Hernández]

Following this, we could add ConcreteGame (α × β) and ConcreteGame (MulTy α β) instances.

[Violeta Hernández]

Speaking of. I was thinking about splitting ConcreteGame into ConcreteLGame and ConcreteIGame, with the latter extending the former with proofs that relLeft and relRight are wf.

[Aaron Liu]

that sounds not bad

[Violeta Hernández]

I managed to find a bit of a simplification in definitions. Turns out you don't need MulTy.split, you can just do this:

def leftMoves (x : MulTy α β) : Set (MulTy α β) :=
  ⋃ y ∈ x, (x.erase y + ·) '' leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ y

[Violeta Hernández]

I like how when you simplify a definition the proofs follow neatly

[Violeta Hernández]

I'm still breaking my head over this. I haven't been able to prove the main theorem about MulTy yet (corec of x : MulTy α β equals Σ ±aᵢ * bᵢ), but I feel like I'm making progress.

[Violeta Hernández]

Can't continue today though, and probably can't continue tomorrow either, but I'll see what I can do over the week.

[Aaron Liu]

good luck

[Violeta Hernández]

Call an LGame short if Finite {y | Subposition y x}. Is the product of two short LGames short?

[Violeta Hernández]

At face value it seems like the answer should be no, because MulTy α β is always infinite for nonempty types. But it is possible for a lot of the states to collapse. For instance, I'm pretty sure dud * x = dud for all x ≠ 0.

[Violeta Hernández]

At the very least, I'm not aware of counterexamples.

[Aaron Liu]

Consider $\bold{tis} = \{\bold{tisn} | \}$ and $\bold{tisn} = \{ | \bold{tis}\}$

[Aaron Liu]

then I claim the product $\bold{tis} \cdot \bold{tisn}$ has infinitely many distinct subpositions

[Violeta Hernández]

What does tis stand for?

[Aaron Liu]

image.png

[Aaron Liu]

from Winning Ways volume 2

[Violeta Hernández]

Oh nice

[Violeta Hernández]

Someone should make a small PR adding those two

[Violeta Hernández]

(deleted)

[Violeta Hernández]

So clearly tisn= -tis and thus tis * tisn = -(tis * tis)

[Aaron Liu]

I have to go for now

[Violeta Hernández]

The only left move of tis * tis is -3 • (tis * tis), it has no right moves

[Violeta Hernández]

It doesn't seem completely implausible that tis * tis = tis

[Violeta Hernández]

I gtg too, I'll come back to this

[Violeta Hernández]

So then 3 • (tis * tis) = {2 • (tis * tis) - 3 • (tis * tis) | }

[Violeta Hernández]

Interesting

[Aaron Liu]

I'm back

[Violeta Hernández]

So am I

[Aaron Liu]

welcome back

[Aaron Liu]

so the infinitely many subpositions I was talking about is 3 ^ n • (tis * tis) for every odd n

[Aaron Liu]

clearly these are all distinct

[Aaron Liu]

and they also all arise as subpositions

[Violeta Hernández]

It's not clear to me

[Violeta Hernández]

There's idempotent games such as dud

[Aaron Liu]

count how many moves you can make in a row as left before you run out

[Violeta Hernández]

The only left option of 3 ^ n • (tis * tis) is (3 ^ n - 1) • (tis * tis) - 3 • (tis * tis)

[Violeta Hernández]

The left options of that I'm not too eager to calculate

[Aaron Liu]

what are the left options of - 3 • (tis * tis)?

[Violeta Hernández]

Oh, there's none

[Violeta Hernández]

I see

[Violeta Hernández]

So you can do 3 ^ n consecutive moves as left, no less and no more

[Violeta Hernández]

And obviously this value is well-defined so that shows all these games are distinct

[Violeta Hernández]

Oh and also obviously they're all achievable as subpositions

[Violeta Hernández]

You just keep dividing tis * tis into -3 copies of itself over and over

[Violeta Hernández]

Awesome!

[Violeta Hernández]

I'd love to see this in the counterexample folder

[Violeta Hernández]

...as soon as I actually PR multiplication of loopy games, that is

[Violeta Hernández]

I did it!
image.png

[Violeta Hernández]

Only took 400 lines of code + two maxHeartbeats 1000000

[Violeta Hernández]

(feel inclined to tag Bhavik just to annoy him :stuck_out_tongue:)

[Violeta Hernández]

https://github.com/vihdzp/combinatorial-games/pull/168

[Violeta Hernández]

I made a best effort to organize and explain my code, though it's still a bit rough around the edges. I'd appreciate if you guys could take a good look.

[Violeta Hernández]

Violeta Hernández said:

Someone should make a small PR adding those two

I truly can't help myself
https://github.com/vihdzp/combinatorial-games/pull/171/files

[Violeta Hernández]

@Tristan Figueroa-Reid asking you as someone more familiar with literature. How should we define the preorder of loopy games?

[Violeta Hernández]

I've been reluctant about adding definitions of outcomes to IGame, since they're entirely determined by the order relations of a game with 0. But in the loopy case this isn't true anymore.

[Tristan Figueroa-Reid]

No clue for that one. Outcome classes are the only way I know how to reason with ordering for loopy games.

[Tristan Figueroa-Reid]

You could also try defining ordering with stoppers? Though it seems more intuitive to define ordering with outcome classes, then formalize stoppers and reason with those after the fact.

[Violeta Hernández]

In any case we need some way to state what the outcome of a game is.

[Violeta Hernández]

Tristan Figueroa-Reid said:

You could also try defining ordering with stoppers? Though it seems more intuitive to define ordering with outcome classes, then formalize stoppers and reason with those after the fact.

How do you define ordering with stoppers?

[Tristan Figueroa-Reid]

I think this trick was done in Aaron Siegel's masters thesis (this might not be terminating on long loopy games?), but for determining G <= H, you can show that right can not force left to run out of games in H - G by traversing H - G starting at its start vertex:

When traversing a vertex V with player P, you store a counter c to V for the number of its outgoing edges that are not marked as wins for the opposing player of P. If c is 0 then V is a win, and all nodes connecting incoming edges get their counters decremented (where this c = 0 check gets propagated backwards). Then you repeat this for all outgoing neighbors of V.

(I'll just try to find the reference but I don't have a copy of Aaron Siegel's thesis anymore?)

[Tristan Figueroa-Reid]

(Then, since this works only for stoppers, you can decompose a game into its sides and do this check for both sides when either one of G and H aren't loopy)

[Violeta Hernández]

But not all loopy games have such a decomposition, do they?

[Violeta Hernández]

I recall seeing that in another of Siegel's papers

[Tristan Figueroa-Reid]

Right - Bach's Carousel can't be decomposed with sides.

[Violeta Hernández]

So I think the question now is how to formalize outcomes.

[Violeta Hernández]

Do we need to first formalize strategies? That sounds somewhat painful.

[Tristan Figueroa-Reid]

I don't think so? At least for non-tied loopy games, you can say that a loopy game is winnable by Left or Right recursively by looking for empty sets of right or left moves respectively (then for games with no empty right/left sets, looking at the right/left options and checking if any of it's left/right options are in the desired outcome class).

[Violeta Hernández]

Well that's the thing, we can't define things recursively if the games aren't well-founded

[Tristan Figueroa-Reid]

Perhaps if there exists some amount of fuel which can be used to traverse these games?

[Violeta Hernández]

Actually. What even is the mathematical definition of saying that a loopy game is tied, say, if left starts?

[Tristan Figueroa-Reid]

Good question! I've always understood it as games that don't belong in any of the winning outcome classes, which is why I suggested using fuel.

[Violeta Hernández]

I'm unsure if using fuel works even in the case of an infinite well-founded game.

[Violeta Hernández]

At least I can't figure out how to complete the idea. Is it "a game is tied iff it isn't won by left or right in n moves, for any n"?

[Violeta Hernández]

Take some positive game x such that for every n, there exists some right option of x that cannot end in less than n turns. This definitely exists, I think every positive irrational should work.

Then, if right starts, the game x is won by left, but it's not necessarily won by left in n turns, for any given n.

[Violeta Hernández]

From working with loopy vs. well-founded games, I get the impression that the theory of loopy games is somehow more global - for instance, to define a general loopy game, you need to use the corecursor, which requires you to build the entire game graph. By contrast, the theory of well-founded games is more local. To define a game you only need consider its immediate options.

[Violeta Hernández]

From that perspective, it seems quite reasonable that strategies would be required to talk about loopy games, even if they can be omitted from a treatment of well-founded games.

[Violeta Hernández]

Though perhaps a better question to ask: how do you define survivability?

[Violeta Hernández]

I think that is what we need to formalize. A strategy is just a proof of survivability on a well-founded game.

[Violeta Hernández]

Informally a strategy is a sort of recursive object. In a strategy for left, for every subposition reachable by right under the strategy, it assigns a left move. (Which in particular implies a left move exists, under these circumstances)

[Violeta Hernández]

As to how to translate this into Lean...

[Violeta Hernández]

I feel like this might be a coinductive type? Not sure.

[Tristan Figueroa-Reid]

You can (terribly, with dependent types and all) formalize strategies by making a function from an LGame subtype of all possible options of x to its subpositions. However, I don't think having a definition of strategy is the biggest concern?

[Violeta Hernández]

Well, I don't see a way to define survivability otherwise.

[Tristan Figueroa-Reid]

How would survivability be defined?

[Violeta Hernández]

Left survives a loopy game if there exists a strategy for him.

[Violeta Hernández]

Tristan Figueroa-Reid said:

You can (terribly, with dependent types and all) formalize strategies by making a function from an LGame subtype of all possible options of x to its subpositions. However, I don't think having a definition of strategy is the biggest concern?

That's not quite it, I think. What would be a left strategy for 1? It exists, of course. But there's no function that maps all subpositions of 1 to a left option of them, because 0 has no left option.

[Violeta Hernández]

Perhaps I misunderstand what you mean?

[Tristan Figueroa-Reid]

You're right, it should be a partial function.

[Violeta Hernández]

Oh, that might actually work

[Tristan Figueroa-Reid]

Violeta Hernández said:

Left survives a loopy game if there exists a strategy for him.

Strategies can exist without them being good ones.

[Violeta Hernández]

So a partial function such that if you follow it, the output is never none?

[Tristan Figueroa-Reid]

Violeta Hernández said:

So a partial function such that if you follow it, the output is never none?

Hm, that might work for properly loopy games, but I believe that fails for well-founded games.

[Violeta Hernández]

Tristan Figueroa-Reid said:

Violeta Hernández said:

Left survives a loopy game if there exists a strategy for him.

Strategies can exist without them being good ones.

I'm not saying Left has to win. To survive a game is simply not to lose.

[Violeta Hernández]

Tristan Figueroa-Reid said:

Violeta Hernández said:

So a partial function such that if you follow it, the output is never none?

Hm, that might work for properly loopy games, but I believe that fails for well-founded games.

Take 1. A strategy for left is the function 1 -> 0 and 0 -> none. If you follow the strategy, after any right move, the function doesn't return none, because there's no move right can make if you follow the strategy!

[Tristan Figueroa-Reid]

Hm. How about a Left strategy on -1?

[Violeta Hernández]

That won't exist, because -1 is won by right.

[Tristan Figueroa-Reid]

Right. Left's strategy on {-1|}?

[Violeta Hernández]

That's equivalent to 0, right? So if left starts he doesn't have a strategy, because right wins.

[Violeta Hernández]

Let me formalize what I mean. Let x be a game. Let f be a partial function mapping subpositions of x to either left options of them, or none. Define a (left) "history" of f as a list of pairs p_i = (a_i, b_i), where a_0 = x, b_i is some arbitrary right move of a_i, and a_(i+1) = f(b_i). Then f is a strategy for left (starting first) if for every history of f ending in (a_i, b_i), we have f(b_i) ≠ none.

[Violeta Hernández]

A strategy for left starting second can be defined similarly. It can also be defined as a function from right options of x to strategies of left starting first.

[Tristan Figueroa-Reid]

This definition seems to work :+1:

[Violeta Hernández]

Here's a stub:

import CombinatorialGames.Game.Loopy.Basic
import CombinatorialGames.Game.IGame

namespace LGame

/-- A sequence of moves following a left strategy `f`. -/
def LeftHistory (f : LGame → Option LGame) (l : List (LGame × LGame)) : Prop :=
  match l with
  | [] => False
  | [(a, b)] => b ∈ a.rightMoves
  | (a, b) :: (c, d) :: l => b ∈ a.rightMoves ∧ a ∈ f d ∧ LeftHistory f ((c, d) :: l)

theorem LeftHistory.ne_nil {f : LGame → Option LGame} {l : List (LGame × LGame)}
    (hl : LeftHistory f l) : l ≠ [] := by
  cases l with
  | nil => contradiction
  | cons a l => exact List.cons_ne_nil a l

/-- A strategy for Left, when they go second. -/
structure LeftStrategy (x : LGame) (f : LGame → Option LGame) : Prop where
  forall_mem_leftMoves {y z : LGame} (h : z ∈ f y) : z ∈ y.leftMoves
  exists_forall_leftHistory {l : List (LGame × LGame)}
    (hl : LeftHistory f l) (hl₀ : (l.getLast hl.ne_nil).1 = x) : (f (l.head hl.ne_nil).2).isSome

proof_wanted zero_le_of_leftStrategy {x : IGame} {f : LGame → Option LGame}
    (hf : LeftStrategy x.toLGame f) : 0 ≤ x

end LGame

[Violeta Hernández]

Does this seem reasonable?

[Aaron Liu]

I have a different idea

[Violeta Hernández]

I'm all ears

[Aaron Liu]

Instead of asking left to win in n moves for some n

[Aaron Liu]

wait what was the goal again?

[Tristan Figueroa-Reid]

To define a Preorder on LGame

[Aaron Liu]

what's the order?

[Violeta Hernández]

The one from Misere games

[Violeta Hernández]

x ≤ y when o(x + z) ≤ o(y + z) for all z

[Aaron Liu]

so the goal is to define outcomes

[Violeta Hernández]

Indeed

[Violeta Hernández]

I was trying to define what it meant for a player to survive a game

[Violeta Hernández]

I don't see a better way to do it than strategies

[Aaron Liu]

Define survive as "not die"?

[Aaron Liu]

I have an idea that I think works for dying on stoppers

[Tristan Figueroa-Reid]

Stoppers are fine, but I think it was brought up earlier that we can't decompose all LGames to their sides.

[Aaron Liu]

yeah not all loopy games have stopper sides

[Aaron Liu]

I think

[Violeta Hernández]

(yet another thing to add to the counterexample folder)

[Aaron Liu]

I'm a bit hazy on everything

[Tristan Figueroa-Reid]

I think we had an explicit counterexample of Bach's Carousel. That's going to be fun to encode in LGame.

[Violeta Hernández]

So yeah, the best idea I've got is to define strategies

[Aaron Liu]

Here's my spelling of "left kills right when right goes first on x":

∃ f : LGame.{u} → (Option Ordinal.{u} × Option Ordinal.{u}),
  (f x).2.isSome ∧ ∀ : LGame.{u} y,
    (∀ o ∈ (f y).1, ∃ z ∈ y.leftMoves, ∃ o' ∈ (f z).2, o' < o) ∧
    (∀ o ∈ (f y).2, ∀ z ∈ y.rightMoves, ∃ o' ∈ (f z).1, o' ≤ o)

[Aaron Liu]

this also works with slight modifications for left going first, or for right killing left

[Violeta Hernández]

I think I sort of get it. f x is supposed to represent the number of left/right moves remaining?

[Aaron Liu]

yes

[Violeta Hernández]

∀ y, (∀ o ∈ y.1, ∃ z ∈ y.leftMoves, ∃ o' ∈ z.2, o' < o)

I have no idea what the types are supposed to be here.

[Aaron Liu]

sorry, editited

[Aaron Liu]

I think it should be good now

[Aaron Liu]

I was typing this without an infoview

[Violeta Hernández]

Shouldn't it be o ≤ o' in the last inequality?

[Aaron Liu]

explain?

[Violeta Hernández]

Every right move of y should be no better for right than for left

[Aaron Liu]

I don't get it

[Violeta Hernández]

o is the value for right, o' is the value for left

[Violeta Hernández]

I think

[Aaron Liu]

not true

[Aaron Liu]

the ordinals need to decrease to ensure termination

[Violeta Hernández]

What do the ordinals represent, though?

[Aaron Liu]

they're a death clock

[Aaron Liu]

they keep decreasing, and when they hit zero then right loses

[Violeta Hernández]

And left never loses before right does, because...?

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think I sort of get it. f x is supposed to represent the number of left/right moves remaining?

How is that consistent with the above statement? I don't see how this + the ordinals decreasing + o ≤ o' being wrong can all coexist.

[Aaron Liu]

Violeta Hernández said:

And left never loses before right does, because...?

because left always has another move (∀ o ∈ (f y).1, ∃ z ∈ y.leftMoves, ...)

[Aaron Liu]

when left moves the death clock goes down

[Violeta Hernández]

Oh, so f x is really just a single clock, and you read the entry according to which player is playing. If left plays, he has some move decreasing the clock. If right plays, none of her moves can increase the clock.

[Aaron Liu]

It's not side weird two sided clock

[Aaron Liu]

The only reason I needed two sides is that you can arrive at a game with either player to move

[Violeta Hernández]

Why do we need the (f x).2.isSome condition, though?

[Aaron Liu]

So you can't just supply fun _ => (none, none)

[Aaron Liu]

This satisfies all the other conditions

[Violeta Hernández]

Oh, of course. Your clock needs to at the very least consider every position that right could get to under this strategy.

[Violeta Hernández]

And for that it's sufficient that it considers x itself.

[Violeta Hernández]

This is a very elegant definition. I wouldn't mind just going ahead and calling this a strategy.

[Aaron Liu]

I guess it is a strategy

[Violeta Hernández]

(I'm a bit confused though, are strategies in the literature supposed to win? Or just survive?)

[Aaron Liu]

It's a strategy to win

[Aaron Liu]

You can probably cook up a different definition for a strategy to survive

[Tristan Figueroa-Reid]

Strategies in the literature can either win or survive (you can define a variant for either one, so this construction seems natural).

[Violeta Hernández]

Aaron Liu said:

You can probably cook up a different definition for a strategy to survive

Do we need to? Left survives if there exists no winning strategy for right.

[Aaron Liu]

We don't need to

[Aaron Liu]

But we can do it

[Aaron Liu]

It could be useful

[Tristan Figueroa-Reid]

Defining (a surviving strategy) using the existing winning strategy, then adding a theorem that defines it directly seems nicer from a trusted code perspective.

[Aaron Liu]

Surviving strategies are simpler

[Aaron Liu]

They don't have ordinals since there's no need to force an end

[Aaron Liu]

It's just a set of games satisfying some properties

[Tristan Figueroa-Reid]

Then perhaps we can define winning strategies from surviving strategies? A winning strategy for Left is when Left survives but Right doesn't.

[Aaron Liu]

Well, two sets

[Aaron Liu]

You can also drop the second set

[Aaron Liu]

Just like you can define LE without LF

[Violeta Hernández]

Can you type that down?

[Aaron Liu]

"right goes first and left survives"

∃ s : Set LGame.{u}, x ∈ s ∧ ∀ y ∈ s, ∀ z ∈ y.rightMoves, ∃ r ∈ z.leftMoves, r ∈ s

[Aaron Liu]

you can probably define it coinductively

[Aaron Liu]

wasn't there some sort of greatest_fixpoint thing?

[Violeta Hernández]

Coinductive types are primitives in Coq, not in Lean

[Aaron Liu]

lean4#8097

[Violeta Hernández]

This is news to me

[Aaron Liu]

I haven't touched Coq (or Rocq) so I wouldn't be confusing it

[Violeta Hernández]

Aaron Liu said:

"right goes first and left survives"

∃ s : Set LGame.{u}, x ∈ s ∧ ∀ y ∈ s, ∀ z ∈ y.rightMoves, ∃ r ∈ z.leftMoves, r ∈ s

Oh, I get it. s is precisely the set in which the partial function of the strategy is defined.

[Violeta Hernández]

This does smell coinductive to me, but I don't know what we'd gain out of defining it as a coinductive predicate.

[Aaron Liu]

The coinduction?

[Aaron Liu]

I guess we already get the coinduction

[Violeta Hernández]

What would coinduction say here?

[Aaron Liu]

It's exactly the Exists.intro on the definition I put above

[Violeta Hernández]

Hm yeah that makes sense

[Aaron Liu]

I've just realized the construction I have is essentially what Tarski's fixpoint theorem tells you

[Aaron Liu]

All that's left is to prove it's a fixpoint

[Violeta Hernández]

Not sure what you mean by that.

[Violeta Hernández]

This is genuinely so nice.

def LeftStrategy (x : LGame) (s : Set LGame) : Prop :=
  x ∈ s ∧ ∀ y ∈ s, ∀ z ∈ y.rightMoves, ∃ r ∈ z.leftMoves, r ∈ s

def LeftSurvivesSnd (x : LGame) : Prop :=
  ∃ s, LeftStrategy x s

def LeftSurvivesFst (x : LGame) : Prop :=
  ∃ y ∈ x.leftMoves, LeftSurvivesSnd y

[Violeta Hernández]

I think we should now consider API.

[Violeta Hernández]

I think something important is to link these definitions to IGame. Prove that LeftSurvivesSnd (toLGame x) ↔ 0 ≤ x and LeftSurvivesFst (toIGame x) ↔ 0 ⧏ x.

[Violeta Hernández]

We should also prove that either left or right survives any given game.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think we should now consider API.

I think I am in favor of just defining a bunch of explicitly-named definitions for surviving/outcomes, in hopes that Left/RightSurvivesFst/Snd, and their tie and win variants eventually become either notation or auxiliary.

[Violeta Hernández]

I'm unsure if we need tie/win variants.

[Violeta Hernández]

I think we could introduce notation on top of this. Define leftOutcome x as either of L, D, or R. Likewise for rightOutcome. And then we get our outcome function by taking the product of these linear orders.

[Violeta Hernández]

So maybe instead of LeftSurvivesSnd x we simply write D ≤ rightOutcome x.

[Violeta Hernández]

Yeah, the API should definitely be written in terms of this outcome function.

[Tristan Figueroa-Reid]

Hm, it being given a linear order feels a little confusing when trying to differentiate between left and right outcomes.

[Tristan Figueroa-Reid]

(Though I suppose this is fine since the scope of left/rightOutcome would be near auxiliary)

[Aaron Liu]

what instead then?

[Tristan Figueroa-Reid]

Aaron Liu said:

what instead then?

Two distinct enums for each left and right outcome with explicit conversions between the two, which would make ordering quickly canonical for each one. Again, though, that is a lot for this small-scoped construction.

[Violeta Hernández]

Should left/rightOutcome be auxiliary? I feel like in a sense they're more natural definitions than outcome itself.

[Tristan Figueroa-Reid]

They are more natural, but I was under the impression that outcome itself was very auxiliary.

[Violeta Hernández]

I'm pretty sure outcome is what this entire theory is all about!

[Tristan Figueroa-Reid]

It is! Though outside of outcome itself, LGame would mainly be using outcome through *LGame ordering?

[Violeta Hernández]

I don't think so. In the case of IGame the four outcomes very neatly correspond to the four possible order relations a game can have with zero. With LGame there's nine outcomes, and there's no such known characterization.

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

Aaron Liu said:

what instead then?

Two distinct enums for each left and right outcome with explicit conversions between the two, which would make ordering quickly canonical for each one. Again, though, that is a lot for this small-scoped construction.

I think we get a slightly nicer API if we have two distinct enums, and our final outcome enum be the 9 possible outcomes, where we can then define the usual lattice on loopy outcomes.

[Violeta Hernández]

I don't really see what we get out of duplicating our outcome order.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I don't really see what we get out of duplicating our outcome order.

Just to clearly type-differentiate between the left/right outcomes. I don't really see a benefit when we don't differentiate.

[Violeta Hernández]

Presumably there's little ambiguity as is? leftOutcome and rightOutcome tell you outright. As for the outcome function, the left entry would be leftOutcome, and the right entry would be rightOutcome. You don't even need a mnemonic for that one.

[Aaron Liu]

Not like intent and extent

[Tristan Figueroa-Reid]

Violeta Hernández said:

Presumably there's little ambiguity as is? leftOutcome and rightOutcome tell you outright. As for the outcome function, the left entry would be leftOutcome, and the right entry would be rightOutcome. You don't even need a mnemonic for that one.

I forgot that we'll know the origin of our data as we're working in a theorem prover. :+1:

[Violeta Hernández]

I'm thinking, LeftStrategy and RightStrategy can be public API. We'll then keep everything private until we can define the outcome function, and state all the results on outcomes in terms of it.

[Violeta Hernández]

So, how do we actually prove this?

private theorem left_or_right_survive_left (x : LGame) :
    (∃ y ∈ x.leftMoves, ∃ s, LeftStrategy y s) ∨ ∃ s, RightStrategy x s := by
  sorry

[Aaron Liu]

It's probably probable

[Aaron Liu]

*provable

[Aaron Liu]

If you put it on a branch I can attempt it today

[Violeta Hernández]

Way ahead of you
https://github.com/vihdzp/combinatorial-games/tree/vi.outcome

[Violeta Hernández]

I gtg, I'll come back to this in a few hours

[Aaron Liu]

I have an idea

[Violeta Hernández]

I'm interested

[Violeta Hernández]

I was thinking about this as well

[Violeta Hernández]

My class doesn't start for another eight minutes

[Aaron Liu]

you have class???

[Violeta Hernández]

I'm a uni student yeah

[Aaron Liu]

this is more complicated than I thought

[Violeta Hernández]

There's probably some auxiliary theorems you need to prove first

[Violeta Hernández]

Like, if there's a LeftStrategy for x, there's one for some left move of every right move of x.

[Violeta Hernández]

In fact this should be an iff

[Aaron Liu]

Here's what I'm thinking about

noncomputable
def stoppingTimeLeftApprox : (LGame.{u} → WithTop NatOrdinal.{u} × WithTop NatOrdinal.{u}) →o
    (LGame.{u} → WithTop NatOrdinal.{u} × WithTop NatOrdinal.{u}) where
  toFun f x := (⨅ i ∈ x.leftMoves, (f i).2, ⨆ i ∈ x.rightMoves, (f i).1 + 1)
  monotone' := sorry

noncomputable
def stoppingTimeRightApprox : (LGame.{u} → WithTop NatOrdinal.{u} × WithTop NatOrdinal.{u}) →o
    (LGame.{u} → WithTop NatOrdinal.{u} × WithTop NatOrdinal.{u}) where
  toFun f x := (⨆ i ∈ x.leftMoves, (f i).2 + 1, ⨅ i ∈ x.rightMoves, (f i).1)
  monotone' := sorry

theorem consistent_le_closed_left {x y}
    (hx : x ≤ stoppingTimeLeftApprox x)
    (hy : stoppingTimeLeftApprox y ≤ y) :
    x ≤ y := sorry

theorem consistent_le_closed_right {x y}
    (hx : x ≤ stoppingTimeRightApprox x)
    (hy : stoppingTimeRightApprox y ≤ y) :
    x ≤ y := sorry

theorem lfp_eq_gfp_left : stoppingTimeLeftApprox.lfp = stoppingTimeLeftApprox.gfp := sorry
theorem lfp_eq_gfp_right : stoppingTimeRightApprox.lfp = stoppingTimeRightApprox.gfp := sorry

/--
The ordinal corresponding to the time it takes for left to force a win going first,
counted in right moves.
-/
noncomputable
def stoppingTimeLeftLeft (x : LGame.{u}) : WithTop NatOrdinal.{u} :=
  (stoppingTimeLeftApprox.lfp x).1

/--
The ordinal corresponding to the time it takes for left to force a win going second,
counted in right moves.
-/
noncomputable
def stoppingTimeLeftRight (x : LGame.{u}) : WithTop NatOrdinal.{u} :=
  (stoppingTimeLeftApprox.lfp x).2

/--
The ordinal corresponding to the time it takes for right to force a win going second,
counted in left moves.
-/
noncomputable
def stoppingTimeRightLeft (x : LGame.{u}) : WithTop NatOrdinal.{u} :=
  (stoppingTimeRightApprox.lfp x).1

/--
The ordinal corresponding to the time it takes for right to force a win going first,
counted in left moves.
-/
noncomputable
def stoppingTimeRightRight (x : LGame.{u}) : WithTop NatOrdinal.{u} :=
  (stoppingTimeRightApprox.lfp x).2

[Aaron Liu]

I hope all the sorrys are actually true

[Aaron Liu]

I didn't check that carefully

[Junyan Xu]

For loopy games you can still define winning positions as an inductive predicate. These should be contained in the surviving positions (i.e. those contained in some strategy). The right surviving positions should be the complement of the left winning positions.

[Aaron Liu]

My reasoning is: if you prove the least and greatest fixpoints are equal, then you can use both induction and coinduction

[Violeta Hernández]

Aaron Liu said:

I hope all the sorrys are actually true

I've no idea

[Violeta Hernández]

I admit I liked the other definition we had better.

[Aaron Liu]

but you get an ordinal out this way

[Aaron Liu]

that's more information than just "yes" or "no"

[Violeta Hernández]

These are nice definitions, assuming they work. But perhaps they should be a separate development from strategies.

[Aaron Liu]

maybe

[Aaron Liu]

but you can directly extract a strategy from them

[Violeta Hernández]

Violeta Hernández said:

Way ahead of you
https://github.com/vihdzp/combinatorial-games/tree/vi.outcome

I think I know how to prove this. You need two lemmas:

• A game has a left strategy iff every right move has a left move with a left strategy. Simple enough.
• If every right move of a game has no right strategy, then the game has a left strategy. The left strategy is really silly: for every single game with no right strategy, take an arbitrary left move such that every right move has no right strategy.

[Violeta Hernández]

Aaron Liu said:

but you can directly extract a strategy from them

The more I think about it the more I like your idea. It feels weird to use this to define strategies rather than the much easier set definition. But it might be worth putting this in its own file.

[Violeta Hernández]

Surely, surely this definition exists somewhere in the literature?

[Violeta Hernández]

(again, assuming it works)

[Aaron Liu]

I don't read enough literature to know if this exists somewhere

[Violeta Hernández]

Glad we have our resident reader @Tristan Figueroa-Reid

[Junyan Xu]

It's interesting that Lean doesn't accept this inductive predicate:

inductive IsLeftWinning : LGame → Prop
  | intro (x : LGame) : (∀ y ∈ x.rightMoves, ∃ z ∈ y.leftMoves, IsLeftWinning z) → IsLeftWinning x
/- (kernel) invalid nested inductive datatype 'Exists', nested inductive datatypes parameters cannot contain local variables. -/

In principle this is similar to docs#Acc. Let me think of another way to construct it ...

[Junyan Xu]

If I break it down then it works:

inductive IsLeftWinning : LGame → Prop where
  | intro (x : LGame) (f : ∀ y ∈ x.rightMoves, LGame) :
      (∀ y (hy : y ∈ x.rightMoves), f y hy ∈ y.leftMoves) →
      (∀ y (hy : y ∈ x.rightMoves), IsLeftWinning (f y hy)) → IsLeftWinning x

[Violeta Hernández]

Interesting! Yeah, this seems like it should work.

[Violeta Hernández]

I think it's by far the most natural definition in this thread.

[Violeta Hernández]

Presumably we can prove whatever the inductive principle for the exists version should be.

[Aaron Liu]

what about the coinductive principle

[Violeta Hernández]

I don't think this definition is supposed to be coinductive?

[Aaron Liu]

there is an inductive definition and a coinductive definition and they are complements

[Aaron Liu]

I think

[Violeta Hernández]

I think the coinductive version might correspond to games that left survives

[Aaron Liu]

yes that's what I was thinking I think

[Aaron Liu]

not sure anymore

[Violeta Hernández]

I mean, as nice as it would be to have this inductive/coinductive duality

[Violeta Hernández]

We really only need one or the other

[Aaron Liu]

I'm trying to prove it right now

[Violeta Hernández]

Oh nice

[Junyan Xu]

proven half of it
image.png

[Junyan Xu]

I changed the definition of LeftStrategy in order to state leftStrategy_iUnion to prove a key lemma isLeftSurviving_iff_forall:
image.png

[Aaron Liu]

I did it!

[Aaron Liu]

now for the easy part

[Junyan Xu]

I just pushed a proof of left_or_right_survive_left at this branch

[Aaron Liu]

I proved stoppingTimeLeftApprox.lfp = stoppingTimeLeftApprox.gfp

[Aaron Liu]

I might make a PR

[Violeta Hernández]

I'm not opposed to having these definitions in the repo, because they do seem like pretty natural notions (they straightforwardly generalize the number of moves left in a short game). But I would prefer to first see them used somewhere else. That would then inform the names of definitions and the results to be proven.

[Aaron Liu]

I have never seen these used anywhere I saw them once in The Search for the Longest Infinite Chess Game

[Violeta Hernández]

Holy **** you're right they're exactly that!

[Violeta Hernández]

Well actually I'm not sure if they're exactly that

[Aaron Liu]

might be off by one in some places

[Violeta Hernández]

https://neugierde.github.io/cantors-attic/Omega_one_chess

[Violeta Hernández]

(deleted)

[Violeta Hernández]

There's a mismatch in definitions. You measure the left stopping time in terms of right moves, while that definition measures it in terms of left moves

[Aaron Liu]

yes that is true

[Aaron Liu]

off by one in some places

[Violeta Hernández]

And now we play the game of figuring out which definition is better

[Aaron Liu]

I will of course advocate for my definition

[Aaron Liu]

its range is Set.univ

[Violeta Hernández]

Does the other one not have that property?

[Aaron Liu]

it doesn't hit ω

[Aaron Liu]

if white is to move

[Aaron Liu]

white to move misses all the limit ordinals

[Aaron Liu]

black to move hits everything

[Violeta Hernández]

Huh

[Violeta Hernández]

To be frank, I also find "supremum of the successors" to be a more mathematically satisfying definition than "successor of the supremum".

[Aaron Liu]

It's an infimum though

[Violeta Hernández]

Huh

[Aaron Liu]

infimum over all possible moves of how long to kill the opponent in each position

[Aaron Liu]

since you always choose the best move which is the minimum time to kill

[Violeta Hernández]

No you wrote down supremum of the succesors

[Violeta Hernández]

Supremum is the union thing isn't it

[Aaron Liu]

that's the other one

[Aaron Liu]

supremum over all the positions of how long to die

[Violeta Hernández]

Hm yeah the thing is that the "successor of supremum" definition is the one used in the article
https://arxiv.org/pdf/1302.4377

[Violeta Hernández]

Do we know that these definitions are only off by one?

[Aaron Liu]

I know they are only off by one

[Junyan Xu]

Supremum of successors sound more natural as it's also used in PSet.rank.

[Junyan Xu]

I'm currently working on outcomes that incorporate misere play convention
image.png

[Junyan Xu]

Just recording that this also doesn't work with a different error message:

inductive IsLeftWinning : LGame → Prop where
  | intro' (x : LGame) :
      (∀ y ∈ x.rightMoves, ¬ (∀ z ∈ y.leftMoves, ¬ IsLeftWinning z)) → IsLeftWinning x
/- (kernel) arg #2 of 'LGame.IsLeftWinning.intro'' has a non positive occurrence of the datatypes being declared -/

[Aaron Liu]

Yeah

[Aaron Liu]

There are reasons

[Violeta Hernández]

Junyan Xu said:

I'm currently working on outcomes that incorporate misere play convention
image.png

Does the toMisere idea I had earlier not work here? Take any state without moves for some player and add a single move for that player to 0

[Aaron Liu]

This one happens to work out but if you modify it slightly you get a contradiction

[Junyan Xu]

It doesn't seem possible to make IsLeftWinning and IsRightLosing mutual recursives either.

[Aaron Liu]

I have something just as good

[Aaron Liu]

It's the stopping times I proved yesterday

[Junyan Xu]

Violeta Hernández said:

Does the toMisere idea I had earlier not work here? Take any state without moves for some player and add a single move for that player to 0

Yes, I think it works and is a better solution!

[Junyan Xu]

It's the stopping times I proved yesterday

If you want to prove something about the "stopping time" you might start with some hydra game which should be easier to formalize than chess. And we can certainly show e.g. that the left stopping time isn't top iff IsLeftWinning.

[Junyan Xu]

Junyan Xu said:

It doesn't seem possible to make IsLeftWinning and IsRightLosing mutual recursives either.

Oops I was wrong, this actually works

mutual
  inductive IsLeftWinning : LGame → Prop where
    | intro (x : LGame) : (∀ y ∈ x.rightMoves, IsRightLosing y) → IsLeftWinning x
  inductive IsRightLosing : LGame → Prop where
    | intro (x y : LGame) : y ∈ x.leftMoves → IsLeftWinning y → IsRightLosing x
end

[Aaron Liu]

Junyan Xu said:

It's the stopping times I proved yesterday

If you want to prove something about the "stopping time" you might start with some hydra game which should be easier to formalize than chess. And we can certainly show e.g. that the left stopping time isn't top iff IsLeftWinning.

I proved something about the stopping times of loopy games (that you can do both induction and coinduction)

[Junyan Xu]

Using mutual inductives shortens the code a bit. The same definition works also for IGame and in fact for ConcreteGame as well. For IGames we should show that IsLeftSurviving is the same as IsLeftWinning, or maybe we should show this for any position such that the union of the left and right relations (or the appropriate composition of the left and right relations) is well founded on its subpositions.

[Junyan Xu]

Pushed a proof of theorem mem_range_toLGame_iff_acc {x : LGame} : x ∈ range IGame.toLGame ↔ Acc LGame.IsOption x

[Junyan Xu]

Opened PR#179 for loopy outcomes.

[Junyan Xu]

I'm considering dropping the IsLeft/RightSurviving definitions since they're equivalent to the negation of IsLeft/RightLosing. I think it's also more intuitive to switch left and right so that whenever a decl name mentions "left", it always means that left is going first rather than second.

[Violeta Hernández]

I'll check it out in a bit.