The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

By the way, Jasper Hugunin a while ago separated the proof of adjunction from the HoTT library, in case anyone needs it elsewhere. We use it in our code: https://github.com/uwplse/pumpkin-pi/blob/master/plugin/theories/Adjoint.v

From that we get a modified version of Gaëtan's proof with no dependencies on the HoTT modules:

Definition section_adjoint := Adjoint.fg_id' g f retraction section.

Lemma is_adjoint (a : A) : retraction (f a) = f_equal f (section_adjoint a).
Proof.
  apply Adjoint.g_adjoint.
Qed.

Lemma beer:
  forall (P : B -> Type) (a : A) (f0 : forall a : A, P (f a)),
    eq_rect (f (g (f a))) P (f0 (g (f a))) (f a) (retraction (f a)) = f0 a.
Proof.

  intros.

  rewrite is_adjoint.
  destruct (section_adjoint a).
  reflexivity.
Qed.

Jason, about your intuition: I'd had the adjoint versions of section and retraction floating around in my code for a while, figuring they were relevant, but I never figured out how to use them until I saw Gaëtan's proof. In particular, I was surprised that this goal:

eq_rect (f (g (f a))) P (f0 (g (f a))) (f a) (f_equal f (section_adjoint a)) = f0 a

was easily solved by destructing over (section_adjoint a) (like Gaëtan's proof), but the original goal:

eq_rect (f (g (f a))) P (f0 (g (f a))) (f a) (retraction (f a)) = f0 a

was not solved by destructing over (retraction (f a)) (Coq gives a type error if you try that). It wouldn't have occurred to me on my own that rewriting this proof obligation this way would have helped.

So, to make sure I understand correctly. The reason I can't destruct over retraction (f a) is because, as you said:

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.

since:

retraction (f a) : f (g (f a)) = f a

But thanks to adjunction, we get:

retraction (f a) = f_equal f (section_adjoint a)

where:

section_adjoint : g (f a) = a

and we can destruct over such an equality?

I know (or hope) I'm just parroting what you said, I just want to make sure I get it so that when I encounter proof obligations like this in the future, I don't have to bribe the community to help me :)

Talia

On Sat, Oct 10, 2020 at 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
> >
> >
> >