Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert)


Chronological Thread 
  • From: Larry Lee <llee454 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert)
  • Date: Sat, 10 Oct 2020 13:18:40 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=llee454 AT gmail.com; spf=Pass smtp.mailfrom=llee454 AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f68.google.com
  • Ironport-phdr: 9a23:cRBgRRJKPovdnAiAy9mcpTZWNBhigK39O0sv0rFitYgeK//xwZ3uMQTl6Ol3ixeRBMOHsq0C1rGd6vm4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLBi7owrdutQLjYd+N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9g6BVoByhqRJxwJPabp+JO/RxZa7dYcoaSHBdUspNSyBMAIWxZJYPAeobOuZYqpHwqV0UohukHwmtBP7kxDlWiXDowKY31OAhEQXY0wM+EN8DsHvZoc76NKcXS++1za3IwS/fYPNR3Dfw8Y7FeQ0urv+QR7x/a9bRyVUxGAPfiFWdsZLoMy+L2ukQvGWX8fdtWO2hhWM7qgx8vjehyMgyh4TKmI4Z1F7J+CdlzYs1OdG0VlN3bN+qHZZQsyyXK5d6T90kTmp1tig6zbgGtoS6fCgM0JknwwTQa+adc4mI5hLsSvieLS1khH17ZL2/hxC/+lWjxO3kTsS4zkpGoy5fntTPtn0BzQHf58mGR/dn/0qs2jCC3B3J5O5eO0A7j6/bJoYhwrEukpoTtlzOHirsl0X3iK+ab0Qk+u+15+j+bLXrp5yRO5V7igH5NaQulci/DvoiPgcSWGib/Pyw1Lzl/ULnXLVHluM6nrXdvZzAJskWprS1DxJU34si8RqyDjSr3MwdnXYdLVJFfByHj5LuO1HLOP34CfO/jEqynzpkx/3LMabsAprILnfZkbfheaxx5FJbyAo21dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUNW4QpBt2aOHnwAmGVTNeOyvud6057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXUSCq6R8C/Q/4JLRmqDIphnzgDD+XzToYg0VSvs1a/xeQ3aOXT/SIcuNTo090nv7SCxyF3ziR9CoGm60/ISmh1mm0SQDpvhfJwpEV8zhGI1q0q2qUER+wW3OtAV0IBDbCZ1/ZzUomgVQfIf9PPQ1GjEI2r

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



Archive powered by MHonArc 2.6.19+.

Top of Page