Well founded recursion with universes

Stream: new members

[Fox Thomson]

I am attempting to prove the Spauge-Grundy theorem which I am stating as

theorem Sprague_Grundy : ∀ (G : pgame.{u+2}) [G.impartial], inhabited { O : ordinal.{u+1} // G ≈ nim O }

In order to prove this I need to induct on G using the pgame.pgame_wf_tac tactic and using the theorem on G.move_left i for some left move i but I am getting an error about universe levels which I think is due to the subsequent games being of type pgame.{u+1}. How can I make a more flexible universe variable?
My attempted proof and related definitions is here:

def nonmoves {α : Type _} (M : α → ordinal.{u}) : set ordinal.{u+1} := { O : ordinal | ¬ ∃ a : α, ordinal.lift.{u (u+1)} (M a) = O }

lemma nonmoves_nonempty {α : Type _} (M : α → ordinal.{u}) : ∃ O : ordinal, O ∈ nonmoves M :=
begin
    have h : ¬ ∃ a, ordinal.lift.{u (u+1)} (M a) = ordinal.lift.principal_seg.{u (u+1)}.top,
    rintro ⟨ a, ha ⟩,
    have down := ordinal.lift.principal_seg.{u (u+1)}.down (ordinal.lift.{u (u+1)} (M a)),
    have h' : ∃ (b : ordinal), ordinal.lift.principal_seg.{u (u+1)} b = (ordinal.lift.{u (u+1)} (M a)),
        use M a,
        rw ordinal.lift.principal_seg_coe,
    have hcontra := down.2 h',
    have h := (lt_iff_le_and_ne.1 hcontra).2,
    contradiction,
    use ordinal.lift.principal_seg.{u (u+1)}.top
end

theorem Sprague_Grundy : ∀ (G : pgame.{u+2}) [G.impartial], inhabited { O : ordinal.{u+1} // G ≈ nim O }
| G :=
begin
    classical,
    introI,
    let M := λ i, (Sprague_Grundy (G.move_left i)).default.val,
    fconstructor,
    fconstructor,
    have S := nonmoves M,
    apply ordinal.omin,
    exact nonmoves_nonempty M,
    -- exact ordinal.omin.{u+1} (nonmoves M) (nonmoves_nonempty M)
    sorry,
end

[Scott Morrison]

#mwe, or a branch to look at?

[Scott Morrison]

Without catching on what you've been doing, it's hard to say. The fact that G.impartial is a typeclass strikes me as unlikely to be a good choice, however!

[Fox Thomson]

@Scott Morrison I have made a GitHub repository at https://github.com/foxthomson/impartial. The problem is in src/nim.lean.

[Reid Barton]

Why isn't your theorem statement simply

theorem Sprague_Grundy : ∀ (G : pgame.{u}) [G.impartial], inhabited { O : ordinal.{u} // G ≈ nim O }

with a single universe level? I think the issue is in your definition of nim.

[Reid Barton]

As currently stated, the theorem is false.

[Reid Barton]

def nim : ordinal → pgame
| O₁ := ⟨ { O₂ : ordinal // O₂ < O₁ },

this construction is tempting, but it blows up the universe level unnecessarily.

[Fox Thomson]

If O is ordinal.{u} then ordinals less than O are in the universe u. This means that nim O is in the universe u+1.

[Reid Barton]

Right, which is wrong.

[Fox Thomson]

How come?

[Reid Barton]

If O : ordinal.{u} then O is the order type of some type in Type u, and that's the correct universe level to be in

[Reid Barton]

{ O₂ : ordinal // O₂ < O₁ } has the same order type but it's in Type (u+1)

[Fox Thomson]

So I should try to get the order type out of the quotient?

[Reid Barton]

Yeah, if you can define nim directly as a game, you could try to use lift, otherwise use quot.out in some form.

[Fox Thomson]

Thank you, I will try

[Reid Barton]

Another thing you could maybe do is have nim take a well-ordered type, rather than an ordinal

[Fox Thomson]

I have a #mwe which does not depend on nim at all

import set_theory.ordinal
import set_theory.pgame
import tactic.nth_rewrite.default

universes u v

namespace pgame

local infix ` ≈ ` := pgame.equiv

@[class] def impartial : pgame → Prop
| G := G ≈ -G ∧ (∀ i, impartial (G.move_left i)) ∧ (∀ j, impartial (G.move_right j))
using_well_founded {dec_tac := pgame_wf_tac}

@[simp] lemma impartial_def {G : pgame} :
    G.impartial ↔ G ≈ -G ∧ (∀ i, impartial (G.move_left i)) ∧ (∀ j, impartial (G.move_right j)) :=
begin
    split,
    {   intro hi,
        unfold1 impartial at hi,
        exact hi },
    {   intro hi,
        unfold1 impartial,
        exact hi }
end

@[instance] lemma impartial_move_left_impartial {G : pgame} [h : G.impartial] (i : G.left_moves) : impartial (G.move_left i) :=
begin
    rw impartial_def at h,
    exact h.2.1 i,
end

def nonmoves {α : Type _} (M : α → ordinal.{u}) : set ordinal.{u+1} := { O : ordinal | ¬ ∃ a : α, ordinal.lift.{u (u+1)} (M a) = O }

lemma nonmoves_nonempty {α : Type _} (M : α → ordinal.{u}) : ∃ O : ordinal, O ∈ nonmoves M :=
begin
    have h : ¬ ∃ a, ordinal.lift.{u (u+1)} (M a) = ordinal.lift.principal_seg.{u (u+1)}.top,
    rintro ⟨ a, ha ⟩,
    have down := ordinal.lift.principal_seg.{u (u+1)}.down (ordinal.lift.{u (u+1)} (M a)),
    have h' : ∃ (b : ordinal), ordinal.lift.principal_seg.{u (u+1)} b = (ordinal.lift.{u (u+1)} (M a)),
        use M a,
        rw ordinal.lift.principal_seg_coe,
    have hcontra := down.2 h',
    have h := (lt_iff_le_and_ne.1 hcontra).2,
    contradiction,
    use ordinal.lift.principal_seg.{u (u+1)}.top
end

def Grundy_value : Π (G : pgame.{u}) [G.impartial], ordinal.{u+1}
| G :=
begin
    introI,
    let M := λ i, Grundy_value (G.move_left i),
    exact ordinal.omin (nonmoves M) (nonmoves_nonempty M),
end

end pgame

I am getting an error as M in Grundy_value is of the form G.left_moves -> ordinal.{u+1} so nonmoves M is a set of ordinal.{u+2} a universe too big. I think I am loking for a way to write ordinal.{2*u}

[Fox Thomson]

Actually I think it is due to Grundy_value not stepping down a universe when it is used recursively, Lean has understood M as a function from G.left_moves to ordinal.{u+1} when I want it to be sent to ordinal.{u}

[Reid Barton]

Well you wrote Π (G : pgame.{u}) [G.impartial], ordinal.{u+1}--it should take values in ordinal.{u}

[Fox Thomson]

Which should work as G.move_left i is a member of pgame.{u-1}

[Reid Barton]

As the type of Grundy_value I mean

[Fox Thomson]

I want it to take values in the universe u understood as a variable so I can call it with each universe a level down

[Reid Barton]

You can't do recursion with varying universe levels, but in any case, the Grundy value of a game is supposed to be an ordinal in the same universe as the game

[Reid Barton]

for example an "ordinary" game is one that lives in universe level 0, and its Grundy value is an ordinary ordinal which also lives in universe level 0

[Fox Thomson]

But if I have shown that all ordinary games have a Grundy value shouldn't I be able to access their Grundy value viewed as an ordinary ordinal when talking about universe 1 games?

[Reid Barton]

Lean doesn't work that way

[Reid Barton]

I agree in normal math you could do it

[Fox Thomson]

Is there any known tricks to get around this?

[Reid Barton]

I claim it's impossible to actually have this problem in Lean

[Reid Barton]

actually I'm not really sure whether that is true

[Reid Barton]

but if you have this problem then something went wrong earlier

[Reid Barton]

Why would you need this?

[Fox Thomson]

The S-G theorem requires nonmoves to be able to find the mex. This requires nonmoves to be nonempty so nonmoves has to be defined as a set of ordinal.{u+1} otherwise we could feed it the identity function on ordinal.{u} and it would be empty.

[Reid Barton]

I think nonmoves also has the wrong result universe level, it should be set ordinal.{u}.

[Fox Thomson]

This means that the Grundy value has to be strictly universe higher than the Grundy value of all subsequent games

[Reid Barton]

There's no way to index all of ordinal.{u} with a Type u-sized family--but there is a theorem to be proved here!

[Reid Barton]

No, you can't do it that way in Lean (and you wouldn't do it that way in math either)

[Reid Barton]

Only one universe is needed

[Reid Barton]

The classical way to describe the situation would be: to an impartial game we assign the least ordinal which is not the value of any option of the game; such an ordinal exists because ordinals form a proper class but the options of the game only form a set.

[Fox Thomson]

Oh, so saying alpha is type u means that nonmoves is nonempty without jumping up a universe

[Reid Barton]

I think there's a theorem to this effect somewhere in set_theory.ordinal or set_theory.cardinal

[Mario Carneiro]

I tried to make an API for this sort of construction, but I wasn't able to make anything sufficiently general to cover all the use cases. But you can get a type with the order type of the ordinal using quot.out, and use that

[Mario Carneiro]

o.out.α has the right size