The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Even if you stick to the definition that you gave, you can prove a restricted proof-irrevelance for this case, namely:

Lemma lt_unique : forall n m (H1 H2 : n < m), H1 = H2.

  (if you're lost with the proofs it is contained in the CoLoR library: http://color.inria.fr/doc/CoLoR.Util.Nat.NatUtil.html#lt_unique)

  Best,

  Adam

On Wed, Feb 10, 2010 at 17:04, Nadeem Abdul Hamid <nadeem AT acm.org> 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

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [15 rue Berlier, 75013 Paris, France]
Sent from Amsterdam, NH, Netherlands