fix universes in list library

[Alizter]

We explicitly annotate all the lemmas in the list library in order to make sure there is no universe blow up. The universe blow up stems from poor implementation of various tactics with respect to universe polymorphism.

I will get onto cleaning up universes in the linear algebra library too, but that is also affected by a more critical universe blow up which will have to be considered separately.

[Alizter]

It seems that this is not ready. I need to work out a way to keep it compatible with 8.18. It seems that inference improved since 8.18 meaning that I need to work in 8.18 and be more explicit to be fully compatible.

[jdchristensen]

Ok, tag me when this is ready to review. BTW, I think that in many case, Coq does the right thing with universe variables by default, and I prefer to not annotate things in those cases, as it makes the statements harder to read.

[Alizter]

@jdchristensen I've tried to be as conservative as possible with Coq 8.18 however it ends up with me needing to annotate the term beyond recognition. I'm wondering if it might be a good time to bump to 8.19 as the universe inference in 8.18 is just too poor to be usable.

An example of a problem that I am encountering. In 8.18, all the lemmas about paths with nth need to live in the path type of the option type. However Coq introduced a new universe variable because of the option type, which ends up with me having to write paths@{i}.

[SkySkimmer]

What changed about universes in 8.19? There's kernel sort polymorphism but that shouldn't matter for hott.

[Alizter]

@SkySkimmer I'm unsure what has changed in the Coq side. I suspect something about cumulative universes might be different. If you have a look at this PR you will see a clear difference between the versions.

[jdchristensen]

I'm wondering if it might be a good time to bump to 8.19

Since 8.19 was released more than four months ago, I'm fine with this.

[Alizter]

@jdchristensen I've relaxed some of the annotations in Theory.v and kept only the ones where the annotations matter. I think this is ready for another round of review.

Let me know if you still think there are too many universe annotations in some places. I've had a go, but perhaps there are areas I can improve.

[jdchristensen]

I just pushed changes to List/Theory.v. There were several cases where there was a universe constraint i <= j that was not needed, but could be replaced with an upper bound universe u with i <= u and j <= u. While the upper bound approach has more universe variables, it's still the correct thing to do, as the other approach introduces an unnecessary constraint. (And I think that in the future Coq might support using max(i,j) in more places, which would allow us to get rid of u.)

I also removed lots of annotations that had no effect, as Coq 8.19 does the right thing by default.

And I simplified two proofs, near the beginning.

When trying to fix issues with too many universe variables, I always try to trace things down to the earliest result with extra variables. After fixing that, I check whether later results still have problems. If so, I again search for the earliest result that has issues, and fix it, always working bottom up. I often find that I just need to annotate a small number of early results and that the later results get fixed automatically.

[jdchristensen]

I forgot to fix the tests, and will do so in a minute.

[jdchristensen]

I'm also in the process of using a fix tactic to simplify things further, so don't push any changes.

[jdchristensen]

I added simple_list_induction which is just like simple_induction, and it works well. Those upper bound universes are always free, so they tend to multiply, so using this trick to get rid of them is useful.

[jdchristensen]

@Alizter I'm done, so if you think it looks good, feel free to merge.

[Alizter]

Thanks @jdchristensen LGTM!