Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational

Prove that square-root of 2 is irrational.

Documentation

sqrt2IsIrrational :: IO Proof

Prove that square-root of 2 is irrational. That is, we can never find a and b such that sqrt 2 == a / b and a and b are co-prime.

In order not to deal with reals and square-roots, we prove the integer-only alternative: If a^2 = 2b^2, then a and b cannot be co-prime. We proceed by establishing the following helpers first:

1. An odd number squared is odd: odd x -> odd x^2
2. An even number that is a perfect square must be the square of an even number: even x^2 -> even x.
3. If a number is even, then its square must be a multiple of 4: even x .=> x*x % 4 == 0.

Using these helpers, we can argue:

4. Start with the premise a^2 = 2b^2.
5. Thus, a^2 must be even. (Since it equals 2b^2 by a.)
6. Thus, a must be even. (Using 2 and b.)
7. Thus, a^2 must be divisible by 4. (Using 3 and c. That is, 2b^2 == 4*K for someK.)
8. Thus, b^2 must be even. (Using d, b^2 = 2K.)
9. Thus, b must be even. (Using 2 and e.)
10. Since a and b are both even, they cannot be co-prime. (Using c and f.)

Note that our proof is mostly about the first 3 facts above, then z3 and KnuckleDragger fills in the rest.

We have:

>>> sqrt2IsIrrational
Chain: oddSquaredIsOdd
  Lemma: oddSquaredIsOdd.1              Q.E.D.
  Lemma: oddSquaredIsOdd.2              Q.E.D.
Lemma: oddSquaredIsOdd                  Q.E.D.
Lemma: squareEvenImpliesEven            Q.E.D.
Chain: evenSquaredIsMult4
  Lemma: evenSquaredIsMult4.1           Q.E.D.
Lemma: evenSquaredIsMult4               Q.E.D.
Lemma: sqrt2IsIrrational                Q.E.D.
[Proven] sqrt2IsIrrational