Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
  • Date: Thu, 18 Aug 2016 10:09:16 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
  • Ironport-phdr: 9a23:SRGMsx1tTFlShEHwsmDT+DRfVm0co7zxezQtwd8ZsegfK/ad9pjvdHbS+e9qxAeQG96KsrQe0KGP6fyoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMS33HkO+86bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4FPIShLK7X8BWE0XlABJCk7L9luyCpz2q27xsvd38CicJ8z/C74uD2eM9aBuHVXTjyoIKyQ+6CWfr817jKtWpFjp8xl+yI7dbYXTL/1zcb/HessyRGxdU8IXXCtEVNDvJ7ATBvYMaL4L57L2oEED+EOz

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



Archive powered by MHonArc 2.6.18.

Top of Page