The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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
You can use a limited form of proof irrelevance that does not rely on an 
axiom.
1/ In standard Coq, it is possible to prove that proofs of equality 
between boolean values are unique.
2/ you can define a function ltb so that n < 10 <-> ltb n 10 = true
3/ you define A as : { n:nat | ltb n = true}
4/ with this definition of A, you can prove a_eq_dec

For the proof that proofs of equality between booleans, look there:

http://old.nabble.com/Re:-FMaps-and-proof-irrelevance-p25505519.html

Note that in that message, I only rephrase results that were obtained by 
other researchers.

Yves