Issues defining Combinatorial game

Stream: Is there code for X?

[Jelmer Firet]

I am stuck trying to define combinatorial games. I know there is PGame in mathlib, I mainly want to know why the following don't work.

structure Game : Type where
  left : Set Game
  right : Set Game
  birthday : Nat
  left_desc : ∀ Gl ∈ left, Gl.birthday < birthday
  right_desc : ∀ Gr ∈ right, Gr.birthday < birthday

This gives two types of errors:

1. left and right have a non-positive occurrence of the datatypes being declared. This one I kinda understand and in PGame they work around it by having a indexing set leftMoves and a function from the indexing set to the actual games playLeft
   2.

Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  Gl
has type `Game` which does not have the necessary form.

Error code: lean.invalidField

This one I don't get. My aim is to make sure that the left and right moves are "defined earlier" in some sense. Why is the birthday field not accessible for the children?

---

To sidestep this first issue I decided to just make the things I want an axiom. Then I tried to define addition:

axiom Game : Type
axiom Game.left (G : Game) : Set Game
axiom Game.right (G : Game) : Set Game
axiom Game.mk (left : Set Game) (right : Set Game) : Game
axiom Game.birthday (G : Game) : Nat
axiom Game.left_desc (G : Game) : ∀ Gl ∈ G.left, Gl.birthday < G.birthday
axiom Game.right_desc (G : Game) : ∀ Gr ∈ G.right, Gr.birthday < G.birthday

noncomputable def Game.add (G H : Game) : Game := by {
  apply Game.mk
  exact {add Gl H | Gl ∈ G.left} ∪ {add G Hl | Hl ∈ H.left}
  exact {add Gr H | Gr ∈ G.right} ∪ {add G Hr | Hr ∈ H.right}
}
termination_by G.birthday + H.birthday
decreasing_by {
  -- G H Gl : Game
  -- ⊢ Gl.birthday + H.birthday < G.birthday + H.birthday
  simp
  -- ⊢ Gl.birthday < G.birthday
  apply Game.left_desc
  -- ⊢ Gl ∈ G.left
  -- I would expect this goal to be in the context based on the set condition, but it isn't
}

Why did it not include the set condition Gl ∈ G.left in the context?

[Niels Voss]

As a quick note, you can use unsafe structure or unsafe inductive to bypass non-strict-positivity issues, just for testing purposes. I'm not quite sure how to fix your field projection issue; I think it is due to Game.birthday not actually being defined until after the inductive type is constructed. I suppose you could define a Pregame type and then define Game to be a Subtype of that.

I do get the goal ⊢ Gl ∈ G.left when I run your code, not sure why it isn't appearing for you.

As a side note, using tactic to construct data is not recommended, because tactics can have unpredictable or unstable behavior when it comes to what terms they produce.

[Robin Arnez]

I think what they meant is that they expected the goal to be solvable just from the fact that the definition contains the condition Gl ∈ G.left in {add Gl H | Gl ∈ G.left}. For that: you can use something like (Gl : Game) (_ : Gl ∈ G.left) instead:

noncomputable def Game.add (G H : Game) : Game :=
  Game.mk
    ({add Gl H | (Gl : Game) (_ : Gl ∈ G.left)} ∪ {add G Hl | (Hl : Game) (_ : Hl ∈ H.left)})
    ({add Gr H | (Gr : Game) (_ : Gr ∈ G.right)} ∪ {add G Hr | (Hr : Game) (_ : Hr ∈ H.right)})
termination_by G.birthday + H.birthday
decreasing_by all_goals simp_all [Game.left_desc, Game.right_desc]

[Kevin Buzzard]

Are you sure that you can't use these axioms to get a contradiction using some kind of diagonal argument? Axioms are a dangerous approach -- there is not a single axiom in mathlib, for example.

[Niels Voss]

You almost certainly can, just take the game g whose left set consists of all games, g := Game.mk Set.univ anything. Then, apply Game.left_desc to get that g.birthday < g.birthday.

[Jelmer Firet]

Thanks for your help.
I did not know about unsafe, and as this is purely for testing (I want to check some lemmas to further my understanding of Combinatorial Game Theory).
I did mean that Gl ∈ G.left did not show up in the assumptions. Specifying Gl and its membership seperately works.
But with unsafe the termination is not checked anyway so I have removed it.

[Aaron Liu]

in CGT we define CGT#IGame inductively as a having a left and right set of options which are docs#Small sets of games, which corresponds to the fact that you can't have a game with a proper class of options

[Violeta Hernández]

Just a reminder that docs#SetTheory.PGame and the material in Mathlib is about a year outdated, and will be removed shortly (the modules themselves have all been deprecated). The theory is currently getting developed in this other repository.

[Violeta Hernández]

But, to try to answer your actual question, you could try doing something like this instead:

inductive Game : Type u
  | mk (m n : ℕ) (f : Fin m → Game) (g : Fin n → Game) : SGame

The type of games you actually want will be some quotient of this by an extensionality relation. The birthday of a game can be then defined after the fact.

[Violeta Hernández]

The issue with your inductive type as written is that Lean cannot automatically verify that the construction is valid. If you were to remove the left_desc and right_desc conditions, it would not be valid: you'd have an injection left : Set Game → Game, which is impossible by Cantor's theorem. We had to do some technical sorcery with docs#QPF in the CGT repo to sidestep this: essentially we proved that there does exist some functor which behaves like the functor we'd want within an inductive definition like the following:

inductive Game : Type (u + 1) where
  ofSets (left : Set Game) (right : Set Game) [Small.{u} left] [Small.{u} right] : Game

And then we defined the type of games via docs#QPF.Fix. A nice consequence of this approach is that it gave us the type of loopy games for free via docs#QPF.Cofix.