The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/08/2013 12:07 PM, Dimitri Hendriks wrote:
> 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 <http://coq.inria.fr/faq> 38 and
> 138)? Any alternatives?
All primitive propositions in

  let (a,b) := x in a > 0 /\ b > 0 /\ gcd a b = 1

are proof irrelevant, and proof irrelevant propositions are closed under 
conjunction. So, the whole proposition is proof irrelevant.

* For proof irrelevance of a > 0 and b > 0 use

  https://sympa.inria.fr/sympa/arc/coq-club/2013-04/msg00034.html

* For proof irrelevance of gcd a b = 1 use

  http://coq.inria.fr/stdlib/Coq.Logic.Eqdep_dec.html

Cheers,

Robbert