coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Talia Ringer <tringer AT cs.washington.edu>
- To: Coq-Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert)
- Date: Fri, 9 Oct 2020 23:11:28 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ua1-f54.google.com
- Ironport-phdr: 9a23:2End+ROjXNH763qEhtYl6mtUPXoX/o7sNwtQ0KIMzox0Iv75rarrMEGX3/hxlliBBdydt6sbzbeM+PC7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLBi6swrdu8oYjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZI+hXtY39p1oUohCjGQesBeXvyjBWiX/swKY31PghERvH3AwmENIBrm7Uoc7pO6cJS+y0wrPHzS7Db/NX3zf955TIchcnof2WQ71/bNfRxFApGgjYgVqetZbrMCmJ1uQRrWeb9exgWPqghmI7rwx8rDehyMkihITNmo4Z1E3J+Dl2zoooIdC1VU51bcOrHZZOuCyXK4V7T8wgTmxmuSs3yaALtYO5cSULzpks2h3Ra+SffoSW/h7uUPydLDR4iX5/Zr6zmQi+/VKgx+DzUMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqh3CyA1wHX6u1dPEA7j7fXJ4cvwrMwmZcfq0vDHijxmEX5iK+ZaF8o9fSv6+Tiernmp5mcOJFoigzmLKgihsiyDf47PwUORWSX5/qw2KP58UD5T7hGlvg2nbPYsJDeK8QbvKm5AwpN34Y/8Ra/DjGm0NsGknkdN19KZAmHg5LnOl7UO/D4Dfa/g1KjkDd3wPDGOKftDYvQIXjeiLvhZ6py61ZAyAovytBS/45bCrYYIP7qRkDxsMHYAQQiPgyvw+fnDc192ZkEVWKOBK+ZKqLSvkWS6uIhOenfLLMS7R36Mr0O4+PkxSsynkZYdq2017MWbmq5F7JoORPKT2Drh4I9GGMLt0IETerlhUfKBSJJZnC9UrgU7Sp9F4u9DYbFSZyqhvqM0DrtTc4eXXxPFl3ZSSSgTI6DQfpZMHvOcP8kqSQNUP2ac6FkzQun7V6owKEhMePP+iweuo7k0p546/CBzUhjpwwxNNyU1iS2d08xm2oJQzEs26Um8B520RGc2LN4gvpXCdtVof5FT1VjbMOO/6lBE9n3Hzn5UJKJRVKhGIj0BDgwSpcsyoZLbRshXdqliR/H0myhBLpHz7E=
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 -> Asection : 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
- [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Talia Ringer, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Gaëtan Gilbert, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Jason Gross, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Talia Ringer, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Larry Lee, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Larry Lee, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Jason Gross, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Derek Dreyer, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Xavier Leroy, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Robbert Krebbers, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Bas Spitters, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Xavier Leroy, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Larry Lee, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Larry Lee, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Talia Ringer, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Jason Gross, 10/10/2020
- Re: [Coq-Club] Is this provable? (I'll give you credit and beer/dessert), Gaëtan Gilbert, 10/10/2020
Archive powered by MHonArc 2.6.19+.