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
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, (continued)
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jason Gross, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Maxime Dénès, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Hugo Herbelin, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Amin Timany, 08/18/2016
- RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Guillaume Melquiond, 08/18/2016
- RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jonathan Leivent, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Pierre Courtieu, 08/18/2016
- RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jason Gross, 08/18/2016
Archive powered by MHonArc 2.6.18.