The Coq mailing list

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

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