[HoTT-reading-group] What HoTT gives you over vanilla Coq

[Jason Gross]

At the last meeting, Gregory, you asked about what you can do with HoTT-Coq
that you can't do with vanilla Coq.  (I've cc'd the mailing list in case
anyone else is interested too.)

Here's an example that you might be interested in.  Say you want to write a
"destruct under binders" tactic that, like [destruct] does to hypotheses
with sigma types, splits one hypothesis into two.  [destruct] never fails,
unless destructing induces unification (i.e., unless the inductive type has
indices).  So "destruct under binders" should never fail unless the
inductive type has indices.  It's currently highly nontrivial to write such
a tactic, even just for sigma types.  (It is probably possible;
essentially, you have to first eta-expand the hypothesis everywhere that it
appears in every other hypothesis and the goal, with some tricks to figure
out the right number of binders and to put the hypothesis in eta-long form,
then you use type-classes to generate the two new hypotheses, then you
change all references to projections of the old hypothesis with references
to the new ones (because they unify), again finding tricks to deal with
some kind of function-eta-long form, then you clearbody the new hypotheses,
and then you remove the old hypothesis.)  If you have the knowledge and
intuition of the HoTT library, you know that (un)currying is an
equivalence, and you can compose equivalences rather than use typeclass
resolution to get the functions, and, furthermore, you don't need to
eta-expand or deal with other trickiness, because you get that your old
hypothesis is equal to the inverse equivalence applied to your new
hypothesis, and you can use this to substitute it in the goal, possibly
with some care about generalizing things appropriately before rewriting.
 (Univalence might make things even easier.)  You could have done this all
without HoTT, but you might not have thought to do it systematically.
I think my general view is that it's not that HoTT gives you things you
couldn't do before (although it does), but it gives you a more systematic
way for dealing with things (proof irrelevance, equality, and perhaps
equivalences/isomorphisms being the main ones), and intuition for these
things.

I hope that helped a bit.

-Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140204/6d8b6524/attachment.htm