coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Shortening proofs that the square root of 2 is non rational.

From: roconnor AT theorem.ca
To: fr�d�ric BESSON <fbesson AT irisa.fr>
Cc: Yves Bertot <Yves.Bertot AT sophia.inria.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Shortening proofs that the square root of 2 is non rational.
Date: Tue, 17 Apr 2007 10:30:33 -0400 (EDT)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, 16 Apr 2007, fr�d�ric BESSON wrote:

Theorem sqrt2_not_rational : ~exists n, exists p, n ^2 = 2* p^2 /\ n <> 0.

Now that we have standard rationals (QArith), I think the statement should read as follows.

Theorem sqrt2_not_rational : ~exists (x:Q), x^2 = 2.

--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

[Coq-Club] Shortening proofs that the square root of 2 is non rational., Yves Bertot
- [Coq-Club] Elliptic curve in Coq, Thery Laurent
- Re: [Coq-Club] Shortening proofs that the square root of 2 is non rational., fr�d�ric BESSON
  - Re: [Coq-Club] Shortening proofs that the square root of 2 is non rational., roconnor
    - Re: [Coq-Club] Shortening proofs that the square root of 2 is non rational., Yves Bertot