Universe-heterogeneous ordinal and cardinal relations

Stream: mathlib4

[Violeta Hernández]

Here's something I've brought up earlier, but which I think we didn't really end up discussing much. Would it be desirable to introduce universe-heterogeneous versions of =, ≤, and < on ordinals and cardinals? e.g. x =l y would be defined as lift x = lift y.

[Violeta Hernández]

I think such a predicate would make working with stuff from different universes much easier. It gets rid of a particular pain point, which is that there's two possible ways to write a lift to a higher universe lift.{v, u} and lift.{max u v, u}, and simp can't rewrite them because it can't rewrite universes.

[Violeta Hernández]

(I previously suggested this on the docs#HasCardinalLT PR, but we decided that this should be discussed separately and independently of it)

[Violeta Hernández]

Here's a really basic sketch of how this would look like

import Mathlib.SetTheory.Ordinal.Basic

universe u v

class HasLift (α : Type u) (β : Type v) [LinearOrder α] [LinearOrder β] where
  Common : Type (max u v + 1)
  linearOrder_Common : LinearOrder Common := by infer_instance
  lift_α : α <i Common
  lift_β : β <i Common

variable {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] [HasLift α β]

def lift_eq (x : α) (y : β) : Prop :=
  HasLift.lift_α x = HasLift.lift_β y

infix:50 " =l "  => lift_eq

noncomputable instance : HasLift Ordinal.{u} Ordinal.{v} where
  Common := Ordinal.{max u v + 1}
  lift_α := Ordinal.liftPrincipalSeg
  lift_β := Ordinal.liftPrincipalSeg

[Violeta Hernández]

Actually, this might be a simpler approach:

import Mathlib.Order.InitialSeg

universe u v
variable {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β]

inductive lift_eq (x : α) (y : β) : Prop where
  | intro (γ : Type (max u v)) [LinearOrder γ] (f : α ≤i γ) (g : β ≤i γ) (h : f x = g y) : lift_eq x y

[Violeta Hernández]

Basically, two elements from two different well-orders can be considered "equivalent" when they're the same after being mapped by initial segments into a larger well-order containing both.

[Violeta Hernández]

The choice of initial segments and of the larger well-order should be mostly irrelevant. Recall that the type of initial segments between two well-orders is a subsingleton.

[Kevin Buzzard]

Is there an actual application for this?

[Violeta Hernández]

Lots! You can find instances of lift x = lift y and the like all over any part of Mathlib depending on cardinals/ordinals.

[Violeta Hernández]

Most notably, lift #X = lift #Y iff Nonempty (X ≃ Y).

[Violeta Hernández]

I've put a more refined version of my design up at #20980

[Violeta Hernández]

I've added what I think is all of the basic API for these predicates. The PR should be ready for review.

[Violeta Hernández]

Maybe @Eric Wieser would be interested in this, iirc we've discussed how to deal with lift lemmas in the past.

[Junyan Xu]

I can attest that lift = lift lemmas are very common in mathlib; I just wrote a few for transcendence degrees, and I recall @Jz Pan also wrote a lot about Module.rank and Cardinal.mk.

[Aaron Liu]

This would be amazing!

[Junyan Xu]

It's definitely good to be able to automate this, and if I understand correctly Violeta's PR does this without introducing new tactics.

[Eric Wieser]

For cardinals, is the definition above any different to using lift.{max u v} always?

[Violeta Hernández]

I think I didn't properly explain what my final design was. Basically, I introduce a new predicate liftEQ x y, which takes in arguments from two well-orders α and β (which might be in different universes!), and is (morally) defined as "for every well-order γ and initial segment embeddings f : α ≤i γ and g : β ≤i γ, we have f x = g y". This predicate is equivalent to lift (typein (· < ·) x) = lift (typein (· < ·) y), but since this file is meant to be used before ordinals are defined, we can't define it this way.

In the case where α and β are both Cardinal.{u} or Ordinal.{u} for different universes u, this predicate is also equivalent to lift x = lift y. This is something I'll prove in a follow-up PR.

The advantage of using this predicate is that we don't have to grapple with all possible ways of writing lift x = lift y. For instance, consider the statement "if lift x = lift y and lift y = lift z, then lift x = lift z". In order to prove this in current Mathlib, we'd first have to rewrite all lifts to a common universe max u v w, then apply transitivity, then rewrite the lifts to our target universe. But with this design, this is just liftEQ_trans.

[Violeta Hernández]

This new predicate also interfaces nicely with simp. We have liftEQ (lift x) y ↔ liftEQ x y and liftEQ x (lift y) ↔ liftEQ x y. Likewise, if x and y come from the same type (i.e. the same universe), we have liftEQ x y ↔ x = y.

[Eric Wieser]

What I'm asking is why not instead use

def LiftRel (r) (a : Cardinal.{u}) (b : Cardinal.{v}) := r (lift.{v} a) (lift.{u} b)

[Eric Wieser]

I understand the benefit of having a name to write API around, I don't see so much the benefit of building it using initial segments

[Junyan Xu]

Eric Wieser said:

For cardinals, is the definition above any different to using lift.{max u v} always?

I think lift.{v} cu = lift.{u} cv is the better spelling and if there is any lift.{max u v} left in the mathlib they should be replaced (unfortunately Cardinal.lift_umax doesn't work as a simp lemma according to the docstring). The PR probably simplifies (or has the potential to simplify) long rewrites like this.

In addition to Eq, LE, LT, it would also be nice to make the other operations like Add and Mul universe polymorphic too. I'm not sure what framework it fits in though. Maybe we need some elaborator to automatically insert lifts in the statements and tactic to insert them as proofs proceed and remove(cancel) them when possible. Maybe just design these specifically for Cardinal since it will be the main use case (as Eric points out).

[Junyan Xu]

A possible challenge problem for such elaborator/tactic:

import Mathlib
universe u v w x
variable {c : Cardinal.{u}} {d : Cardinal.{v}} {e : Cardinal.{w}} {f : Cardinal.{x}}
open Cardinal in
example (h₁ : lift.{v} c ≤ lift.{u} d) (h₂ : lift.{x} e ≤ lift.{w} f) :
    lift.{max w x} (lift.{v} c * lift.{u} d) ≤ lift.{max u v} (lift.{x} e * lift.{w} f) := sorry

It's a pain to even write down the statement.

[Eric Wieser]

This is a nice example of where LiftLE wouldn't really help

[Eric Wieser]

Junyan Xu said:

it would also be nice to make the other operations like Add and Mul universe polymorphic too

Note that it's messy to write Monoid in this framework, because it would need 3 universe parameters for associativity, but only two for mul_one. Maybe the "multiple parameters" rule for typeclasses only applies to term parameters not universe parameters though.

[Eric Wieser]

Another possible way out; refine lift as def lift.{v, u} [UnivLE.{u, v}] (x : Cardinal.{u}) : Cardinal.{v}

[Eric Wieser]

And then the convention becomes "when writing theorems, pick one universe and use it for every lift"

[Junyan Xu]

Yeah I also had the same idea. UnivLE/Small isn't data carrying though so this lift can't be computable. If you make them data carrying I think there are diamonds. Some of mathlib may rely on the defeq that lift is Quotient.map of ULift.

[Violeta Hernández]

Junyan Xu said:

A possible challenge problem for such elaborator/tactic:

import Mathlib
universe u v w x
variable {c : Cardinal.{u}} {d : Cardinal.{v}} {e : Cardinal.{w}} {f : Cardinal.{x}}
open Cardinal in
example (h₁ : lift.{v} c ≤ lift.{u} d) (h₂ : lift.{x} e ≤ lift.{w} f) :
    lift.{max w x} (lift.{v} c * lift.{u} d) ≤ lift.{max u v} (lift.{x} e * lift.{w} f) := sorry

It's a pain to even write down the statement.

We do have simp lemmas for e.g. lift (x * y) = lift x * lift y, so this shouldn't be *nearly" as bad.

[Violeta Hernández]

Eric Wieser said:

Another possible way out; refine lift as def lift.{v, u} [UnivLE.{u, v}] (x : Cardinal.{u}) : Cardinal.{v}

This doesn't seem very different from the approach of using lift.{max u v} throughout, except that we now have an extra typeclass argument to worry about...

[Violeta Hernández]

I do think the convention of writing lift.{max u v, u} is better than our current one of writing lift.{v, u}, though it still leads to some annoyance in e.g. the transitivity example.

[Aaron Liu]

We have push_cast and norm_cast, would it be helpful if someone wrote a push_lift and norm_lift tactic?

[Violeta Hernández]

What exactly would these tactics do?

[Aaron Liu]

It would move lifts around through expressions. For example, push_cast turns Nat.cast (m + n) into Nat.cast m + Nat.cast n, so push_lift could turn Ordinal.lift (m + n) into Ordinal.lift m + Ordinal.lift n.

[Aaron Liu]

Actually, is it possible to add lemmas to push_cast and norm_cast?

[Eric Wieser]

I don't think you can reuse push_cast here, because probably isn't doesn't care for universes

[Eric Wieser]

Also in the example above, I think you'd need push_lift at h1 h2 |-, which would move all the equalities to the same universe

[Eric Wieser]

(perhaps more importantly, I don't think push_cast works on inequalities)

[Violeta Hernández]

A tactic that changes all lifts to a common universe, such as the maximum of all universes that appear in the hypothesis and statement, would definitely alleviate most of the lift hell.

[Violeta Hernández]

But imo my liftEQ implementation can already provide very similar functionality without having to deal with automation

[Violeta Hernández]

There's another thing to consider: unless we add the UnivLE hypothesis to lift (which comes with other issues as we've discussed), we'd have to manually enforce the proper lift convention. Again, the liftEQ predicate sidesteps this issue by providing a single canonical form.

[Eric Wieser]

Here's a solution to @Junyan Xu's challenge:

import Mathlib
universe u v w x
variable {c : Cardinal.{u}} {d : Cardinal.{v}} {e : Cardinal.{w}} {f : Cardinal.{x}}
open Cardinal

attribute [coe] Cardinal.lift
attribute [norm_cast] Cardinal.lift_mul Cardinal.lift_lift

example (h₁ : lift.{v} c ≤ lift.{u} d) (h₂ : lift.{x} e ≤ lift.{w} f) :
    lift.{max v x} (lift.{w} c * lift.{u} e) ≤ lift.{max u w} (lift.{x} d * lift.{v} f) := by
  rw [← lift_le.{max u v w x}] at *
  push_cast at *
  refine mul_le_mul' h₁ h₂

[Eric Wieser]

(I think the original statement was wrong, so I fixed it)

[Eric Wieser]

Having copies of norm_cast that use a different attribute than coe would certainly help a lot here

[Eric Wieser]

Unfortunately norm_cast is in core, so it's going to be annoting to protype that generalization

[Violeta Hernández]

So what does this mean for us in the present? Should I close my PR in favor of waiting for a fully-fledged push_lift tactic? Should we at least change the way we write lift equalities?

[Violeta Hernández]

Ideally, we could even automate the initial step of "lift everything to a common universe". But I don't know if that's a reasonable expectation.

[Violeta Hernández]

Actually, the norm_lift tactic might not even be needed. We could just make our own simp set:

import Mathlib
universe u v w x
variable {c : Cardinal.{u}} {d : Cardinal.{v}} {e : Cardinal.{w}} {f : Cardinal.{x}}
open Cardinal

example (h₁ : lift.{v} c ≤ lift.{u} d) (h₂ : lift.{x} e ≤ lift.{w} f) :
    lift.{max v x} (lift.{w} c * lift.{u} e) ≤ lift.{max u w} (lift.{x} d * lift.{v} f) := by
  rw [← lift_le.{max u v w x}] at *
  simpa only [lift_lift, lift_mul] using mul_le_mul' h₁ h₂

[Eric Wieser]

The benefit of a custom tactic would be that it cleans up the goal state to not be a big pile of maxs

[Eric Wieser]

I guess "put everything in the same level" is not that far off from "lift everything to the smallest of Nat / Int / NNRat / Rat / NNReal / Real"

[Violeta Hernández]

Eric Wieser said:

The benefit of a custom tactic would be that it cleans up the goal state to not be a big pile of maxs

I'm not sure if that's avoidable. For instance in the example above, we couldn't do something like norm_lift mul_le_mul' h₁ h₂ because the expression wouldn't typecheck before lifting h₁ and h₂ to a common universe.

[Eric Wieser]

So I think perhaps what's needed here is a norm_via tactic written from scratch to solve both problems at once

[Eric Wieser]

I'm proposing a tactic that replaces the rw and push_cast in my example above

[Violeta Hernández]

Idk about you but this seems like a big pile of maxs to me
image.png

[Violeta Hernández]

(that's the state after rw and push_cast in your code)

[Eric Wieser]

Yes, so the tactic would clean all that up too

[Violeta Hernández]

How?

[Eric Wieser]

Tactic incoming...

[Eric Wieser]

import Mathlib

section SanitizeLevels

deriving instance DecidableEq for Lean.LevelMVarId
deriving instance DecidableEq for Lean.Level
deriving instance Ord for Lean.Name
deriving instance Ord for Lean.LevelMVarId
deriving instance Ord for Lean.Level

/-- Associate and sort `max`es within a `Level`. -/
def Lean.Level.normalizeMax (l : Level) : Level :=
  addMax (go l)
where
  addMax (l : List Level) : Level :=
    dbg_trace s!"{l}, {l.dedup.mergeSort (compare · · ≠ .lt)}"
    match l.dedup.mergeSort (compare · · ≠ .lt) with
    | [] => panic!"impossible"
    | [l] => l
    | l :: ls => ls.dedup.foldl (Function.swap .max) l
  go : Level → List Level
    | u@.zero | u@(.mvar _) | u@(.param _) => [u]
    | .succ u => [.succ <| addMax (go u)]
    | .max u v => go u ++ go v
    | .imax u v => [.imax (addMax (go u)) (addMax (go v))]

open Lean Elab Meta Parser Tactic Syntax in
/-- Order every `max` term within level arguments. -/
elab "sanitize_levels" loc: optional(location) : tactic => do
  withLocation (Lean.Elab.Tactic.expandOptLocation <| Lean.mkOptionalNode loc)
    (atLocal := fun fvar => do
      Tactic.liftMetaTactic1 fun goal => do
        goal.replaceLocalDeclDefEq fvar <| (← fvar.getType).replaceLevel fun l => l.normalizeMax)
    (atTarget := do
      Tactic.liftMetaTactic1 fun goal => do
        goal.change <| (← goal.getType).replaceLevel fun l => l.normalizeMax)
    (failed := fun _ => do throwError "Failed everywhere")


end SanitizeLevels

universe u v w x
variable {c : Cardinal.{u}} {d : Cardinal.{v}} {e : Cardinal.{w}} {f : Cardinal.{x}}
open Cardinal

attribute [coe] Cardinal.lift
attribute [norm_cast] Cardinal.lift_mul Cardinal.lift_lift

example (h₁ : lift.{v} c ≤ lift.{u} d) (h₂ : lift.{x} e ≤ lift.{w} f) :
    lift.{max v x} (lift.{w} c * lift.{u} e) ≤ lift.{max u w} (lift.{x} d * lift.{v} f) := by
  rw [← lift_le.{max u v w x}] at *; push_cast at *
  sanitize_levels at *
  sorry

which makes the goal

c : Cardinal.{u}
d : Cardinal.{v}
e : Cardinal.{w}
f : Cardinal.{x}
h₁ : lift.{max u v w x, u} c ≤ lift.{max u v w x, v} d
h₂ : lift.{max u v w x, w} e ≤ lift.{max u v w x, x} f
⊢ lift.{max u v w x, u} c * lift.{max u v w x, w} e ≤ lift.{max u v w x, v} d * lift.{max u v w x, x} f

[Eric Wieser]

@Kim Morrison, are those derivings inappropriate for global instances?

[Eric Wieser]

Actually, I think simp already does this automatically, but docs#Lean.Level.normalize associates max the wrong way

[Eric Wieser]

Namely, this accumulator is backwards, and should have its arguments swapped

[Eric Wieser]

Either than, or the associativity of the max notation is wrong

[Eric Wieser]

lean4#6760

[Jz Pan]

An example is the cardinality/rank of an MvPolynomial and its fraction ring. The statement uses various lifts and max's. Do you think a "rw mod lift" tactic is useful?

[Eric Wieser]

I think we should get to the place where lift can be treated in the same way as a cast. So maybe rw_mod_lift is useful, but it would be a better use of time to write it simultaneously with rw_mod_cast

[Eric Wieser]

Eric Wieser said:

lean4#6760

Note this was closed as a duplicate of lean4#5695; please upvote that one instead!

[Violeta Hernández]

Any progress of getting these tactics into Mathlib?

[Jz Pan]

Maybe it's better if we can have a tactic which automatically generalize the universe homogeneous version of a theorem to universe heterogeneous one, by inserting Cardinal.lift, etc. automatically to suitable places.