Make IsTrunc an inductive type

[jdchristensen]

This is based on discussion in PR #1805 . With the changes shown here, around 225 of the 550 files in the library build. Every file changed in this PR builds, including all of Basics, Types, HProp.v, HSet.v, TruncType.v, etc. I haven't got to Truncations/* or Modalities/* yet, but I feel like at this point all of the non-trivial changes are done and it will just be a matter of inserting the constructors of IsTrunc and their inverses (via equiv_istrunc_unfold and/or istrunc_paths) in many places. It's a little annoying having to do this, so that's why I stopped at this point to see what people think. Also, there might be things I should change in the foundations, and it would be good to hear such suggestions before doing the rest of the work.

Two benefits I see: IsTrunc is now cumulative, and several things involving typeclasses that cluttered up Overture.v can simply be deleted.

The downsides: having to convert frequently.

I'm on the fence about whether this is a win, so I'd be particularly interested in feedback on this.

[jdchristensen]

This was moved to Trunc.v and generalized to contr_istrunc.

[jdchristensen]

This could be moved to Trunc.v, since that's the only place it is used.

[jdchristensen]

(It's now also used in ReflectiveSubuniverse. It could still move to Trunc.v, but maybe it's best in Overture.v.)

[jdchristensen]

This example no longer works, and since it was never used, I removed it.

[jdchristensen]

I added a coercion from IsTrunc to Funclass. Now, when using a proof of IsTrunc, you can treat it like a function, which should slightly reduce the number of places to be fixed. But it's much more common to need to produce an element of IsTrunc, and for then you still need to use one of the constructors. I don't know if there's any way to change that.

I had to do something with [n = -2], so I produce the contracting homotopy.

This coercion doesn't satisfy the uniform inheritance property, but it does work in practice.

Question: before this PR, given C : Contr A and a goal of A, apply C would work, with Coq inserting the call to center. I can't figure out why that worked before, but it no longer works now. Is there a way to make it work again?

[jdchristensen]

The second new commit finishes off Modalities/, Truncations/ and HIT/*, getting us more than half-way.

[jdchristensen]

Moved to end of file.

[jdchristensen]

These two moved from Types/Forall, since they are useful here. Also, the first one contr_forall is no longer an instance, since it was redundant.

[jdchristensen]

This was done because otherwise the universe variable in contr_unit was free (since IsTrunc is now cumulative), which caused a problem in another file (Nullification.v, I think).

[Alizter]

I did something similar with the definition of leq for nat and looking back I don't know if it was a good idea. Using inductive types can make the proofs more rigid to reduction, but also means we lose out on a lot of easy simplificiations.

However I suppose that a lesson to be learnt is that proof by reduction can be expensive, in that sense it is cheaper for the proof assistant to have an explicit sequence of terms. It also saves us from having to recompute the same kinds of things repeatedly.

The benefit of this approach is cumulativity and I think that is a good gain, since unnecessary universes cause a lot of performance issues for us.

Also, since being truncated is a hprop, we really shouldn't concern ourselves too much with how the proofs look. If we ever for some reason need to reason about a proof, we can always equate it to a nicer one. For this reason, having something that gains us efficiency is desirable.

Another benefit of this approach is that it will work better with the typeclasses mechanism. It is a huge burden to have to do reduction when resolving typeclasses.

These are my thoughts on this issue, I am therefore happy to proceed with this.

[mikeshulman]

Thanks for giving this a try! I guess I'm on the fence too.

I feel like a smarter exists tactic ought to be able to notice that Contr A can only be built by one constructor, and if we could "coerce from Funclass to something else" then intros ought to work for proving other IsTruncs, but that's just wishing.

Do we have any sense for how much mileage we get out of cumulativity?

[jdchristensen]

With the latest commit, the library builds. I did have to use "Admitted" for two results where universe variables are causing issues, and I didn't have time to investigate. One is hartogs_number_no_injection in Sets/Hartogs.v, and the other is Book_4_6_iii in HoTTBookExercises.v. Both probably just need a few universe annotations. If anyone wants to help, that would be great. I'm tagging @dominik-kirst, who may be able to figure out what universes things should live in in that result.

[jdchristensen]

Do we have any sense for how much mileage we get out of cumulativity?

I'm not sure yet. So far, it has caused problems in two places, but there's a chance that if we now tighten up some universe variables in earlier proofs, those problems would go away.

I do like that Overture.v has gotten simpler, without those various typeclass hints. And most of the changes to the rest of the library were just adding constructors, which isn't a big deal.

I just tried setting minimization to set globally, and around 300 files build, with just 6 failures, which is a bit better than before this PR. I haven't looked into how hard it would be to fix the errors.

[jdchristensen]

I did some timing tests, and this PR speeds things up by about 6% for both -j1 and -j8 builds. And that's without any tuning for the new definition of IsTrunc, so I would guess that there is some low hanging fruit that would speed things up even more. It's also without reducing universe variables as should be possible with this PR. This speedup, combined with the cleanups to Overture.v, make me think it's best to go ahead with this PR, assuming that the two glitches with universe variables are easy to fix.

This PR improved a few proofs while repairing them, and I checked that those files didn't contribute significantly to the speedup. In fact, the files that improved the most were generally files that were not changed at all, or which had very minor changes. For example, the build time of Analysis/Locator.v is 49% of what it was before, even though it was not changed by this PR.

[mikeshulman]

That seems like a good argument!

[jdchristensen]

Rebased. All that is left is the universe issue in Hartogs.

[jdchristensen]

Ok, just a single universe annotation was needed to fix the last issue. @dominik-kirst , if you have a chance, could you confirm that when defining hartogs_number', it is reasonable to assume that the set B is in the same universe as A?

  Definition hartogs_number' : Ordinal.
  Proof.
    set (carrier := {B : Ordinal@{A _} & card B <= card A}).

[jdchristensen]

With the inductive definition of IsTrunc_internal, where Contr A is defined to be IsTrunc_internal A (-2), in this situation

Definition test {A : Type} (H : Contr A) (P : Contr A -> Type) : P H.
  destruct H.

Coq generates two goals, one for each constructor of IsTrunc_internal, even though only the first constructor makes sense:

 P (Build_Contr A center contr)
 P (istrunc_S A i)

This causes problems for both the issig tactic and the make_equiv tactic if there are Contr terms around. Is there a way to make Coq smarter about this? (It might also be nice if it was smarter in the successor case as well.)

Note that when there is a goal of the form Contr A, econstructor knows that it has to apply the first constructor. But our custom ntc_constructor gets confused because it uses destruct internally. (make_equiv uses elim internally, giving the same problem.)

[mikeshulman]

Could we just write a replacement for destruct that does the right thing?

[jdchristensen]

Could we just write a replacement for destruct that does the right thing?

destruct, elim and induction all face this issue (and maybe others). Is there one thing we can change that will fix all of them?

Also, when we are trying to prove something of the form forall (n : trunc_index) (t : IsTrunc_internal A n), P n t (such as isequiv_istrunc_unfold) then we do want the existing induction principle. It's not clear to me how the tactic will know which we want.

I feel like there must be a standard solution to this, since it also comes up with things like vectors.

[Alizter]

@jdchristensen Vectors are unfortunately very poorly behaved and hardly used in Coq. Mainly for these reasons. FTR induction is capable of using different induction principles.

[Alizter]

cc @SkySkimmer @JasonGross Any ideas how to fix pattern matching on indexed inductives with destruct?

[mikeshulman]

Well, one thing that could in principle be done is to convert the index to a non-uniform parameter. That would also fix the ordering issue without an extra notation.

Inductive IsTrunc (n : trunc_index) (A : Type@{u}) : Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), (minus_two = n) -> IsTrunc n A
| istrunc_S : forall {k:trunc_index}, (forall x y:A, IsTrunc k (x = y)) -> (trunc_S k = n) -> IsTrunc n A.

Then destruct would still produce two goals in the objectionable cases, but one of them would be trivial with discriminate.

[SkySkimmer]

You could use inversion instead of destruct if you don't care about the term it generates. If you do care I'm not sure what you expect destruct to do.
I don't think there's any point using induction pn IsTrunc with non-variable index.
I don't know what elim does that destruct doesn't.

[jdchristensen]

I tried the version of IsTrunc with n as a parameter, and having to deal with the equalities is awkward. Moreover, destruct still generates two goals, and my hope is to make things like issig and make_equiv work automatically, so this change wouldn't help with that.

I tried inversion, and maybe it's just user error, but it still generated two goals, and in neither case was the term H in the goal destructed.

I also tried replacing elim with destruct in decomposing_intros (part of make_equiv), and make_equiv no longer works. So I guess we'd need custom versions of both tactics if we went that route.

For now, I've pushed a change that at least makes make_equiv work. (issig is a touch harder, and we can fix it later if it is needed.) Contr_ind is located in Equivalences.v since it uses equiv_ind, and since that is where make_equiv is. The match to determine the family P greatly speeds this up. Is this a reasonable compromise for now? While I'd like to have a more general solution, it's not like we'll be doing induction on elements of IsTrunc very often.

[Alizter]

@jdchristensen You might need dependent inversion. Mike's idea is basically inversion but the tactic goes a step further and tries to eliminate the index equalities.

[jdchristensen]

@jdchristensen You might need dependent inversion. Mike's idea is basically inversion but the tactic goes a step further and tries to eliminate the index equalities.

I had tried dependent inversion and it didn't work either. Anyways, I don't think we want ugly proof terms.

As an aside, I just replaced the equiv_ind proof of Contr_ind with a direct proof using match, since it seems better to prove something that fundamental with a proof that is closer to the metal.

I'm happy to merge this as is, unless anyone wants to look at it further.

[Alizter]

LGTM, feel free to merge.

[mikeshulman]

Sure, that seems fine to me for now.