Require Import ZArith Zwf QArith.
Open Scope Z_scope.

(* This proof encodes the numerical reasoning in a geometrical proof of
  irratianlity proposed by Stanley Tennenbaum and mentioned by Miller and
  Montague "Irrationality from the book"
  http://arxiv.org/abs/0909.4913v1

  The proof was actually found following another path, starting from the paper
  "Simple caonical representation of rational numbers", electronic Notes in
  Theoretical Computer Science, Vol. 85, Issue 7, Sept. 2003, Elsevier and
  using an oral remark by F. Wiedijk that sqrt(2) = ND (1/sqrt(2)).
*)

Lemma usqr : forall x, x ^ 2 = x * x.
Proof. intros; ring. Qed.

Lemma sqrt_lt_rev : forall x y, 0 < y -> x^2 < y^2 -> x < y.
Proof with auto with zarith.
intros x y Y M; apply Znot_ge_lt; intros yx; assert (y^2 <= x^2)...
apply Zle_trans with (y*x); rewrite usqr...
Qed.

Lemma nsqrtp : forall p q, 0 < p -> 0 < q -> p^2 <> 2*q^2.
Proof.
intros p; elim p using (well_founded_ind (Zwf_well_founded 0)); clear p.
intros p Ip q P Q E.
assert (0 < q^2) by (rewrite usqr; apply Zmult_lt_0_compat; auto).
assert (p^2 < (2 * q)^2) by (replace ((2*q)^2) with (4*q^2) by ring; omega).
assert (q < p < 2*q) by (split; apply sqrt_lt_rev; omega).
assert ((2 * q - p)^2 = 2* (p - q)^2) by ring [E].
apply Ip with (y := (2*q-p)) (q := p - q); unfold Zwf; omega.
Qed.

Lemma nsqrt : ~exists p, exists q, p <> 0 /\ p^2=2*q^2.
Proof.
intros [p [q [p0 E]]]; assert (q0 : q <> 0).
  intros q'; rewrite q', usqr, !Zmult_0_r in E.
  apply Zmult_integral_l in E; intuition.
assert (Zabs_lt : forall x, x <> 0 -> 0 < Zabs x).
  intros x x0; destruct x; compute; intuition.
apply (nsqrtp (Zabs p) (Zabs q)); [auto | auto | ].
revert E; rewrite !usqr, !Zabs_square; auto.
Qed.

Open Scope Q_scope.

Lemma sqrt2nQ : ~exists x:Q, x ^ 2 == 2#1.
Proof.
intros [[p q] xsq]; apply nsqrt; exists p; exists (Zpos q); split.
  intros p0; rewrite p0 in xsq; discriminate.
revert xsq; simpl Qpower; unfold  Qmult, Qeq; rewrite Zmult_1_r, !usqr; auto.
Qed.