The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Test subject volunteers.

Also Iris got infected with homotopy type theory lately :) We're 
transporting equalities over our resource algebras.

See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/530#note_57508

On 10/10/2020 19.36, Xavier Leroy wrote:
> At any rate, Talia's message gave me an idea for a paper:
>
> " Q.e.d. or starve?  On the feeding habits of homotopy type theorists "
>
> I still need a few more test subjects, though :-)
>
> - Xavier
>
> On Sat, Oct 10, 2020 at 7:24 PM Derek Dreyer <dreyer AT mpi-sws.org 
> <mailto:dreyer AT mpi-sws.org>> wrote:
>
>     FYI: I don't think Talia was complaining: nerd sniping is fun.  I
>     sometimes nerd-snipe myself.
>
>     https://www.urbandictionary.com/define.php?term=Nerd%20Sniping
>
>
>     Derek
>
>     On Sat, Oct 10, 2020 at 7:19 PM Larry Lee <llee454 AT gmail.com
>     <mailto:llee454 AT gmail.com>> wrote:
>      >
>      > Hey Talia,
>      >
>      > Sorry to hear that you were "nerd sniped" over this. It's possible to
>      > prove the lemma you presented below:
>      >
>      > 1   Require Import ProofIrrelevance.
>      >   1 Require Import FunctionalExtensionality.
>      >   2
>      >   3 Parameter A : Type.
>      >   4 Parameter B : Type.
>      >   5 Parameter f : A -> B.
>      >   6 Parameter g : B -> A.
>      >   7 Axiom section : forall a, g (f a) = a.
>      >   8 Axiom retraction : forall b, f (g b) = b.
>      >   9
>      >  10 Goal
>      >  11   forall (P : B -> Type) (a : A) (f0 : forall a : A, P (f a)),
>      >  12   eq_rect
>      >  13     (f (g (f a)))
>      >  14     P
>      >  15     (f0 (g (f a)))
>      >  16     (f a)
>      >  17     (retraction (f a)) =
>      >  18   f0 a.
>      >  19 Proof.
>      >  20   intros P a f0.
>      >  21   rewrite <- (f_equal_dep (fun a => P (f a)) f0 (section a)).
>      >  22   rewrite (proof_irrelevance (f (g (f a)) = (f a)) (retraction (f
>      > a)) (f_equal f (section a))).
>      >  23   set (b := f a).
>      >  24   set (a0 := g b).
>      >  25   set (b0 := f a0).
>      >  26   assert (a0 = a).
>      >  27   + exact (section a).
>      >  28   + assert (b0 = b).
>      >  29     - exact (retraction b).
>      >  30     - exact (eq_sym (rew_map P f (section a) (f0 a0))).
>      >  31 Qed.
>      >
>      > I don't drink, but a pizza would be nice.
>      >
>      > - Larry Lee
>      > (http://larrylee.tech)
>      >
>      > On 10/10/20, Talia Ringer <tringer AT cs.washington.edu
>     <mailto:tringer AT cs.washington.edu>> wrote:
>      > > Thanks all, love the thought processes too, and happy to ship
>     some beer or
>      > > dessert or get it next conference :)
>      > >
>      > > On Sat, Oct 10, 2020, 7:53 AM Jason Gross
>     <jasongross9 AT gmail.com <mailto:jasongross9 AT gmail.com>> wrote:
>      > >
>      > >> I have not yet looked at Gaëtan's proof, but here is the
>     intuition:
>      > >> What you have is a sort of incoherent equivalence.  What would
>     make
>      > >> your proof easier is having some version of [section] such that
>      > >> [forall a, f_equal f (section a) = retraction (f a)], so that
>     you were
>      > >> dealing with a coherent equivalence instead.  Since your proof
>     goal
>      > >> only uses [retraction], it should be possible to "adjust"
>     [section] so
>      > >> that it satisfies this equation; I suspect that this is what
>     most of
>      > >> Gaëtan's proof is about.  Once you have this additional lemma,
>     your
>      > >> goal is quite straight forward: supposing you have this lemma
>     as [H],
>      > >> you can solve your goal with [rewrite <- H; generalize
>     (section a);
>      > >> generalize (g (f a)); intros; subst; reflexivity.]
>      > >>
>      > >> The underlying intuition that I had here is that the thing
>     getting in
>      > >> the way of the "naive proof" is that you can't just destruct an
>      > >> equality [e] of type [f a0 = f a], because you can't
>     generalize over
>      > >> the two sides.  But since f is an equivalence, HoTT tells us
>     that we
>      > >> can get that [e = ap f <something>] (i.e., [e = f_equal f
>      > >> <something>], where <something> is going to be [ap g e]
>     adjusted so
>      > >> the endpoints line up.  Once you get this, you can just
>     destruct the
>      > >> <something>, and you're golden.
>      > >>
>      > >> (Note that if your goal also mentioned [section], then you'd
>     almost
>      > >> surely be sunk without having an extra hypothesis which related
>      > >> [section] and [retraction].)
>      > >>
>      > >> On Sat, Oct 10, 2020 at 4:00 AM Gaëtan Gilbert
>      > >> <gaetan.gilbert AT skyskimmer.net
>     <mailto:gaetan.gilbert AT skyskimmer.net>> wrote:
>      > >> >
>      > >> > It's proved. HoTT is the only place I know to get lemmas
>     about equality
>      > >> from so that's what I used, but this is axiom less so can be
>     done without
>      > >> HoTT too.
>      > >> >
>      > >> > Thought process:
>      > >> > - eq_rect is complicated, let's turn it into transport to
>     simplify the
>      > >> goal
>      > >> >    this worked but is not actually useful in the end
>      > >> > - maybe there's a fancy destruct which will work (simple
>     proofs about
>      > >> equality are all about the well chosen destruct)
>      > >> >    this went nowhere fast
>      > >> > - maybe I can construct a counterexample using univalence on
>     boolean
>      > >> negation
>      > >> >    obviously this couldn't work
>      > >> > - this looks like the incomplete IsEquiv from HoTT where we can
>      > >> construct some fancy equality proofs to get the full IsEquiv stuff
>      > >> >    let's look at the construction to see if I get any ideas
>      > >> >    a bit of messing about then leads to the solution
>      > >> >
>      > >> > Gaëtan Gilbert
>      > >> >
>      > >> > On 10/10/2020 08:11, Talia Ringer wrote:
>      > >> > > Hello friends,
>      > >> > >
>      > >> > > I got nerd sniped this morning on a proof task I've been
>     at for like
>      > >> 11 hours. Most of the proof obligations are done now, but I
>     ended up
>      > >> stuck
>      > >> at one particular proof obligation that I'm not sure how to
>     solve, or if
>      > >> it
>      > >> is solvable in general. But also I need to work on job
>     applications and
>      > >> normal last year of grad school things, and I haven't eaten
>     dinner. So if
>      > >> you help me out with this one proof obligation, I'll give you
>     appropriate
>      > >> credit and also get you a beer or dessert.
>      > >> > >
>      > >> > > For real. I don't have technical mentors or local expertise to
>      > >> > > consult.
>      > >> > >
>      > >> > > Essentially, I have two types:
>      > >> > >
>      > >> > >     A : Type
>      > >> > >
>      > >> > >     B : Type
>      > >> > >
>      > >> > > that are equivalent:
>      > >> > >
>      > >> > >     f : A -> B
>      > >> > >
>      > >> > >     g : B -> A
>      > >> > >     section : forall a, g (f a) = a.
>      > >> > >     retraction : forall b, f (g b) = b.
>      > >> > >
>      > >> > >
>      > >> > > I know literally nothing else about my types or my
>     equivalence. *I
>      > >> want to know if it is possible to solve this proof obligation:*
>      > >> > >
>      > >> > >     *P : B -> Type
>      > >> > >     a : A
>      > >> > >     f0 : forall a : A, P (f a)
>      > >> > >     ______________________________________(1/1)
>      > >> > >     eq_rect (f (g (f a))) P (f0 (g (f a))) (f a)
>     (retraction (f a)) =
>      > >> f0 a*
>      > >> > >
>      > >> > >
>      > >> > > (I have already solved this proof obligation:
>      > >> > >
>      > >> > >     a : A
>      > >> > >     ______________________________________(1/1)
>      > >> > >     eq_rect (f (g (f a))) (fun _ : B => A) (g (f a)) (f a)
>      > >> > > (retraction
>      > >> (f a)) = a
>      > >> > >
>      > >> > > Literally just "rewrite retraction. apply section." works.
>     But that
>      > >> didn't help me, and I also couldn't get Coq to use the same
>     tactics.)
>      > >> > >
>      > >> > > I can't figure out whether this is me being really bad at
>     equalities
>      > >> of equalities and dependent rewrites, or whether there is
>     something we
>      > >> must
>      > >> know about A, B, or our equivalence for this to hold, or
>     whether there is
>      > >> an additional axiom we must assume for this to hold in
>     general. And it's
>      > >> 11:00 PM and I haven't eaten dinner, so time to ask you all:
>      > >> > >
>      > >> > >   * Is this provable? If so, how? (And why am I so bad at
>     equalities
>      > >> of equalities?)
>      > >> > >   * If it is not, can you explain why?
>      > >> > >   * Is there anything I could assume about A and B to make it
>      > >> > > provable?
>      > >> > >   * Is there anything I could assume about f, g, section, or
>      > >> retraction to make it provable?
>      > >> > >
>      > >> > > Hopefully someone else finds this fun, too. Or really
>     likes beer.
>      > >> > >
>      > >> > > Talia
>      > >> > >
>      > >> > >
>      > >> > >
>      > >>
>      > >