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: 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 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.

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




Archive powered by MHonArc 2.6.18.

Top of Page