The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, proof irrelevance is one way. But in that particular case you can rephrase in an appropriate way Q to use that the condition is decidable:

supposing a test bgt : nat -> nat -> bool for strict comparison, and beq for equality (for instance those defined in the number library http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Natural.Peano.NPeano.html ).

Q := { x : nat*nat | ( let (a,b) := x in bgt a  0 && bgt b 0 /\ beq (gcd a b) 1 ) = true }

The trick, now, is that forall (b1 b2:bool) (p q:b1 = b2), p=q as mentioned in the faq items you cite (using Coq.Logic.Eqdep_dec.UIP_dec in conjunction with Coq.Bool.Bool.bool_dec).

From there, it is a simple exercise to prove that

forall x y:Q, proj1_sig x = proj1_sig y -> x = y

On 8 October 2013 12:07, Dimitri Hendriks <diem AT xs4all.nl> wrote:

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