The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

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