The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Amin,

 

my question was about the “have” in “has decidable equality”. What does make the decidable equality of a type available, so that Coq “has” it? There are lemmas like list_eq_dec in the standard library, but just having a lemma is not enough for Coq using it somehow automatically.

 

I would expect that this is done via class type instances, e.g. for nat and list, but I couldn’t find a class type for decidable equality in the standard library, and even less instances for such a class type.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Amin Timany
Sent: Thursday, August 18, 2016 10:33 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?

 

Hi Micheal,

 

Decidable equality for A means that you can prove forall (x y : A), {x = y} + {~ x = y}. We can prove in general that if we have decidable equality for a type A for any two terms x y : A and H1 H2 : x = y, we have H1 = H2. This is proven in the library of Coq (https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html). I also once (just as an exercise) proved these theorems from scratch which you can find at https://gist.github.com/amintimany/798a096e2f2ff0582b36. What you are getting here in these proofs is (more or less) the same kind of proof for specific A x and y. In other words, when A is an inductive type with decidable equality and x and y are constructors Coq can figure (as hugo explained) the proof out.

 

Regards,

Amin

 

On 18 Aug 2016, at 10:01, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

 

Dear Jason,

 

you are right, my usage of the wording “literal term” was sloppy. I don’t have a good definition of “literal term”, which would exclude Set::nil.

 

But I don’t think I understand what exactly you mean by “has decidable equality”. A declared instance of some type class? I didn’t find a type class for decidability of equality in the standard library, just the HasEqDec module type. Also I tried it with some trivial ad hoc inductive types, for which for sure no type classes or canonical instances are defined, and it did work.

 

Many thanks to all who helped to explain this, especially to John Wiegley who gave the first answer, but whom I forgot to acknowledge in my first response – sorry!

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Jason Gross
Sent: Wednesday, August 17, 2016 9:56 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?

 

It only works if the type has decidable equality.  list nat has decidable equality.   It is also decidable whether or not a list of any type is nil, or not.  If you instead try (feq : Set::nil = Set::nil -> T), you will find that it does not work.  If you try (feq : Set = Set -> T) it will not work.  If you try (feq : list nat = list nat -> T), it will not work.  If you try (feq : S = S -> T) it will not work.  If you try (feq : eq_refl 0 = eq_refl 0 -> T), it may or may not work (this still has decidable equality, but it is more complicated).

 

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

 

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