The Coq mailing list

[Fabian Kunze <fkunze AT fakusb.de>]

Hi,

The lines you required to "Fail" do not fail for me.

I use the following version (output of "coqc -v"):
"The Coq Proof Assistant, version 8.5beta2 (August 2015) compiled on Aug 25 2015 12:59:17 with OCaml 4.02.3"

I friend of mine compiled it under "version 8.5beta2 (June 2015) " and "8.4pl6" and there yout issue still occured.

So maybe updating coq fixes the issue for you.

Best,

Fabian

Yannick <yannick.zakowski AT irisa.fr> schrieb am Di., 27. Okt. 2015 um 18:02 Uhr:

Dear Coq list,

Say I have functions of two arguments whose type of the second argument
depends on the value of the first. Assuming appropriate instances of
EqDec, I defined in my development a generic function to update such
functions.

However, trying to apply this generic update to functions whose second
argument actually does not depend on the first, I encountered issues
around which I can't quite wrap my head.

I tracked the problem down to the smallest example I could, that you
will find enclosed.

Essentially, the question boils down to proving:
forall _:K1, EqDec K2 eq
Knowing an instance of:
EqDec K2 eq

Which Coq manages by itself as long as K1 and K2 are variables, but
fails as soon as K2 is a "real" type, the vacuous one here for instance.

Please find in the attached file the more detailed situation.

Would anyone understand what is going on here, and hopefully know how to
fix it?

Many thanks,
Best,

Yannick