[Agda] Re: Irrationality proof

[N. Raghavendra]

Hi,

I've put the proof I've written for the irrationality of square roots of
primes at http://www.retrotexts.net/agda/My/Surd/ .  The files contain
an adaptation of Coquand's formal proof of the fact that certain primes
in cancellative commutative semigroups don't have "rational" square
roots.  I've also uploaded a definition of positive numbers, and will
soon add to it an Agda proof that square roots of prime numbers are
irrational.

There's nothing original or non-trivial in these files.  It's just a
project to learn Agda.  I've tried to use the stdlib as much as
possible, and enjoyed doing so.

Suggestions and criticism are welcome.

Cheers,
Raghu.

----------------------------------------------------------------------

At 2015-02-20T11:51:16+05:30, N. Raghavendra wrote:

> Hi,
>
> I am trying to understand Coquand's formalisation of a proof of the
> irrationality of the square root of 2.  (It was discussed here earlier
> too, http://thread.gmane.org/gmane.comp.lang.agda/3301/)  He proves that
> if A is a cancellative commutative semigroup, and if p is a prime
> element of A such that the relation
>
> multiple p = (x -> y -> p*x==y)
>
> on A is Noetherian, then there are no a and b in A such that p*a^2==b^2:
>
> (p:A) -> Prime p -> Noether A (multiple p) -> isNotSquare p.
>
> I am stuck when he says that this applies the case where A is the
> semigroup of strictly positive integers, and p is any prime there, e.g.,
> 2.  I don't see how to prove that the relation (multiple 2) on this A is
> Noetherian.  The definition of Noetherian is
>
> (P:Pred A) -> ((x:A) -> ((y:A) -> 2*y==x -> P y) -> P x) -> (x:A) -> P x
>
> Perhaps I am missing something obvious.  Any suggestions?
>
> Thanks and cheers,
> Raghu

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/