HoTT/HoTT — pull request #162 by JasonGross (2013-08-02 07:39:56+00:00)
Title: Add priorities to typeclass instances

The default priorities are rediculously high (small numbers), equal to
the number of (typeclass?) arguments to the instance. Instead, I've
defaulted to 1000 for most instances, 10000 for the instances that are
likely to lead to cycles or information flow in the wrong direction, 100
for instances which I think are likely to lead to speedy resolution, and
0 for instances which have no typeclass arguments (and thus discharge
their goals immediately). (Smaller numbers are higher priority.)

Additionally, I have renamed [Contr] to [Contr_internal] and made
[Contr] a notation for [IsTrunc minus_two]. This, combined with the
fact that [IsTrunc] is now [Opaque] in typeclass search, breaks [Contr]
-> [IsTrunc] -> [Contr] cycles. We now only do typeclass search on
[IsTrunc]. This requires iota-expanding a few instance declarations of
[Contr], to get around deficiencies in Coq's typeclass machinery; I've
submitted a bug report at
https://coq.inria.fr/bugs/show_bug.cgi?id=3101.

Now that all the instances are global, we pick up some instances in
FunextVarieties.v; I've removed the confused comments and explicit
instances.

I remove [hprop_forall] and the associated comment, because we have
[trunc_forall].

I've added some [Hint]s to typeclass search which trigger early and set
up the goal. It seems to me that we generally want to reason about
[IsTrunc (S n) A] rather than [IsTrunc n (a = b)]; the opaqueness of
[IsTrunc] (only to typeclass resolution), [istrunc_paths], and the [Hint
Extern]s I've added to [Overture.v], implement this.

The instance [contr_trunc_minus_two] is no longer; it's not useful,
because we instead want to use [progress change]. If we don't then we
can get into infinite loops because [contr_trunc_minus_two] can, up to
unificiation, be applied an arbitrary number of times.

There are a few proofs where I've changed [auto] to [auto with
typeclass_instances]; [auto] doesn't always work any more, though I
haven't looked into it very closely. I think it's reasonable to need to
inform Coq that you're doing typeclass resolution.

The proof of [trunc_equiv] needed to be modified so we don't loop
infinitely on [eapply I]. I'm annoyed that the context seems to take
precedence over cost 0 hints. However, this is a fairly foundational
proof, and I don't anticipate this kind of problem popping up in
typeclass search often.

This makes my category theory library compile twice as fast, and doesn't
significantly effect the total compile time of the HoTT library.