Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?


chronological Thread 
  • From: "Russell O'Connor" <roconnor AT Math.Berkeley.EDU>
  • To: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?
  • Date: Thu, 27 Nov 2003 08:39:10 -0800 (PST)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, 27 Nov 2003, Pierre Letouzey wrote:

> > (t1,t2:Z) (b1,b2:positive) (H1:(Zgcd t1 (POS b1))) (H2: (Zgcd t2 (POS b2))
> >   t1 = t2 -> b1 = b2 -> (mkRat t1 b1 H1) = (mkRat t2 b2 H2).
> >
> > Is this true in Coq?
>
> That sounds to me like proof irrelevance ... which is not there by
> default. So you end with sereral representation of 1/2, after all, unless
> you add a logical axiom.

I think it will be provable even without logical axioms.  I beleive that
is is a consquence of K_dec_set.

In general unique equality isn't provable, but when it is equality over a
decidable type (like Z) then it is.  Of course the real way to know this
is to prove it.  Which I'll do later if no one else here gets to it first.

-- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.





Archive powered by MhonArc 2.6.16.

Top of Page