The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

I believe this is the original:
https://xkcd.com/356/

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