Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reduce universe variables and other clean-ups #1805

Merged
merged 7 commits into from
Jan 16, 2024

Conversation

jdchristensen
Copy link
Collaborator

When dealing with types defined to land in Set (aka Type0), such as abgroup_Z, Pos, Int and Fin n, it makes sense to use Local Set Universe Minimization ToSet. as otherwise free universe variables are created that are not matched when using the results. By doing this and being careful to use simple_induction, many universe variables are eliminated. For example, abgroup_Z goes from 25 to 0, fsucc_mod goes from 9 to 0, and stratified_succ goes from 17 to 1.

There are other improvements mixed in, such as making use of nat_iter. I also cleaned up various comments and fixed indentation.

Lemma int_add_pred_r a b : a + int_pred b = int_pred (a + b).
Proof.
apply int_add_assoc.
Qed.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The section above was just moved to Int/Spec.v, where it fits better.

@jdchristensen jdchristensen requested a review from Alizter January 9, 2024 20:23
Copy link
Collaborator

@Alizter Alizter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! Did we ever experiment with using minimization to set globally?

@jdchristensen
Copy link
Collaborator Author

Did we ever experiment with using minimization to set globally?

I tried it, and some things fail. One big issue is that IsTrunc is not cumulative, since it is defined using IsTrunc_internal, which is a Fixpoint. As far as I know, fixpoints can't be made cumulative. So that means IsHProp and IsHSet are not cumulative, which causes problems. There are other issues as well. In one spot, the coercion equiv_fun needed to be manually inserted. In another, some types in generic universes were forced to be in Set. A large number of files compiled without problems, but I didn't keep pushing this to see how much breaks. I think it might just take a few hours to get something like this working, with some universe annotations to block the minimization to set when it causes problems.

The problem with IsHSet means that this PR needs updating. I'm just about to push a commit that frees up the proofs of IsHSet. While working on this, I noticed that Decidable and DecidablePaths are not cumulative. They are classes with a single field. These can be made cumulative if the field is surrounded by { and }, but then to construct instances, you need to use Build_Decidable everywhere, which is a bit awkward. So for now I have left them not cumulative, and have also freed up their proofs.

It would be easier to use minimization to Set widely if we could make more things cumulative somehow.

(I also just realized that Spaces/Nat.v could use a similar treatment. I'll take a look later today, so let's not merge this yet.)

@mikeshulman
Copy link
Contributor

We could consider making IsTrunc inductive rather than recursive.

Inductive IsTrunc : nat -> Type -> Type :=
| istrunc_iscontr : forall {A:Type}, IsContr A -> IsTrunc 0 A
| istrunc_succ : forall {A:Type} {n:nat}, (forall x y:A, IsTrunc n (x = y)) -> IsTrunc (S n) A.

Of course that would involve adding some constructors in places where now we can just compute.

@SkySkimmer
Copy link
Collaborator

We would probably want to change the argument order so that the type argument can be a parameter. Otherwise its universe has more restricted cumulativity AFAICT.

@mikeshulman
Copy link
Contributor

Ugh. Maybe we could make a notation that puts the arguments back in the right order.

It would be nice if there were a way to indicate which arguments are indices and which are parameters that didn't require all the parameters to come before all the indices.

@jdchristensen
Copy link
Collaborator Author

@SkySkimmer Is there any chance that in the future Coq could have cumulative fixpoints?

@SkySkimmer
Copy link
Collaborator

I haven't seen any proposed rules of how that would work.

@jdchristensen
Copy link
Collaborator Author

I tried the inductive definition of IsTrunc, and Coq accepts it in the modified form below, but it seems quite awkward to work with.

Cumulative Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| istrunc_iscontr : Contr_internal A -> IsTrunc_internal A minus_two
| istrunc_succ : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Existing Class IsTrunc_internal.

Notation IsTrunc n A := (IsTrunc_internal A n).

It's not just that you need to apply constructors, but that you need to go backwards. For example, we define Contr A to be IsTrunc (-2) A, but then one needs to prove that Contr A is equivalent to Contr_internal A. And when given a hypothesis of the form IsTrunc n.+1 A, when you do induction on it, you need to handle the istrunc_iscontr constructor somehow. The following helps:

Scheme IsTrunc_internal_ind := Induction for IsTrunc_internal Sort Type.
Scheme IsTrunc_internal_rec := Minimality for IsTrunc_internal Sort Type.
Definition IsTrunc_internal_rect := IsTrunc_internal_ind.

Definition IsTrunc_unfolded (n : trunc_index) (A : Type)
  := match n with
    | minus_two => Contr_internal A
    | n.+1 => forall x y : A, IsTrunc n (x = y)
    end.

Definition istrunc_unfold (n : trunc_index) (A : Type)
  : IsTrunc n A -> IsTrunc_unfolded n A.
Proof.
  intros [istr|k istr]; exact istr.
Defined.

Definition isequiv_istrunc_unfold (n : trunc_index) (A : Type)
  : IsEquiv (istrunc_unfold n A).
Proof.
  simple refine (Build_IsEquiv _ _ (istrunc_unfold n A) _ _ _ _).
  - destruct n; constructor; assumption.
  - destruct n; reflexivity.
  - intros [istr|k istr]; reflexivity.
  - intros [istr|k istr]; reflexivity.
Defined.

Definition equiv_istrunc_unfold (n : trunc_index) (A : Type)
  := Build_Equiv _ _ _  (isequiv_istrunc_unfold n A).

I also put primes on the constructors of Contr_internal and did:

Definition center (A : Type) {H : Contr A} : A := @center' A (istrunc_unfold _ _ H).
Definition contr {A : Type} {H : Contr A} (y : A) : center A = y := @contr' A (istrunc_unfold _ _ H) y.

But even with these, it's annoying to work with. E.g. the last result in Contractible.v needs to use that ap of an equivalence is an equivalence, but that currently comes later. It wouldn't be hard to flip the dependency between Contractible.v and Equivalences.v to handle this, but I suspect that we'd continue to find it annoying to work with.

@mikeshulman
Copy link
Contributor

We could also rid of Contr_internal and incorporate it in the definition of IsTrunc:

Cumulative Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| istrunc_iscontr : (center : A) -> (forall y : A, center = y) -> IsTrunc_internal A minus_two
| istrunc_succ : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Then there would only need to be one definition of center and contr.

For example, we define Contr A to be IsTrunc (-2) A, but then one needs to prove that Contr A is equivalent to Contr_internal A. And when given a hypothesis of the form IsTrunc n.+1 A, when you do induction on it, you need to handle the istrunc_iscontr constructor somehow.

Sure, but don't we only need to do that once? Once we've proven the relevant equivalences, we can just apply those lemmas and tactics.

In general, I've come more and more to believe in the principle that whenever possible types should be canonical, not things that compute definitionally, because this makes it easier to match against them. For instance, mightn't an inductive IsTrunc simplify some of the problems with typeclass inference? We have the comment that

We prefer to reason about [IsTrunc (S n) A] rather than [IsTrunc n (@paths A a b)]

but if IsTrunc is canonical there would be no difficulty with this: IsTrunc (S n) A doesn't reduce to anything, we just have to apply a tactic or lemma to use it (e.g. istrunc_intro x y rather than intros x y).

@jdchristensen
Copy link
Collaborator Author

@mikeshulman You're probably right that with appropriate tactics, using the inductive definition would be fairly painless. But it would probably require many small changes throughout the entire library to do the conversion, so it might be a bit of work.

Another observation is that with my sample code above, we essentially have both definitions. IsTrunc is the inductive one, and IsTrunc_unfolded is essentially the fixpoint one, except that it goes via IsTrunc in the inductive step. Theorems would be stated using IsTrunc and proved using IsTrunc_unfolded, and we'd be frequently converting back and forth. Except for the benefit of cumulativity, it would seem cleaner to just use one definition. One of the things I've learned is that if you can get things to work out definitionally, it really simplifies things in many cases!

@mikeshulman
Copy link
Contributor

It seems to me that the only time we'd actually need to transfer explicitly across that equivalence would be in proving that IsTrunc is a proposition (and we might be able to just do that by hand without introducing IsTrunc_internal at all). Once we know that, it seems to me that in further proofs we'd only need to use the constructors of IsTrunc and their inverses.

@Alizter
Copy link
Collaborator

Alizter commented Jan 12, 2024

@jdchristensen Are you happy with this being merged?

@jdchristensen
Copy link
Collaborator Author

No, let's not merge this yet. If the WIP on making IsTrunc inductive pans out, then the last commit here will need to be undone. Also, I plan to see if I can make similar improvements to Nat.

@jdchristensen
Copy link
Collaborator Author

I rebased, removed the universe variables added to proofs of IsHSet, etc., removed universe variables in Empty, improved the simple_induction tactic (so you don't have to do intro n first, which should also make the proof term smaller), added simple_induction' (with autogenerated IH name), and removed the universe variables from Spaces/Nat/*. I think this is ready to merge once this batch of changes has been reviewed.

@jdchristensen jdchristensen requested a review from Alizter January 16, 2024 18:52
@Alizter
Copy link
Collaborator

Alizter commented Jan 16, 2024

I wonder if we can shadow induction everywhere and define it as simple_induction.

Copy link
Collaborator

@Alizter Alizter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Thank you very much for all this careful work!

@jdchristensen jdchristensen merged commit 89cd1d2 into HoTT:master Jan 16, 2024
23 checks passed
@jdchristensen jdchristensen deleted the universe-vars branch January 16, 2024 21:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants