WLOG/suffices and universe polymorphism

Stream: lean4

[Alex Meiburg]

I'm proving a theorem of the form,

theorem foobar.{u_1, u_2} {tx : Type u_1} {ty : Type u_2} : |some_func tx - some_func ty| <=
   other_func tx + other_func ty

Now what I really want to bother proving is that some_func tx - some_func ty <= other_func tx + other_func ty, and then I take the max on the left hand side, and swap x and y if needed. So I write something like

wlog h : some_func tx <= some_func ty

and then I want to use this ty tx to show this is sufficient. (Essentially identical logic if I use suffices manually instead of wlog).

But this doesn't work! Because the theorem statement has tx in universe u_1 and ty in universe u_2, so I can't pass ty into this because it's at the wrong universe level.

I tried manually doing it with suffices, but I can't see anyway to make the suffices statement universe polymorphic. (At the time I write the hypothesis, I have to instantiate particular universes; I can't use that hypothesis subsequently with different universe levels.) I tried doing suffices {tx : Type (max u_1 u_2)} or something but of course that didn't work either. I would ideally have something like,

suffices h.{u3,u4} :  ∀ {tx : u_3} {ty : u_4} ... by

or

have :  ∀ {u_3 : universes} {u_4 : universes} {tx : u_3} {ty : u_4} ... by

or something like that.

[Alex Meiburg]

I'm aware that one solution is "just pull out the thing you're proving and prove it in a separate theorem first".
But if that 'separate thing' is an ugly lemma that depends on (say) a Nat in the context of the larger theorem, that can be quite ugly to pull out! And feels like a nasty hack of a solution

[Alex Meiburg]

On the other hand, the fact that you could always pull out whatever you need to get the universe polymorphism back feels like exactly a case for why this should be possible. Clearly it doesn't compromise Lean's type system in anyway. In the same way that various tactics, or props in defs, get pulled out into separate .proof_N or auxLemma top-level objects, surely there's a way to have a suffices that (if needed) gives me the new thing at the top level with a universe polymorphism?

[Jireh Loreaux]

I'm fairly certain this isn't possible without making foobar depend on the universes u3 and u4, which is problematic because they don't appear in the statement. The claim "clearly it doesn't compromise Lean's type system in any way" is not so obvious to me (but IANA type theorist), unless it is actually pulled out as a top-level object, at which point you could just do that yourself. :shrug:

[Alex Meiburg]

Even I make foobar dependent on u_3 and u_4, it doesn't work, because I can't 'plug in' u_1 for u_3 in my suffices or something. I don't see any way to do _besides_ pulling it out as a top-level object.

[Alex Meiburg]

IANA type theorist either, but I feel reasonably confident in the claim "if I can construct a type T using a type U where U is a top-level object, I can also construct a type T using U in a let-clause"

[Kevin Buzzard]

If it's inconceivable that you would ever need to apply this with two different universes then you could always just put the types in the same universe. This is usually my first reaction to universe problems. My impression is that we're only maximally universe polymorphic by default because it's there, not because it's actually useful in practice

[Jireh Loreaux]

Kevin, surely that isn't true for anything that tangentially interacts with the category theory portion of of the library, right?

[Jireh Loreaux]

(because universe bumps are forced there)

[Alex Meiburg]

It's pretty inconceivable, sure. But it's a fact I want to use in other places that I've sorryed out, and they all also make the same "lazy" choice of having universes not actually be equal. So if I make the universes equal here, everything else using this must also be changed to be universe symmetric. That feels a bit worse.

[Eric Wieser]

Does let rec work here? It genuinely extracts a definition unlike have

[Kevin Buzzard]

Jireh my impression is that whenever there are universe problems then this is an indication that we're being too polymorphic, which is why my go-to fix is to be less polymorphic. I know that we've tried lots of other fixes instead but I'm just saying my opinion.

[Alex Meiburg]

let rec sadly does not work. Although I can introduce fresh universe variables there, they get added as universe variables in the enclosing theorem, so they are already "bound" to some particular (abstract) values when I want to apply it. The same is true for term-mode let rec. Good idea, though.

[Alex Meiburg]

I don't know enough about Lean at the 'basic level' but maybe this is actually just not supported by Lean syntax (even though it's supported by the underlying type theory, by e.g. defining it externally to the theorem)?

[Alex Meiburg]

It's quite strange, so if I do let rec myWlog := ∀ (d₁ : Type) {d₂ : Type} ..., then it creates new universe variables and adds them as universe parameters to the enclosing theorem foobar so that it's foobar.{u1,u2,u3,u4}`.

If I do #print foobar.myWlog, I see a type like what I want:

theorem foobar.myWlog.{u1,u2,u3,u4} : ∀ (d₁ : Type u_3) {d₂ : Type u_4} ...

But! That's not the type I actually have access to, as given by let rec! The only myWlog I'm able to access within the proof of foobar, is the one where myWlog has been instantiated already with the universe variables u1,u2,u3,u4 from the enclosing scope.

[Alex Meiburg]

If I try to pass in universe variables, I get invalid use of explicit universe parameters, 'myWlog' is a local.

[Alex Meiburg]

The same thing happens if I do theorem foobar ... := by (.....) where myWlog = .... .

[Jireh Loreaux]

I would argue that when you're saying "it's supported by the underlying type theory", that it really isn't. When you make a declaration that's external to the theorem, it may be universe polymorphic, but it's not one Lean.Expr that holds for all universes. Rather, each universe can be inserted into the declaration to get a new Lean.Expr (this is docs#Lean.Expr.const). So, if you declare it externally, and then use it in the proof twice, you are actually using two different expressions. Whereas, if you try to make it universe polymorphic in the proof it would require you to make an expression in the proof of the form "for all universes ...", which can't exist in the type theory.

Now, in practice, you are only using the two universes in scope, so you don't actually need the "for all universes" statement, you just need the two individual ones (i.e., the u1,u2 and the u2,u1 instantiations).

[Alex Meiburg]

I guess I understand why let rec works this way -- you want it to be able to bind variables in the surrounding statement. If your internal statement depends on external values, then you also depend on their universes. The new definition exists at the top level, and it takes the form (localValues) -> letRecGivenType. But you don't want to have to manually go plugging all of the local variables in yourself, so let rec does that for you and just gives you the (possibly dependent) type that you asked for.

This object you get has already been instantiated with some arguments, which also means all of its universe arguments have to be instantiated. Sadly this is true even if your let rec depends on no local variables. If lean supported "mixed" arguments and universes, this could be avoided, but I don't think that's possible.

[Alex Meiburg]

Alright Jireh, that's a fair point, I'll have to think about that a bit

[Alex Meiburg]

I think an interesting instance to think about is something like this:

theorem twoUs (x : Type u1) (y : Type u2) : Type :=
  sorry

def usingIt : Type :=
  let oneArg := twoUs ℕ
  if 3 = 5 then
    oneArg ℚ
  else
    oneArg (Type → ℚ) --error

def usingIt' : Type :=
  if 3 = 5 then
    twoUs ℕ ℚ
  else
    twoUs ℕ (Type → ℚ)

whatever twoUs is, usingIt is trying to trying to plug in two arguments to get an output. The first one doesn't compile and the second one does, even though the second is precisely the result of plugging that let in to both cases where it might be used. The let instantiates twoUs at some particular universe level. It doesn't know what yet -- that gets filled in later -- but it needs to fill it in with something. In the first case, it can't do that consistently across both branches. It's the same with let rec.

Sorry if I'm rambling a bit, I'm trying to figure this out myself too

[Jireh Loreaux]

Alex Meiburg said:

even though the second is precisely the result of plugging that let in to both cases where it might be used

No, it's not. oneArg doesn't have a universe as a (universe level) implicit argument, it has a universe metavariable. So after the first branch, that metavariable is instantiated, and then it can't work in the second branch. In contrast, the two twoUs in the branches of UsingIt' are actually different, and have instantiated the universe level implicit arguments differently.

[Alex Meiburg]

Sorry, I meant plugging in the string (which is obviously not a very meaningful notion in general). I get why it's happening. It's just weird

[Jireh Loreaux]

If you step through the tactic state here, it may help.

example : False := by
  let oneArg := twoUs ℕ
  let foo := twoUs ℕ ℚ
  let bar := twoUs ℕ (Type → ℚ)
  let baz := oneArg ℚ
  let broken := oneArg (Type → ℚ)

[Jireh Loreaux]

Another thing, if you try to explicitly construct the docs#Lean.Expr you want to correspond to oneArg, I think you'll see why you have to put a metavariable in for the universe level. There's nothing else you can put there. This is what I mean when I say it's not supported by the underlying type theory.

[Kyle Miller]

Oh no, it looks like you're running into a bug in Type* that I've know about but never have seen anyone run into it yet. The Type* elaborator adds the universe level to the current declaration, and it really only makes sense in the top level binder list. Maybe try using Type _ instead for your let rec?

[Kyle Miller]

To underscore this, Type* modifies the current list of universe levels. Using in the body of a declaration is not supported, and I should make it throw an error if you try.

[Alex Meiburg]

Mm, switching to Type _ makes myWlog have universe metavariables, and avoids adding new universe variables to the top level. So I can then apply it to one case or the other. But, same as the let ... thing talked about above, those metavariables get fixed the first time I use it, so I can't change it the other time. In fact it seems to become part of the definition of myWlog, that #print foobar.myWlog shows its declaration has its universe variables explicitly bound to be one pair or the other. That makes sense with how metavariables work in retrospect, but I admit was not what I expected

[Alex Meiburg]

I was able to write a simple elaborator that effectively accomplishes this:

universe u_1

def x (F : Type*) : Nat := by
  let y := 3
  auxU z : (fun t ↦ y : ∀ (T : Type _), ℕ)
  exact y + (z ℚ) + (x.z y F) + (x.z 37 (Type u_1))

[Alex Meiburg]

my auxU declares the term given as x.z, or whatever the variable name is within the current enclosing name; and then also gives a let z := ... to use it immediately. So I use it once as z Rat at universe level 1, but then I can also use it at the universe levels u_2 (for F) and u_1+1 if I want to, by referring to in the enclosing name

[Alex Meiburg]

It binds the surrounding y into the closure so that if I use it directly (as z) I don't need to pass that back in; subsequent calls do of course. So there I pass in y the second time (or I can pass in something else like 37 if I want to)

[Alex Meiburg]

Ideally I would make another elaborator like getAux so that getAux z gets me the variable again (without needing to explicitly refer to the name of the surrounding function, which feels hacky) and could also provide the closure'd fvars again. But idk if I'll go that far

[Alex Meiburg]

(deleted)

[Eric Wieser]

This feels like a shortcoming in the syntax of where and let rec to me:

universe u v u' v'

-- fails
def foo {α  : Type u} {β : Type v} : (α → β) × (β → α) :=
  let rec aux (α' : Type u') (β' : Type v') : (α' → β') := _
  ⟨aux α β, aux β α⟩

-- fails
def bar {α  : Type u} {β : Type v} : (α → β) × (β → α) :=
  ⟨aux α β, aux β α⟩
where aux (α' : Type u') (β' : Type v') : (α' → β') := _

--works
def aux (α' : Type u') (β' : Type v') : (α' → β') := _
def baz {α  : Type u} {β : Type v} : (α → β) × (β → α) :=
  ⟨aux α β, aux β α⟩

It seems like where aux.{u',v'} could be legal syntax, and then everything would behave reasonably

[Alex Meiburg]

I agree that it feels like a syntactic deficiency, but I don't think you could make

def baz {α  : Type u} {β : Type v} : (α → β) × (β → α) :=
  ⟨aux α β, aux β α⟩ where...

work without actually changing the definition of TermM (or maybe MetaM?) to include extra data -- because you can't have one local variable aux that works for both