Zulip Chat Archive

Stream: new members

Topic: Well founded recursion with universes


view this post on Zulip 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,
    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

view this post on Zulip Scott Morrison (Aug 10 2020 at 01:59):

#mwe, or a branch to look at?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 10 2020 at 10:38):

As currently stated, the theorem is false.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 10 2020 at 10:40):

Right, which is wrong.

view this post on Zulip Fox Thomson (Aug 10 2020 at 10:40):

How come?

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 10 2020 at 10:41):

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

view this post on Zulip Fox Thomson (Aug 10 2020 at 10:41):

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

view this post on Zulip 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.

view this post on Zulip Fox Thomson (Aug 10 2020 at 10:43):

Thank you, I will try

view this post on Zulip 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

view this post on Zulip 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,
    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}

view this post on Zulip 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}

view this post on Zulip 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}

view this post on Zulip Fox Thomson (Aug 10 2020 at 14:05):

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

view this post on Zulip Reid Barton (Aug 10 2020 at 14:06):

As the type of Grundy_value I mean

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 10 2020 at 14:10):

Lean doesn't work that way

view this post on Zulip Reid Barton (Aug 10 2020 at 14:11):

I agree in normal math you could do it

view this post on Zulip Fox Thomson (Aug 10 2020 at 14:11):

Is there any known tricks to get around this?

view this post on Zulip Reid Barton (Aug 10 2020 at 14:11):

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

view this post on Zulip Reid Barton (Aug 10 2020 at 14:11):

actually I'm not really sure whether that is true

view this post on Zulip Reid Barton (Aug 10 2020 at 14:12):

but if you have this problem then something went wrong earlier

view this post on Zulip Reid Barton (Aug 10 2020 at 14:16):

Why would you need this?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 10 2020 at 14:17):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip Reid Barton (Aug 10 2020 at 14:18):

Only one universe is needed

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:23):

o.out.α has the right size


Last updated: May 16 2021 at 05:21 UTC