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: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
- Date: Thu, 18 Aug 2016 09:48:38 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
- Ironport-phdr: 9a23:0KeN9R+VDMjmZf9uRHKM819IXTAuvvDOBiVQ1KB91OscTK2v8tzYMVDF4r011RmSDNydsa4P1bSe8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuJP04W2nL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRAIPaD9uoZW3/VmeFUrcrkcbB24Ri19DBxXPxBD8RJb49CXg5cRn3yzPH8rwRKw0UDLqy6pqVhLulG9TNTk/8WLajsF9pK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MMDyE=
On 08/18/2016 06:09 AM, Soegtrop, Michael wrote:
Dear Guillaume,
There has been a lot of confusion in this thread. While decidable equality isThanks for the clarification!
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.
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.
One can already do this, to some extent. The procedure involves declaring sumbool to be an Existing Class, and then declaring each decidable equality an Existing Instance. Then, applying Eqdep_dec.UIP_dec will automatically infer the necessary instance.
I've used this in https://github.com/jonleivent/deptacs.
I'm not so much a fan of Existing Class as a standard way to get this done, mostly because it is not a controllable declaration (there is no Local variant, and it greedily makes instances out of all subsequent matching declarations (but not definitions!).). Having an alternative definition of UIP_dec that expects an actual typeclass instance instead would be better, if all of the individual eqdec definitions were instances.
-- Jonathan
- 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?, Jonathan Leivent, 08/18/2016
- 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.