Reduce universe variables in a number of places

[jdchristensen]

This PR improves things that were getting in the way in practice with certain formalizations. Lots more could be done, but these were things I was noticing. Each commit can be read independently.

Some highlights: conn_point_incl goes from 17 universe variables to 2 and Susp goes from 6 to 1. OO_inverts_ap' goes from 6 to 1, with no changes, just inheriting improvements from elsewhere. This allows us to avoid defining it in two steps.

Another nice thing sometimes happens: when you reduce foo from 8 to 4 variables, you often go from having to specify 8 variables to having to specify none, since the ones that remain are often determined by the context. So this PR is able to remove a number of annotations in high-level code (in exchange to adding some to more fundamental results).

[jdchristensen]

The first commit, introducing const_tt, uses the universe level Set in a few places where by default Coq was introducing a free universe variable. I think this is because we have Global Unset Universe Minimization ToSet. in Overture.v. Since we do intentionally put Unit, nat and some other things in Set, it seems odd to not allow Coq to minimize a universe variable to Set. However, if I flip this setting, then induction m fails in Basics/Trunc.v with Warning: Cannot remove m. [cannot-remove-as-expected,tactics], even though revert m; apply trunc_index_rect. works fine. If there's a way to fix the issue with induction, then I wonder if we should allow universe minimization to Set. Or would this minimize other things that we don't want minimized?

(Idempotents.v and several of the Classes files do locally turn on minimization to Set.)

[jdchristensen]

Just to be clear what I am talking about:

From HoTT Require Import Basics.

Definition myid (A : Type) : A -> A := fun a => a.
Set Printing Universes.
Print myid.

Definition id_unit : Unit -> Unit := myid Unit.
Print id_unit.
Check id_unit@{u}. (* An unused universe variable. *)

Definition const_unit (A : Type) : A -> Unit := @const A Unit tt.
Print const_unit.
Check const_unit@{u v}. (* u is unused, while v is the universe containing A. *)

Local Set Universe Minimization ToSet.

Definition id_unit' : Unit -> Unit := myid Unit.
Print id_unit'. (* myid@{Set} Unit *)
Check id_unit'@{}. 

Definition const_unit' (A : Type) : A -> Unit := @const A Unit tt.
Print const_unit'. (* const@{Set u} tt *)
Check const_unit'@{u}.

[SkySkimmer]

However, if I flip this setting, then induction m fails in Basics/Trunc.v with Warning: Cannot remove m. [cannot-remove-as-expected,tactics], even though revert m; apply trunc_index_rect. works fine

This is because we do Scheme trunc_index_rec := Minimality for trunc_index Sort Type. in Overture, but induction understands that name to mean "scheme for Sort Set" so uses it. Minimality is the non dependent induction so it's no good for our dependent goal.
(with minimization to set the goal is paths@{Set} _ _ : Set, without it's paths@{u} _ _ : Type@{u})

Using _rec to mean "non dependent" seems like a footgun when Coq interprets it as "for Set" so we should probably rename those schemes.

[mikeshulman]

We intentionally chose that meaning of _rec to match the Book, and I don't think the book invented it out of nowhere. It seems broken to me if Coq allows you to rename the induction principles but the tactic induction assumes that you haven't renamed them.

[jdchristensen]

Thanks for explaining! Yes, it seems like we're fighting Coq here by using names that conflict with built-in names. Changing the name for trunc_index_rec does solve that particular problem, but various other problems arise that are unrelated to induction schemes, so it seems like turning on minimization to set will be a bit challenging. (As an aside, since Set is the same as Type@{Set}, I'm not sure why Coq needs separate induction schemes specialized for Set...)

I also tried changing the definition of Type0 from Set to Type@{Set+1}, so that we could completely avoid using Set (and I forced nat to be in this new Type0), but then I got Error: Anomaly "Unable to handle arbitrary u+k <= v constraints." in Basics/Trunc.

So, I think for now this PR could go in. I added a comment mentioning that that const_tt trick could be removed if we figure out how to get minimization to set working. (I also changed the definitions of nat and trunc_index to document that they were already landing in Type0.)

[SkySkimmer]

but various other problems arise that are unrelated to induction schemes

What are those problems?

As an aside, since Set is the same as Type@{Set}, I'm not sure why Coq needs separate induction schemes specialized for Set

It may be related to -impredicative-set which allows to declare inductives that have induction schemes for Set but not for Type.

[jdchristensen]

What are those problems?

In PropResizing/Nat.v, Coq can't prove IsHProp Unit and IsHProp Empty using typeclass search. But manually filling in the proofs works.

In Categories/Functor/Sum.v, we get

The term "C" has type
 "PreCategory@{HoTT.Categories.Functor.Sum.1 HoTT.Categories.Functor.Sum.2}"
while it is expected to have type
 "PreCategory@{HoTT.Categories.Functor.Sum.10 Set}".

and I couldn't figure out how to fix this.

In Extensions.v, we get

The term "equiv_extendable_pathsplit n.+2 C f" has type
 "ExtendableAlong n.+2 f C <~>
  PathSplit n.+2 (fun g : forall b : B, C b => g oD f)"
while it is expected to have type
 "?T@{g0:=isequiv_pathsplit n} -> PathSplit n.+2 ?f".

and I didn't investigate this. There will likely be other issues, but they aren't revealed because of dependency issues.

(Also, in Categories/IndiscreteCategory.v, we get Warning: Cannot remove right_inverse. [cannot-remove-as-expected,tactics], but the file builds. I didn't investigate, but it's likely something to do with the induction schemes.)

[jdchristensen]

BTW, trunc_index_rec is currently never used in the library, and nat_rec is only used once, so it's very easy to make these names refer to what Coq expects (although it would be a bit confusing to readers of the library to have one convention for these types and another for other types). There are around 1000 lines matching '_rec\b' (where \b means a word boundary), so changing everything would be intrusive.

Related to Mike's comment, is there any mechanism to instead get induction to use results with different names?

[jdchristensen]

Ah, I found coq/coq#10766, from 2019, which is requesting this feature. No comments at all on that issue, so I can't tell if there's any chance it might be implemented.

[jdchristensen]

The issues involving turning on minimization to Set are too big to tackle as part of this PR, so if anyone is able to review it as is, that would be great.

[jarlg]

The changes seem good to me! Just a few minor comments.

[jdchristensen]

I just saw #1531 and addressed it. In master, freudenthal has 34 universe variables. With this PR, before the latest commit, it was down to 15. By removing just one line, a pose command that was unused, it goes down to 9. The other changes in the latest commit are just stylistic, to do the proof in smaller steps. Then there is the redefinition that gets it down to 2 universe variables.

[jdchristensen]

I'll merge this when the CI is done. If there is further feedback, I'm of course happy to make requested fixes. The things in this PR are pretty innocuous, and make lots of things better. If we can figure out how to get more things living in Set, that would get rid of lots more free universe variables that multiply in many situations, but that's blocked on things I don't know how to solve.