The Coq mailing list

[Larry Lee <llee454 AT gmail.com>]

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