The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> Now, I want to instantiate SIG with an implementation of A and B
> being a finite subset of natural numbers, e.g.
> 
> Definition A := { n:nat | n < 10 }.
> Definition B := { n:nat | n < 10 }.
> 
> Lemma a_eq_dec : forall (a a':A), a=a' \/ a<>a'.
> ...
> 
> The problem here is that I can only seem to establish this by
> introducing the proof_irrelevance axiom.
> 
> So the question is: Does anyone have other suggestions for defining
> concrete instantiations of A and B as finite subsets of the natural
> numbers, that would allow proof of the a_eq_dec property without
> introducing proof irrelevance?

Defining decidable operators as functions to bool, as in the "small
scale reflection" approach, is indeed a nice way to get
proof-irrelevance for free (and more generally an interesting
alternative to the "sumbool" approach to decidability).

Regarding "<" in particular, the way it is defined in the Coq standard
library implies that there is only one closed proof of any "n < m"
statement. In particular, proof-irrelevance for "<" is provable
(see e.g. question 138 of the FAQ, currently at
http://coq.inria.fr/node/16?som=5#le-uniqueness).

More generally, irrelevance is a "natural" property of proofs that has
been considered for a few years now for addition to the Calculus of
Inductive Constructions (see e.g. Benjamin Werner's IJCAR '06
paper). Afaik a few theoretical and practical issues remain but the
general opinion and pronostic is that Coq will eventually enforce
proof-irrelevance natively (i.e. in the conversion rule). In
particular, I would not consider using the proof-irrelevance axiom as
"bad", but just as an anticipation of some future state where it will
be transparently available in Coq.

Hugo Herbelin