The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Hi all,

I have functions valq : list two -> Q and locq : Q -> list two, where two is a two-element set, and Q is the sigma type

Q := { x : nat*nat | let (a,b) := x in a > 0 /\ b > 0 /\ gcd a b = 1 }.

I have that valq is injective. Now for surjectivity I want to show that locq is a right-inverse of valq, i.e., forall r:Q, valq (locq r) = r. So I have to deal with equality between dependent pairs ... Do I need proof irrelevance, or can I somehow use that > and = are decidable on nat (as suggested by the answers to faq 38 and 138)? Any alternatives?

Further info: valq and locq are based on val : list two -> nat*nat, loc : nat*nat -> list two, and it holds that  forall a b, a > 0 -> b > 0 -> gcd a b = 1 -> val (loc (a,b)) = (a,b) .

Thanks for your suggestions, 

Dimitri