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 14:51:34 +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 mga14.intel.com
  • Ironport-phdr: 9a23:AKtYBh+JBD+7C/9uRHKM819IXTAuvvDOBiVQ1KB92+McTK2v8tzYMVDF4r011RmSDNydsa4P1Lqe8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuJP04X1HL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRGduD2dgrsbsrFzISRaFznoaSGQf1BRSSUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3pZxsRRD0kiAfc3Yc8WrXg8F0xuoPpROqpxVyx8jPZ4yaKOB5Zovce88XQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo/1Y=

Dear Pierre,

> OK but pattern matching cannot currently use such information to infer
> return clause. I think this is what Michael had in mind IIUC and it makes
> sense
> indeed.

actually my idea was to use "apply UIP_dec_typeclass" to solve "proof
irrelevance for equalities" goals rather than return clause inference. I
would prefer this because I think it is easier to understand.

I can imagine that extending return clause inference with type classes would
solve many of the "ill typed term" issues I ran into since I am experimenting
with dependent types. But I don't know how understandable this would be. It
is already quite complicated and hard to predict as is.

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