feat(library/theories/number_theory/square_root_irrational): add proof that sqrt 2 is irrational

library/theories/number_theory/number_theory.md

@@ -3,4 +3,5 @@ theories.number_theory
 
 * [primes](primes.lean)
 * [bezout](bezout.lean) : Bezout's theorem
-* [prime_factorization](prime_factorization.lean) : prime divisors and multiplicity
+* [prime_factorization](prime_factorization.lean) : prime divisors and multiplicity
+* [square_root_irrational](square_root_irrational.lean) : quadratic surds

library/theories/number_theory/square_root_irrational.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+A proof that the square root of an integer is irrational, unless the integer is a perfect square.
+-/
+import data.rat
+open nat eq.ops
+
+/- First, a textbook proof that sqrt 2 is irrational. -/
+
+theorem sqrt_two_irrational_aux {a b : ℕ} (co : coprime a b) : a * a ≠ 2 * (b * b) :=
+assume H : a * a = 2 * (b * b),
+have even (a * a), from even_of_exists (exists.intro _ H),
+have even a, from even_of_even_mul_self this,
+obtain c (aeq : a = 2 * c), from exists_of_even this,
+have 2 * (2 * (c * c)) = 2 * (b * b), by rewrite [-H, aeq, mul.assoc, mul.left_comm c],
+have 2 * (c * c) = b * b, from eq_of_mul_eq_mul_left dec_trivial this,
+have even (b * b), from even_of_exists (exists.intro _ (eq.symm this)),
+have even b, from even_of_even_mul_self this,
+have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
+have 2 ∣ 1, from co ▸ this,
+absurd `2 ∣ 1` dec_trivial
+
+/- Let's state this in terms of rational numbers. The problem is that we now have to mediate between
+   rat, int, and nat. -/
+
+section
+  open rat int
+
+  theorem sqrt_two_irrational (q : ℚ): q^2 ≠ 2 :=
+  suppose q^2 = 2,
+  let a := num q, b := denom q in
+  have b ≠ 0, from ne_of_gt (denom_pos q),
+  assert bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H),
+  have b * b ≠ (0 : ℚ), from rat.mul_ne_zero bnz bnz,
+  have (a * a) / (b * b) = 2,
+    by rewrite [*of_int_mul, -div_mul_div bnz bnz, -eq_num_div_denom, -this, rat.pow_two],
+  have a * a = 2 * (b * b), from eq.symm (mul_eq_of_eq_div `b * b ≠ (0 : ℚ)` this⁻¹),
+  assert a * a = 2 * (b * b), from of_int.inj this,    -- now in the integers
+  let a' := nat_abs a, b' := nat_abs b in
+  have H : a' * a' = 2 * (b' * b'),
+    begin
+      apply of_nat.inj,
+      rewrite [-+nat_abs_mul, int.of_nat_mul, +of_nat_nat_abs, +int.abs_mul_self],
+      exact this,
+    end,
+  have coprime a b, from !coprime_num_denom,
+  have nat.coprime a' b', from of_nat.inj this,
+  show false, from sqrt_two_irrational_aux this H
+end