universes

Stream: lean4

[Eric Rodriguez]

I still don't fully understand the details behind universes+cumulativity (I asked a question on the new SE recently but I'm wondering what the status of cumulativity/compiler support of ulift is in Lean4.

The reason I ask is because I recently had to use ulift ℚ in lean3, and realised that there was no field (ulift α) instance, and had to write it, which was tedious, and would dislike having to deal with it more and more often, and so I wonder if Lean4 brings any changes in this

[Mario Carneiro]

The proof of field (ulift A) should be a copy paste job from e.g. src#ulift.comm_ring

[Mario Carneiro]

I'm kind of surprised we didn't have it already

[Mario Carneiro]

pretty sure lean 4 changes nothing about the situation, and universe cumulativity is a huge step to take in exchange for the marginal benefit of using ℚ instead of ulift ℚ when you need a lifted type. Note that my proof in #leantt of the consistency of lean does not work in the presence of universe cumulativity, so we would be back in the Coq situation of "consistency is widely believed but an open question"

[Eric Rodriguez]

what about implicit casts, or making explicit types like ℚ polymorphic? and yes, the proof was (modulo a tiny detail) just a copy paste job, but this seems like a nice thing the compiler could support so that we don't have to worry about it

[Eric Rodriguez]

maybe even a @derive handler

[Mario Carneiro]

a derive handler like solution is possible, although I don't think the derive handler framework is designed for many classes on one type as opposed to one class on many types

[Mario Carneiro]

implicit casts are possible today, although I'm not sure if they will be consistently placed where we want

[Mario Carneiro]

Making types like Q polymorphic is a bad idea without some low level elaborator changes, because it will put lots of undetermined universes in statements and proofs, so we will have to specify them a lot more than we do today. We generally only use this method selectively, for example with punit and pempty

[Reid Barton]

Making something like a derive handler for ulift has been on the back of my mind for a while. I think it's harder than it might seem if you want to include non-algebraic classes like topological_space (even field is not quite algebraic).

[Reid Barton]

In general, I think mathlib needs much better support for ulift (and conversely, shouldn't be going out of the way so much to support using multiple universes at once). The combination (1) no universe cumulativity, (2) rat is not universe polymorphic, (3) limited support/automation for ulift leads to an awkward situation and downstream hacks--you can ask @Adam Topaz about mv_polynomial pempty R in LTE.

[Gabriel Ebner]

This almost works:

def ulift.field (K : Type u) [field K] : field (ulift K) :=
by transport using (equiv.ulift.symm : K ≃ ulift K)

[Reid Barton]

I don't really understand yet what the optimal situation should look like--it's a bit frustrating because 99% of the time the correct elaboration should be "instantiate all universe parameters to the same universe variable u"--but we could start by having instances for ulift X, which definitely seems correct anyways.

[Gabriel Ebner]

Just found this:

instance {K : Type u} [field K] : field (ulift K) := equiv.ulift.field

[Reid Barton]

Mario Carneiro said:

Note that my proof in #leantt of the consistency of lean does not work in the presence of universe cumulativity

Is this about Prop, or does it already not work when the Type u universes are cumulative?

[Eric Rodriguez]

It's a shame that there'd be issues if all ℚ (for example) were replaced with ℚ.{?m_1}.

[Mario Carneiro]

@Reid Barton It essentially uses the unique typing property, and that proof was difficult and original. With cumulativity I'm not even sure what the analogous statement of unique typing is, but it is primarily important for distinguishing Prop from Type u. How can I prove that Type u : Prop is false?

[Mario Carneiro]

There is a part in the model construction where I want to know, for any expression, whether it denotes a proof or not. For well typed lean expressions, I can say e : A and A : Sort u and then if u = 0then it's a proof otherwise it's data. Importantly, if u = 1 I want to deduce that it's not also the case that u = 0, which is saying that if A : Type then A : Prop is not derivable. With universe cumulativity this is not true

[Mario Carneiro]

In fact, cumulativity would also break the model construction itself, because the reason I ask the question is so I can translate forall differently from Pi. Cumulativity is going to force the two translations to match, because anything constructed in a low universe can be lifted without change to a higher universe. That sounds awfully close to a false statement: \lambda x : nat, (rfl : x = x) translates to $\bullet$ but \lambda x : nat, (rfl : (x = x : Type)) translates to $(x\in\mathbb{N}\mapsto \bullet)$

[Reid Barton]

Well the last example is why I suggested keeping Prop non-cumulative with Type.

[Mario Carneiro]

It's plausible that this is enough, but it would still be difficult to adapt, because (A : Prop) -> !(A : Type) is just one small consequence of the unique typing theorem, which has to be stated in a general way and involve many clauses so that it can be proven by a (very large mutual) induction

[Kevin Buzzard]

If making ulift(rat) a field was so easy then can someone come up with a one-liner to make ulift(int) totally ordered? Amelia needs this.

[Reid Barton]

I certainly agree the metatheory becomes murkier with cumulative universes and I don't think it's something we are likely to ever see in Lean.
I should have added another item to my list, (4) no support for hypothesized universe inequalities u <= v--this is relevant because while you can define things like "the category of R-modules in Type v for R : Type u", it's not well-behaved when u > v (e.g. it has a tensor product but no unit object, it has colimits but you can't construct them using the usual general machinery). And using circumlocutions like "the category of R-modules in Type (max u v)" tends to cause unification to break quickly. Things should be OK if we could require u <= v in the formation of Mod.{u v} R, but we can't.
Consequently it's better to just use ring and modules in the same universe--and now we need ulift in a few places because int and rat and so on are trapped in Type 0. But since you have to deal with this universe issue somehow it's better to do it up front and put your base ring in the universe you want, and then never think about universes again.

[Gabriel Ebner]

If making ulift(rat) a field was so easy then can someone come up with a one-liner to make ulift(int) totally ordered?

@[reducible] def equiv.linear_ordered_ring {α β} (e : α ≃ β) [linear_ordered_ring β] :
  linear_ordered_ring α :=
by letI := e.ring; apply e.injective.linear_ordered_ring _; try {apply_instance};
  intros; apply e.apply_symm_apply

instance : linear_ordered_ring (ulift ℤ) := equiv.ulift.linear_ordered_ring

[Eric Rodriguez]

From what @Eric Wieser said on my PR, this will mess up defeqs until a future change.

[Eric Wieser]

Right, we have two different families of function.injective lemmas; the ones with _pow _nsmul suffices, and the ones without

[Eric Wieser]

If you mix them you end up with diamonds in those fields

[Eric Wieser]

If you avoid the _nsmul ones, you end up with diamonds in the nat-actions

[Eric Wieser]

So I'd argue that the majority of those definitions (and all of the equiv ones) are foot-guns

[Eric Wieser]

I'm trying to fix that in #12126, but I have to patch all the feet with holes in at the same time

[Gabriel Ebner]

I think all the function.injective constructions are wrong in the same way, so as long as you don't mix them with anything else you should be fine. (And I believe we don't have any instances for ulift ℤ yet.)

[Eric Wieser]

Right, but you have to mix them to create things like add_comm_group as { ..add_group_smul, add_comm_semigroup }

[Eric Rodriguez]

I did try the equiv.field that you suggested at a leaf lemma, and it refused to work, presumably because of these issues

[Eric Wieser]

So it's not that _all_ the versions without _smul are bad, it's just the ones for which a _smul variant could exist but doesn't that are the traps. add_comm_semigroup has no nsmul operator so is safe.

[Eric Wieser]

Maybe the first step of the refactor should be to rename all the ones that are dangerous to .injective.foo_bad_smul, and remove the smul suffix from the ones that are not

[Eric Rodriguez]

Maybe actually the best idea for compiler support in Lean4 is to make an automatic equiv/injection pushforward, and then this ulift stuff can be a special case that can get handled by some meta code

[Gabriel Ebner]

Right we should add such a command (after the port). We'll also be able to add to_additive for classes.

[Reid Barton]

I'm not sure why this would need compiler support. But then, I also seem to be the only person who thinks this is actually quite nontrivial to do.

[Eric Wieser]

Meta support for something like "given I've shown +, 0, le, ... are preserved by this injective map f, transfer every typeclass possible to the domainof f" would be useful

[Eric Wieser]

Not so much generating the injective lemmas automatically, but applying them to ulift automatically

[Eric Wieser]

Another way to hand that might be more typeclasses

[Mac]

One way to get around ULift in a lot of instances is to just make the type in question universe polymorphic like PUnit.{u} : Sort u. A lot of parameterized types are already polymorphic (e.g., List, Array) so as long as the base type is polymorphic, the whole chain is polymorphic.

[Reid Barton]

I think this is really the correct approach in theory, but then what becomes annoying in practice is that type formers like -> and Prod are too polymorphic, so that types like PRat -> PRat would always require additional universe annotations.

[Reid Barton]

What we would like is a command like default universe u that would just instantiate all universe variables to u

[Eric Rodriguez]

Mario Carneiro said:

pretty sure lean 4 changes nothing about the situation, and universe cumulativity is a huge step to take in exchange for the marginal benefit of using ℚ instead of ulift ℚ when you need a lifted type. Note that my proof in #leantt of the consistency of lean does not work in the presence of universe cumulativity, so we would be back in the Coq situation of "consistency is widely believed but an open question"

a weird ping-pong, but through the SE I've been made aware of this - does this not prove consistency for coq?

[Mario Carneiro]

@Eric Rodriguez It looks close, but as far as I can tell they never claim that the system they are proving consistent is Coq, and it seems to be missing some features from Coq like coinductive types, the Set and SProp universes, and impredicative inductive types. Also modules and other features of Coq that interact with the kernel are not touched. In short, while that paper could plausibly be used as the core of a proof of consistency of Coq, there is still more work to do to cover the full system.

[Eric Wieser]

Eric Rodriguez said:

From what Eric Wieser said on my PR, this will mess up defeqs until a future change.

We now live in this future

[Kevin Buzzard]

So now can we have a partially ordered ulift int without any footholes?

[Eric Wieser]

Yes