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?

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
Date: Thu, 18 Aug 2016 16:22:23 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:qtgDyBSfbfPFmTuXZ3AnCWYRktpsv+yvbD5Q0YIujvd0So/mwa64bRGN2/xhgRfzUJnB7Loc0qyN4vmmAzBLvszJ8ChbNscdD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbshsi6n9q/54fUK10RwmHsOPUocF7p902R7pBQ2to6bP5pi1PgmThhQ6xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/TGKdwaE52MdX2MKiVIIRlGdtFCpFqv25wD9r6JW3DSQdZn9SqlxUjC/5Y9qTgXpgWEJLWhq3nvQj5lIja9Buh/pjBti2ZLVbZzdYOJ/c7nHcJURQndbQsdcSgROB4q9a80ECO9XbrUQlJX0u1Zb9Uj2PgKrHu66j2YQ3nI=

2016-08-18 15:48 GMT+02:00 Jonathan Leivent
<jonikelee AT gmail.com>:
> On 08/18/2016 06:09 AM, Soegtrop, Michael wrote:
>> 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.

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.

Best
Pierre

Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, (continued)