!4#3247

Stream: PR reviews

[Jeremy Tan]

I've found out that LinearAlgebra.Dimension, even after the recent changes, depends on new theorems that are only forward-ported in !4#3343, which in turn depends on !4#3247. This latter PR is stale. Need someone to review why/whether noncomputable is needed (discussed in a comment on !4#3247)

[Jeremy Tan]

image.png

[Jeremy Tan]

Specifically Cardinal.lift_lt_aleph0

[Eric Wieser]

I can look at these on Thursday

[Scott Morrison]

I made a suggestion for a fix to !4#3247. I think we need to add an extra instance to steer Lean away from using a noncomputable ComMonoid Cardinal instance.

[Scott Morrison]

But I'm not sure where it is best to put this instance --- possibly at the first place that the "bad" instance gains priority (in Cardinal.Basic itself it seems fine).

[Scott Morrison]

Okay, found a good place to put it. Perhaps I'll just merge my changes and send this off, even though this makes this PR no longer an exact forward port.

[Eric Wieser]

We have similar instances to keep real operations computable

[Eric Wieser]

What are the non-computable and computable instances coming from?

[Scott Morrison]

noncomputable instance linearOrderedCommMonoidWithZero :
    LinearOrderedCommMonoidWithZero Cardinal.{u} :=
  { Cardinal.commSemiring,
    Cardinal.linearOrder with
    mul_le_mul_left := @mul_le_mul_left' _ _ _ _
    zero_le_one := zero_le _ }

is causing Lean to find a noncomputable CommMonoid Cardinal, even though a perfectly reasonable computable version is available via CommSemiring.

[Scott Morrison]

Okay, !4#3247 has compiled the relevant file, so I've sent it off to bors.

[Reid Barton]

This has to be the silliest example of the computable tax

[Reid Barton]

A Cardinal has literally no computational content

[Scott Morrison]

And it is silly that mathlib3 PRs about stuff like this are getting in the way of the port...

[Scott Morrison]

Oh, dear. !4#3343 discharges some forward porting debt, but also depends on yet another mathlib3 PR creating more? I don't like this. So to merge this (which we apparently need to do in order to start porting linear_algebra.dimension), I need to review a mathlib3 PR which could otherwise just wait.

[Scott Morrison]

Okay, I have merged everything.

[Eric Wieser]

I really don't think we should create forward-port PRs that depend on mathlib3 PRs

[Eric Wieser]

CI is failing on !4#3343: I recommend we:

• Forward-port only the trivial lemmas needed by linear_algebra.dimension, without updating the SHA, and leave porting notes that they are newer that the file sha
• Forward-port the other changes later under less time pressure (removing those porting notes). If this is a pain, consider reverting the mathlib3 change.

[Eric Wieser]

I would guess the first bullet could easily be done while porting linear_algebra.dimension, if the lemmas are just the ones I added.

[Eric Wieser]

@Jeremy Tan, are you happy to just add the missing lemmas as you need them when forward-porting that file?

[Jeremy Tan]

@Eric Wieser I think the aforementioned lift_lt_aleph0 is the only lemma needed by LinearAlgebra.Dimension

[Eric Wieser]

I imagine you might also need lift_le_nat_cast but the proof is also trivial

[Eric Wieser]

I think adding it in the porting PR of linear_algebra.dimension with -- porting note: not yet forward-ported from mathlib3#NNNN is fine

[Jeremy Tan]

So yes, we can just port the necessary extra lemmas first and kick the rest down the drain

[Eric Wieser]

I think "down the drain" doesn't quite translate how you intend it to (I read it as "throw away forever"); I assume/hope you mean "down the road"

[Jeremy Tan]

Yeah, it's a slip-up there. I did mean down the road

[Jeremy Tan]

!4#3354 is the mathlib4 port; I haven't done comment renaming yet, and there is a universe problem at cardinal_le_rank_of_linearIndependent I don't know how to solve

[Jeremy Tan]

OK, done the comment naming

[Jeremy Tan]

Then again, there's the symbol ↥ which works perfectly fine in LinearAlgebra.LinearPMap but completely bombs out in LinearAlgebra.Dimension. It apparently stands for coe_sort in mathlib3 – but it throws an expected '⟩' error in mathlib4

[Eric Wieser]

#15041 may or may not help with the universe problem

[Eric Wieser]

I would guess the coe_sort symbol can now just be written as ↑.

[Jeremy Tan]

Is #15401 the PR you mean? There are no universe twiddles in there

(but yeah, how did I miss the plain up-arrow)

[Jeremy Tan]

I must note that there are several more universe errors all over the place, including such absurdities as (L582)

stuck at solving universe constraint
  max w ?u.375172 =?= max w ?u.375184
while trying to unify
  (lift (#ι) = lift (#ι')) (lift (#ι) = lift (#ι')) ((lift (#ι) = lift (#ι')) (#ι)) ((lift (#ι) = lift (#ι')) (#ι'))
with
  (lift (#ι) = lift (#ι')) (lift (#ι) = lift (#ι')) ((lift (#ι) = lift (#ι')) (#ι)) ((lift (#ι) = lift (#ι')) (#ι'))

[Eric Wieser]

Apologies, that was data corruption because I had no clipboard available; I've edited the correct number in above

[Jeremy Tan]

Does that mean I have to wait for #15041 in order to get the file compiling?!

[Jeremy Tan]

AND its forward-port?

[Eric Wieser]

It depends; does it look like the changes in 15041 are in the same places that the problems are happening in the port?

[Jeremy Tan]

image.png This is one of the errors in my port, and it's touched by 15041 too

[Eric Wieser]

Yeah, this might be a place where it's worth going through with #15041

[Eric Wieser]

Let's see what @Scott Morrison thinks

[Eric Wieser]

Jeremy Tan said:

I must note that there are several more universe errors all over the place, including such absurdities as (L582)

stuck at solving universe constraint
  max w ?u.375172 =?= max w ?u.375184
while trying to unify
  (lift (#ι) = lift (#ι')) (lift (#ι) = lift (#ι')) ((lift (#ι) = lift (#ι')) (#ι)) ((lift (#ι) = lift (#ι')) (#ι'))
with
  (lift (#ι) = lift (#ι')) (lift (#ι) = lift (#ι')) ((lift (#ι) = lift (#ι')) (#ι)) ((lift (#ι) = lift (#ι')) (#ι'))

This error message really looks like a bug; why is it showing the same thing four times?

[Eric Wieser]

Or is this just something going wrong when you copy stuff out of the widget view?

[Eric Wieser]

(set_option pp.universe true might help see the details)

[Jeremy Tan]

It's not exactly the same thing four times:

stuck at solving universe constraint
  max w ?u.375172 =?= max w ?u.375184
while trying to unify
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
with
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
Dimension.lean:583:0
stuck at solving universe constraint
  max (max w w') ?u.375172 =?= max (max w w') ?u.375184
while trying to unify
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
with
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
Dimension.lean:583:0
stuck at solving universe constraint
  max (max (w+2) (w'+2)) (?u.375172+2) =?= max (max (w+2) (w'+2)) (?u.375184+2)
while trying to unify
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
with
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
Dimension.lean:583:0
stuck at solving universe constraint
  max w' ?u.375172 =?= max w' ?u.375184
while trying to unify
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375172 + 2)} (lift.{max w' ?u.375172, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375172, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))
with
  (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    (Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
      (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w} ι))
    ((Eq.{max (max (w + 2) (w' + 2)) (?u.375184 + 2)} (lift.{max w' ?u.375184, w} (Cardinal.mk.{w} ι))
        (lift.{max w ?u.375184, w'} (Cardinal.mk.{w'} ι')))
      (Cardinal.mk.{w'} ι'))

[Jeremy Tan]

In any case I seriously think @Violeta Hernández went overboard with cardinals

[Violeta Hernández]

What's the problem here?

[Jeremy Tan]

You made so many changes to the cardinal files that we can't port them to mathlib4

[Violeta Hernández]

In my defense it was mostly one old PR

[Violeta Hernández]

I'll fix the noncomputability issue and add that to my port of the cardinal changes asap

[Eric Wieser]

That's a problem, but not the blocking one

[Eric Wieser]

@Violeta Hernández, the current question is whether your universe PR will solve a problem that Jeremy is seeing while porting

[Violeta Hernández]

Ah, I see

[Violeta Hernández]

I would certainly hope so

[Violeta Hernández]

I've encountered a lot of similar universe issues and that PR seemed to solve them

[Eric Wieser]

In lean 4?

[Jeremy Tan]

But really, get !4#3343 fixed first @Violeta Hernández

[Eric Wieser]

There's no rush on 3343 unless we need the universe changes too

[Jeremy Tan]

We do need the universe changes

[Eric Wieser]

We can try making them in mathlib4 in a single lemma and see if they help before commiting to the the full PR

[Eric Wieser]

Just add a primed copy of the lemma with the new universes

[Violeta Hernández]

At least I'm glad that 8 month old PR is finally gaining traction

[Jeremy Tan]

Well, this version of the problematic lemma does work:

theorem cardinal_lift_le_rank_of_linearIndependent {ι : Type w} {v : ι → M}
    (hv : LinearIndependent R v) :
    Cardinal.lift.{v} (#ι) ≤ Cardinal.lift.{w} (Module.rank R M) := by
  apply le_trans
  · exact Cardinal.lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩
  · simp only [Cardinal.lift_le, Module.rank]
    apply le_trans
    swap
    exact le_csupᵢ (Cardinal.bddAbove_range.{v, v} _) ⟨range v, hv.coe_range⟩
    exact le_rfl

So I've changed the universes in #15041, while at the same time priming Cardinal.lift_mk_le (Cardinal.lift_mk_le' pre-#15041 becomes Cardinal.lift_mk_le post-#15041, so once the mathlib3 #15041 is forward-ported the priming would be reverted)

[Jeremy Tan]

Similarly for Basis.indexEquiv, this works without changing anything else:

def Basis.indexEquiv (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι' :=
  (Cardinal.lift_mk_eq'.1 $ mk_eq_mk_of_basis v v').some

[Jeremy Tan]

@Eric Wieser just pushed the universe fixes, the number of errors plummeted to 26

[Jeremy Tan]

@Eric Wieser it seems I might have been mistaken about the universe errors, but at least they're far less now

[Jeremy Tan]

How do I fix the remaining 26 errors?

[Jeremy Tan]

(25 after removing one lemma that is also removed in #15041)

[Violeta Hernández]

#18781 reinstates the cardinal partial order instance as suggested. Should be an uncontroversial merge.
!4#3247 does this too. Uncontroversial merge too.
!4#3343 can be merged immediately after.

[Violeta Hernández]

Sorry for this whole mess

[Scott Morrison]

It's okay! The problem here is a process issue with managing the freeze/transition. No individual author or reviewer is at fault -- indeed, everyone is doing their best to make great contributions to the library. We just need to work on processes to minimize these traffic jams!

[Scott Morrison]

I've merged !4#3247 again, hopefully it goes through again.

[Scott Morrison]

And !4#3343