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

[Gregory Malecha]

Thanks Jason. This seems very interesting. You wouldn't happen to have this
(or something like it) in a Coq buffer would you? If not, I can see if I
can figure out how it works (maybe it would be an interesting thing to talk
about next Monday).



On Tue, Feb 4, 2014 at 4:58 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> 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
>>
>>
>


-- 
gregory malecha
http://www.people.fas.harvard.edu/~gmalecha/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140205/7eb6bc03/attachment-0001.htm