The Coq mailing list

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

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