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

Wed Feb 5 23:19:19 EST 2014

Thanks Jason.

This is going to take some time for me to understand. I should be able to
get to it by Monday though.

Thanks again.

On Wed, Feb 5, 2014 at 4:21 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> Here's <https://gist.github.com/JasonGross/8831581> a version without
> HoTT that only works when the hypothesis doesn't show up in the goal, and
> here's <https://gist.github.com/JasonGross/8832741> a version with HoTT
> that should work even if the hypothesis is in the goal (both include a
> version for [and] that's much shorter, and works only when the hypothesis
> isn't in the goal).  The HoTT version is a bit longer, but that's because
> I've included a lemma about the type-theoretic axiom of choice being an
> equivalence (the code also depends on
> https://github.com/HoTT/HoTT/pull/313 for some unfolding).  If I can get
> that merged (https://github.com/HoTT/HoTT/issues/314), then the lengths
> will be comparable, even though the HoTT version is doing a lot more (of
> course, if you include the length of the prerequisite machinery in the HoTT
> library, it's very long).
>
> There's an alternate version that uses currying explicitly (figuring that
> out is probably a decent exercise), and if you use the version of Coq
> that has judgmental eta for records<https://github.com/mattam82/coq/tree/polyproj>,
> I'm decently sure you can avoid using funext (because I think that with eta
> for records, both currying and the type-theoretic axiom of choice are
> judgmentally equivalences).
>
> -Jason
>
>
> On Wed, Feb 5, 2014 at 9:55 AM, Gregory Malecha <gmalecha at cs.harvard.edu>wrote:
>
>> 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/
>>
>
>

-- 
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/199154e3/attachment-0001.htm