The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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