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

[Jason Gross]

It's an example of a more systematic way of dealing with something;
something that you could do in an ad-hoc way without HoTT, but you probably
wouldn't think to do systematically.

Higher inductive types are the typical example of something that no-one had
thought up pre-HoTT, and which can't be done in vanilla Coq (or Agda,
etc.).  You can use these to define quotients, truncation (squash), and
types like the interval (which lets you prove functional extensionality)
and the circle.  Also a way of defining the reals via the hyper-reals which
has nice constructive properties.

-Jason


On Tue, Feb 4, 2014 at 4:50 PM, David Darais <david.darais at gmail.com> wrote:

> Can you elaborate on this last point?
>
> > 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.
>
> Is the example you just gave a witness of something you couldn't do
> before, or a more systematic way of dealing with something?  If it's the
> latter, can you comment on something that satisfies the former?
>
> Not trying to be confrontational.  I'm just as excited about HoTT as the
> next guy.
>
> Thanks,
> David
>
> On Feb 4, 2014, at 4:15 PM, Jason Gross <jasongross9 at gmail.com> wrote:
>
> > 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
> >
> > _______________________________________________
> > HoTT-reading-group mailing list
> > HoTT-reading-group at mit.edu
> > http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140204/23bf8ec0/attachment.htm