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

[Jason Gross]

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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140205/3725a612/attachment.htm