The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume,

> There has been a lot of confusion in this thread. While decidable equality 
> is
> the reason why it is possible in the first place, Coq does not care about 
> it at
> all. As Hugo explained, Coq just happens to implement a limited version of
> the small inversion trick.

Thanks for the clarification!

I wonder if it wouldn't be a better approach to have a type class for 
decidable equality (in the standard library) and a variant of UIP_dec which 
takes an instance of such a type class to solve "Proof irrelevance of 
equalities" goals. It would be a simple apply with some straight forward type 
class inference then.

I would think this would work in cases, the small inversion trick doesn't 
(e.g. if one of the terms is unknown), and if it doesn't work it would be 
more obvious why and how to fix it. Also the proof term should be much 
simpler then, since it would reuse existing lemmas.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928