# Zulip Chat Archive

## 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,
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 (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.

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

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,
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 (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