<div dir="ltr">Thanks Jason.<div><br></div><div>This is going to take some time for me to understand. I should be able to get to it by Monday though.</div><div><br></div><div>Thanks again.</div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Wed, Feb 5, 2014 at 4:21 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><a href="https://gist.github.com/JasonGross/8831581" target="_blank">Here's</a> a version without HoTT that only works when the hypothesis doesn't show up in the goal, and <a href="https://gist.github.com/JasonGross/8832741" target="_blank">here's</a> 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 <a href="https://github.com/HoTT/HoTT/pull/313" target="_blank">https://github.com/HoTT/HoTT/pull/313</a> for some unfolding). If I can get that merged (<a href="https://github.com/HoTT/HoTT/issues/314" target="_blank">https://github.com/HoTT/HoTT/issues/314</a>), 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).<div>
<br></div><div>There's an alternate version that uses currying explicitly (figuring that out is probably a decent exercise), and if you use <a href="https://github.com/mattam82/coq/tree/polyproj" target="_blank">the version of Coq that has judgmental eta for records</a>, 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).</div>
<span class="HOEnZb"><font color="#888888">
<div><br></div><div>-Jason</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Feb 5, 2014 at 9:55 AM, Gregory Malecha <span dir="ltr"><<a href="mailto:gmalecha@cs.harvard.edu" target="_blank">gmalecha@cs.harvard.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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).<div>
<br></div></div><div class="gmail_extra"><div><div><br><br><div class="gmail_quote">On Tue, Feb 4, 2014 at 4:58 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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.<div>
<br></div><div>
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.</div>
<span><font color="#888888">
<div><br></div><div>-Jason</div></font></span></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 4, 2014 at 4:50 PM, David Darais <span dir="ltr"><<a href="mailto:david.darais@gmail.com" target="_blank">david.darais@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Can you elaborate on this last point?<br>
<div><br>
> 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.<br>
<br>
</div>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?<br>
<br>
Not trying to be confrontational. I’m just as excited about HoTT as the next guy.<br>
<br>
Thanks,<br>
David<br>
<div><div><br>
On Feb 4, 2014, at 4:15 PM, Jason Gross <<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>> wrote:<br>
<br>
> 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.)<br>
><br>
> 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.<br>
> 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.<br>
><br>
> I hope that helped a bit.<br>
><br>
> -Jason<br>
><br>
</div></div>> _______________________________________________<br>
> HoTT-reading-group mailing list<br>
> <a href="mailto:HoTT-reading-group@mit.edu" target="_blank">HoTT-reading-group@mit.edu</a><br>
> <a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br>
</blockquote></div><br></div>
</div></div></blockquote></div><br><br clear="all"><div><br></div></div></div><span><font color="#888888">-- <br><div dir="ltr">gregory malecha<br><div><a href="http://www.people.fas.harvard.edu/~gmalecha/" target="_blank">http://www.people.fas.harvard.edu/~gmalecha/</a></div>
</div>
</font></span></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr">gregory malecha<br><div><a href="http://www.people.fas.harvard.edu/~gmalecha/" target="_blank">http://www.people.fas.harvard.edu/~gmalecha/</a></div>
</div>
</div>