The Coq mailing list

[Carsten Varming <varming AT cmu.edu>]

This has been dealt with in ssreflect. They make < into a function nat -> 
nat -> bool, and thus get proof irrelevance for free. They have also 
packaged this kind of reasoning very nicely in suitable structures. They 
have even defined the finite type you need and put some work into showing 
suitable lemmas you may need.

Carsten

On Wed, 10 Feb 2010, Nadeem Abdul Hamid wrote:

> I'm working on something where I try to prove properties of functions on some 
> parameterized sets -- i.e.
>
> Module Type SIG.
>
> Parameter A : Set.
> Parameter B : Set.
>
> Parameter a_eq_dec : forall (a a':A), a = a' \/ a <> a'.
>
> Parameter f : A -> B.
> .... properties of f ...
> End SIG.
>
> (* followed by some proofs in another functor of SIG that uses properties of 
> f *)
>
>
> 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?
>
> Thanks in advance,
> nadeem