Written by: Ikegami Daisuke [email protected]
Revised by: Sergei Romanenko [email protected]
The original proof (in Agda1/Alfa) is due to Thierry Coquand.
This version tries to exploit the the Agda standard library.
- Agda
http://wiki.portal.chalmers.se/agda/pmwiki.php - Agda standard library
http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary - The original proof on Agda1/Alfa
http://www.cs.ru.nl/~freek/comparison/files/agda.alfa - The paper
http://www.cs.ru.nl/~freek/comparison/comparison.pdf - Other proofs by another different proof assistants
http://www.cs.ru.nl/~freek/comparison/
-
Cancellative.agda
The definition of cancellative abelian monoid. -
Theorem.agda
The main theorem which is originally proved by Thierry Coquand: any prime cannot be a square of rational in cancellative abelian monoid.
-
2Divides
Some properties of natural numbers (with zero). -
NatPlus.agda
A set of natural numbers without zero.
Corollary.agda
The set of the natural numbers without zero and multiplication forms a cancellative abelian monoid.
Thus, the square root of two is irrational.
-
Corbineau.Sqrt2
There is no m and n such that
n ≢ 0
andm * m ≡ 2 * (n * n)
Hence, sqrt 2 is irrational.
The proof in Coq has been originally written by Pierre Corbineau
http://www-verimag.imag.fr/~corbinea/ftp/programs/sqrt2.v
-
Danielsson.2IsPrime
2 is prime.
Originally written by Nils Anders Danielsson
https://lists.chalmers.se/pipermail/agda/2011/003464.html