Update Forall.v

Variation on dpath_forall
Fiddling.

Signed-off-by: jcmckeown <jesse@sockwright>
Use polymorphic [Axiom]s, not the [admit] exploit

The newer versions of HoTT/coq support polymorphic axioms, and no longer
require the [admit] exploit.  This way, we have two fewer top-level
constants floating around.
Make [f_ap] more powerful

It now can use [apD10] and deal with some dependent functions.
Fix library so that it works with the newest coq

Closes #152
Speed up the issig tactics significantly

It now takes only 0.8 seconds for me to typecheck Record.v, rather than
the 48 seconds it used to take.

As an unintended side effect, the issig2 and issig3 tactics are now
significantly shorter and easier to understand, and the pattern is
trivial to extend (up to tracking nested projections).

On the other hand, our units and counits are now mangled, unfortunately.

This closes #157.

Here's a dump of a partial explanation about why this is faster, from
issue #157:

What's special about `equiv_adjointify` is that it's type is simpler.  I
only have to mention the fibration type once or twice, rather than n
times.  If you prove a similarly general lemma about the coherence of
the unit and counit which doesn't depend on what record I'm dealing
with, only on how many projections it has (and what they are), perhaps
that would be just as good.  (Perhaps there's a kind of "generalized
sigma type" where we can ask for the builder, the projections, and the
proofs of the elim/computation rules, and then prove something about
those, and maybe that would be faster.  I might try to play with this
idea a bit.)

It would be great if we could replace the `issig` tactics with `issig`
lemmas, which quantify over records, but Coq doesn't give us any syntax
to do so.  Using `let ... in ...` doesn't help at all.  Using
`abstract`, which I think is closest to hiding something behind a name
(well, an opaque one), doesn't seem to help in this case.  If you want
to play with the case I'm working with, it's at
https://github.com/JasonGross/HoTT-categories/blob/lax-comma-partial/theories/Comma/LaxCommaCategory.v#L130.
(If my git submodule setup, or anything else, is giving you trouble, let
me know.)

I don't fully understand the internals of Coq, and all of my knowledge
of what is fast and slow comes from the experiences I've had with slow
proofs.  These are the lessons I've drawn:  (I can try to elaborate on
any particular one of them if you want)

* Things tend to start getting slow at around 100 000 --- 1 000 000
  terms in the goal (when I say a goal has n terms, I mean that if I
  `Set Printing All.`, and run the output through a `wc -w`, the number
  outputted is n).
* If `admit` is slow, then you almost certainly need to back up; no
  matter what you do, you're probably not going to be faster than
  `admit`.  (I hypothesize that the slowness is either due to the size
  of the proof-tree so far, of the size of the type of the goal; my
  intuition suggests the latter is more probable than the former)
* Using `abstract` can help, especially when `Defined` or `Qed` is slow;
  I think that it combines the "does this full proof pass the kernel
  checker?" check with some ad-hoc type-checking done during proof
  generation.  I hear that `abstract` can help immensely with space/RAM
  issues, but I've never experienced this.  Sometimes `abstract` makes
  things slower for me, though you should always compare the build +
* `Defined`/`Qed` time, and not just the time to build the proof, when
  looking at how `abstract` changes things.
* The order of operations matters, especially when destructing things.
  There's a difference between applying a lemma to a projected component
  of a sigma type, versus destructing the sigma type and applying the
  lemma to the resulting component.  Very often, I've found that
  destructing sigma/record types is slow, but applying generic lemmas
  (such as `f_equal` or `ap`) to projected components is even slower,
  and so it helps to destruct my record types before applying lemmas.
  On the other hand, if a lemma takes the sigma type whole, it's often
  faster to not destruct it.
* Destructing sigma types (especially nested ones) is very slow.
  Destructing records is sometimes significantly faster.  (Compare the
  times of the `issect` and `isretr` in the `LaxCommaCategory.v` file I
  linked to above.  The one which destructs the record is at least a few
  order of magnitudes faster.)  The problem gets worse the more
  complicated the fibration (the `P` in the type `sigT P`) of the sigma
  type is.  I suspect this is because destructing records gets coded as
  a single `match` without needing many type annotations, where
  destructing nested sigmas gets coded as nested `match`es with many
  type annotations, and the size of the proof tree gets very large very
  quickly.
* The only time Coq does delta reduction (unfolding) seems to be when
  checking convertibility.  That means that previously defined lemmas
  which show up in a proof tree don't, themselves, significantly add to
  the size of the proof tree, nor (often) the time (unless the proof
  requires that they be convertible with, e.g., `idpath`), regardless of
  how big the lemma is when unfolded.
* Combining the previous with the fact that `abstract` often doesn't
  help much suggests that the size of the type of the goal becomes
  important long before the size of the existing proof tree becomes
  important.  (However, I tend to have experience with wide proof trees
  (where the type of each level is a very large term), rather than with
  deep ones; `abstract` is probably more useful for deep proof trees.)
Fix a typo, FunExt -> Funext; now things compile

I believe this was due to a merge conflict between
74fddcd8b492cfa92874d606c6e3d6b9629a28ad and
64dcc4f24a23ff532ff27f2e44980e9faf39e0da.  I think this was because
e4f905e4afbc55f6f0bc0011f00bd3c5885a2849 was a merge from HoTT/HoTT,
rather than a rebase on top of it.
Fix library so that it works with the newest coq

Closes #152
Add types/Sum

This closes #127.

This makes (at least) partial progress on #53.
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.
Make Unit a Set

Having Unit in Prop causing issues and universe inconsistencies, such as
https://github.com/HoTT/coq/issues/50.
Fix a typo, FunExt -> Funext; now things compile

I believe this was due to a merge conflict between
74fddcd8b492cfa92874d606c6e3d6b9629a28ad and
64dcc4f24a23ff532ff27f2e44980e9faf39e0da.  I think this was because
e4f905e4afbc55f6f0bc0011f00bd3c5885a2849 was a merge from HoTT/HoTT,
rather than a rebase on top of it.
Fix library so that it works with the newest coq

Closes #152
Make Unit a Set

Having Unit in Prop causing issues and universe inconsistencies, such as
https://github.com/HoTT/coq/issues/50.
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.
Merge pull request #145 from JasonGross/polymorphic-axioms

Use [Admitted] rather than [admit] for axioms.
Merge branch 'master' of https://github.com/jcmckeown/HoTT
Getting sections closed correctly
Better description of dsigma_forall'
Merge branch 'master' of github.com:HoTT/HoTT