Stream: new members

Topic: Well founded recursion with universes

Fox Thomson (Aug 09 2020 at 15:58):

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,
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 (Aug 10 2020 at 01:59):

#mwe, or a branch to look at?

Scott Morrison (Aug 10 2020 at 02:00):

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 (Aug 10 2020 at 10:27):

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

Reid Barton (Aug 10 2020 at 10:35):

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 (Aug 10 2020 at 10:38):

As currently stated, the theorem is false.

Reid Barton (Aug 10 2020 at 10:39):

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


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

Fox Thomson (Aug 10 2020 at 10:40):

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 (Aug 10 2020 at 10:40):

Right, which is wrong.

How come?

Reid Barton (Aug 10 2020 at 10:40):

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 (Aug 10 2020 at 10:41):

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

Fox Thomson (Aug 10 2020 at 10:41):

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

Reid Barton (Aug 10 2020 at 10:42):

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 (Aug 10 2020 at 10:43):

Thank you, I will try

Reid Barton (Aug 10 2020 at 10:47):

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

Fox Thomson (Aug 10 2020 at 13:49):

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,
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 (Aug 10 2020 at 14:04):

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 (Aug 10 2020 at 14:05):

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

Fox Thomson (Aug 10 2020 at 14:05):

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

Reid Barton (Aug 10 2020 at 14:06):

As the type of Grundy_value I mean

Fox Thomson (Aug 10 2020 at 14:07):

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 (Aug 10 2020 at 14:07):

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 (Aug 10 2020 at 14:08):

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 (Aug 10 2020 at 14:10):

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 (Aug 10 2020 at 14:10):

Lean doesn't work that way

Reid Barton (Aug 10 2020 at 14:11):

I agree in normal math you could do it

Fox Thomson (Aug 10 2020 at 14:11):

Is there any known tricks to get around this?

Reid Barton (Aug 10 2020 at 14:11):

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

Reid Barton (Aug 10 2020 at 14:11):

actually I'm not really sure whether that is true

Reid Barton (Aug 10 2020 at 14:12):

but if you have this problem then something went wrong earlier

Reid Barton (Aug 10 2020 at 14:16):

Why would you need this?

Fox Thomson (Aug 10 2020 at 14:16):

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 (Aug 10 2020 at 14:17):

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

Fox Thomson (Aug 10 2020 at 14:18):

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

Reid Barton (Aug 10 2020 at 14:18):

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 (Aug 10 2020 at 14:18):

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

Reid Barton (Aug 10 2020 at 14:18):

Only one universe is needed

Reid Barton (Aug 10 2020 at 14:19):

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 (Aug 10 2020 at 14:20):

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

Reid Barton (Aug 10 2020 at 14:22):

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

Mario Carneiro (Aug 10 2020 at 19:21):

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 (Aug 10 2020 at 19:23):

o.out.α has the right size

Last updated: May 16 2021 at 05:21 UTC