search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

upper/lower triangular matrix rings #1981

Closed Alizter closed 6 days ago

Alizter commented 1 month ago

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:

jdchristensen commented 1 month ago

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 commented 1 month ago

@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 commented 1 month ago

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

Alizter commented 1 month ago

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

Alizter commented 1 month ago

@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 commented 1 month ago

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 commented 1 month ago

~2500 universe variables!

:exclamation:

I will see about fixing this.

jdchristensen commented 1 month ago

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 commented 1 month ago

@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 commented 3 weeks ago

@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 commented 3 weeks ago

I also opened this:

jdchristensen commented 3 weeks ago

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 commented 3 weeks ago

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

Alizter commented 3 weeks ago

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 commented 1 week ago

@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 commented 6 days ago

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!