negating games

Stream: lean4

[Kevin Buzzard]

I was playing with the idea of "finite pre-games" in Lean, because I am writing a talk on Number for a conference next week. There's no reason not to try it in Lean 4. Notation is amazing. You define something and you instantly make notation for it and then you can use it immediately afterwards in everything (e.g. equation compiler).

But the equation compiler and I are not getting on with neg:

/-- Conway-type games with the `List` monad. -/
inductive list_game
| mk : List list_game → List list_game → list_game

-- notation for the constructor of `list_game`
syntax "{" term "∣" term "}" : term

-- definition of the notation
macro_rules
| `({ $L ∣ $R}) => `(list_game.mk $L $R)

namespace list_game

def neg : list_game → list_game
| { L ∣ R } => { R.map neg ∣ L.map neg}
/-
fail to show termination for
  neg
with errors
structural recursion cannot be used

well founded recursion has not been implemented yet
-/

end list_game

I suspect I can make it directly with the recursor but I confess I haven't tried yet. I wondered whether the equation compiler could be persuaded or whether this is still a WIP or even not possible for some good reason

[Eric Wieser]

Doesn't lean3 notation work just as well for this example?

[Daniel Fabian]

you can in fact be a bit naughty and use notation even in the definition itself:

set_option hygiene false in
infixl:40 " ==> " => step
inductive step : tm → tm → Prop :=
  | ST_PlusConstConst : ∀ n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : ∀ t1 t1' t2,
      t1 ==> t1' →
      P t1 t2 ==> P t1' t2
  | ST_Plus2 : ∀ n1 t2 t2',
      t2 ==> t2' →
      P (C n1) t2 ==> P (C n1) t2'

[Kevin Buzzard]

I think in lean 3 you'd need brackets around a notation constructor

[Kevin Buzzard]

I'm a bit confused about which monads all this works for. I think option and list are fine for neg, and set you can't make the type because of mk univ univ

[François G. Dorais]

It works if you avoid the nested inductive:

inductive Game
| nil : Game
| consL : Game → Game → Game
| consR : Game → Game → Game

def Game.neg : Game → Game
| nil => nil
| consL a b => consR (neg a) (neg b)
| consR a b => consL (neg a) (neg b)

[Scott Morrison]

From memory this is identical behaviour to Lean3.

[Kevin Buzzard]

This is a different definition of Game, as far as I can see. Edit: Oh, I see!

[Kevin Buzzard]

I made my recursor anyway, so I can continue:

noncomputable def useful_recursor (g : game) (motive : game → Type u)
  (IH : ∀ x, (∀y, y ∈ xᴸ → motive y) → (∀ y, y ∈ xᴿ → motive y) → motive x) : motive g :=
by
  apply g.rec (λ LL RR (hL : ∀ y, y ∈ LL → motive y) (hR : ∀ y, y ∈ RR → motive y) =>
    IH {LL ∣ RR} hL hR);
  { exact λ g hg => False.elim $ List.not_mem_nil g hg };
  { intros h T hh hT g hg;
    rw [List.mem_cons_iff g h T] at hg;
    have hdone : ∃ x : motive g, true := match hg with
    | Or.inl h => ⟨h ▸ hh, rfl⟩
    | Or.inr h => ⟨hT _ h, rfl⟩;
    exact Classical.choose hdone };

[Kevin Buzzard]

Wait, this _is_ a different definition of Game, because consL and consR don't commute with this definition. However this is not really a game, because there are other much stronger definitions of "equality" that you want to put on this type, so perhaps it doesn't matter.

[Scott Morrison]

Yes, you're going to be quotienting later anyway, so it's not mathematically important exactly which "pregame" you use. Using a list rather than an indexing type is a bit weird, however. :-)

[Kevin Buzzard]

I was just experimenting with this stuff, because you suggested a while ago that in my talk about numbers I could use Conway's numbers as an example, but I was trying to make the definition look conceptual whilst still giving me enough to get the naturals.