Documentation

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 (4).)
6. Thus, a must be even. (Using (2) and (5).)
7. Thus, a^2 must be divisible by 4. (Using (3) and (6). That is, 2b^2 == 4K for some K.)
8. Thus, b^2 must be even. (Using (7), and b^2 = 2K.)
9. Thus, b must be even. (Using (2) and (8).)
10. Since a and b are both even, they cannot be co-prime. (Using (6) and (9).)

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

We have:

>>> sqrt2IsIrrational
Lemma: oddSquaredIsOdd
  Step: 1                               Q.E.D.
  Step: 2 (expand square)               Q.E.D.
  Result:                               Q.E.D.
Lemma: squareEvenImpliesEven            Q.E.D.
Lemma: evenSquaredIsMult4
  Step: 1                               Q.E.D.
  Step: 2 (expand square)               Q.E.D.
  Result:                               Q.E.D.
Lemma: sqrt2IsIrrational                Q.E.D.
[Proven] sqrt2IsIrrational :: Bool