coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Pierre Letouzey
- [Coq-Club] Re: Coq Poll: What are your preferred rational numbers ?, Milad Niqui
- Message not available
- <Possible follow-ups>
- [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Thery Laurent
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Pierre Letouzey
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Russell O'Connor
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Venanzio Capretta
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Russell O'Connor
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Venanzio Capretta
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Benjamin Werner
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Pierre Courtieu
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Venanzio Capretta
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Russell O'Connor
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, Bruno Barras
- Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?,
Pierre Letouzey
Archive powered by MhonArc 2.6.16.