The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Robbert, Arnaud,

Many thanks for your help! It works out well. 

I now have the bijection from (list two) to Q, 
as part of a formalization of the Calkin-Wilf tree:
http://www.cs.vu.nl/~diem/coq/calkin-wilf/ .
In particular, your hints are used here:
http://www.cs.vu.nl/~diem/coq/calkin-wilf/cw.html#Q .

Dimitri

On Oct 8, 2013, at 13:01 , Robbert Krebbers wrote:

> 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
> 
>