upper/lower triangular matrix rings

[Alizter]

We define upper and lower triangular matrices, show that they satisfy various closure properties and define the subring of upper and lower triangular matrices.

Depends on:

• fix universes in Vector.v #1980
• theory of diagonal matrices #1977

[jdchristensen]

I see that you marked this a draft again, but I had noticed a few simplifications to the proofs, so I have pushed them. There is still a build problem having to do with the other PRs this depends on.

[Alizter]

@jdchristensen I re-drafted it since I forgot about the result mentioning diagonal matrices coming later. You can still continue to review it if you like, but it won't fully build just yet.

[jdchristensen]

I repushed my changes since they got lost in the force push you did.

[Alizter]

@jdchristensen I'm so sorry, I totally forgot that you pushed changes when rebasing. I won't force push any longer after undrafting.

[jdchristensen]

LGTM once the two sets of slow lines are improved.

[Alizter]

@jdchristensen This commit speeds up those lines a bit, I could probably speed it up further if I split it up like I did for the diagonal. WDYT?

[jdchristensen]

This commit speeds up those lines a bit, I could probably speed it up further if I split it up like I did for the diagonal. WDYT?

I think they are still too slow, so should be split up. ... And I checked matrix_diag_ring and it's actually still a bit slow, but you don't notice it because the time is spread over multiple tactics. I wonder if part of the slowness is because some of the lemmas about diagonal matrices use almost 600 universe variables? And the results about triangular matrices involve ~2500 universe variables!

In general, all of this should be really fast, so it would be good to check for slow lines and fix them, beginning with a fix to the universe variables.

[Alizter]

~2500 universe variables!

❗

I will see about fixing this.

[jdchristensen]

A quick look shows that the problems occur already in the List/Theory.v file, e.g. with nth'_seq'. I wonder if we should be using minimization to set in List/Core.v, etc. E.g. does seq need to land in list@{i} nat, or would list@{Set} nat be good enough? Do we want to have Local Set Polymorphic Inductive Cumulativity. in most of these files?

Maybe the thing to do is to make a separate PR with cleanups to the universe variables, and then rebase this one on that one to see if the speed issue goes away.

[Alizter]

@jdchristensen I've been tweaking it from where you said since yesterday but the work grows a lot. I need to finish and split up the work. You're correct that seq and seq' should land in Set. The problem is way bigger than I expected.

[jdchristensen]

@Alizter I'm curious how things look here after rebasing, now that some universe variables are fixed in other places. Can you rebase? Or I can try hitting the "Update branch" button.

[Alizter]

I also opened this:

• fix universes in vector #1987

[jdchristensen]

Already the fixes to lists have made a huge improvement here, reducing the number of universe variables from thousands to dozens (e.g. 33 for lower_triangular_matrix_ring). But the proof of lower_triangular_matrix_ring is still a bit slow, unfortunately.

[Alizter]

After the universe modifications to vector and matrix, we can revisit the speed in this proof.

[Alizter]

I want to do another cleanup of universe levels but this time in Matrix. The fact that matrix rings are taking 30 universes seems to be the crux of the issue.

[Alizter]

@jdchristensen I've annotated the file so that the subrings for diagonal and upper/lower triangular matrices have the correct number of universes. This can probably be improved so that annotations can be removed but I don't see how to avoid Ring being reduced to Set without unsetting minimization to set.

[jdchristensen]

Yes, it's odd that sometimes Ring is interpreted as Ring@{i} and sometimes as Ring@{Set}. Your new annotations look fine. With the various improvements to universes, the proof of matrix_diag_ring became fast. I still thought the triangular_matrix_ring results were a touch slow, so I expanded them in my last commit, and now they are fast.

So this LGTM!