(in-package "ACL2") ;; This book presents the proof that sqrt(2) is an irrational number. ;; The proof proceeds by observing that p^2 is even precisely when p ;; is even. Thus, if p^2 = 2 q^2, p must be even. But then, p^2 ;; isn't just even, it's a multiple of 4, so q^2 = p^2 / 2 must also ;; be even. But since q^2 is even, so is q. Now, letting p be the ;; numerator of 2 and q the denominator of 2, we find that both the ;; numerator and denominator are even -- but this is an ;; impossibility. Hence, we can conclude that 2 is not rational. ;; The proof is completed by observing that sqrt(2) is not complex. ;; The reason is that if x is complex, x^2 is real only when x is a ;; pure imaginary number. But in those cases, x^2 is negative (include-book "../arithmetic/top" :load-compiled-file nil) ;; Step 1: We begin by proving that p^2 is even precisely when p is ;; even. (encapsulate () ;; Since ACL2 is so strong in induction, it is common to use ;; induction to prove simple number theoretic results. But to induce ;; over the even numbers requires that each time through the ;; induction we "step" by 2, not the usual 1. So we start by ;; introducing the induction scheme for the even numbers. (local (defun even-induction (x) "Induct by going two steps at a time" (if (or (zp x) (equal x 1)) x (1+ (even-induction (1- (1- x))))))) ;; Now we can prove that if p^2 is even, so is p. Because we're ;; doing this inductively, we only consider the even naturals to ;; begin with. (local (defthm lemma-1 (implies (and (integerp p) (<= 0 p) (evenp (* p p))) (evenp p)) :hints (("Goal" :induct (even-induction p))) :rule-classes nil)) ;; Technically, we do not need to worry about the negative integers ;; in this proof, since both the numerator and denominator of 2 (if ;; they existed) are positive. But it's easy enough to prove this, ;; and it gets rid of the "non-negative" hypothesis. In general, it ;; is good to get rid of hypothesis in ACL2 rewrite rules. (local (defthm lemma-2 (implies (and (integerp p) (<= p 0) (evenp (* p p))) (evenp p)) :hints (("Goal" :use (:instance lemma-1 (p (- p))))) :rule-classes nil)) ;; Now, we can prove that if p^2 is even, so is p. But the converse ;; is trivial, so we could show that p^2 is even iff p is even. ;; Because equalities are more powerful rewrite rules than ;; implications, we prefer to do so, even though we don't really need ;; the stronger equality for this proof. So we prove the converse ;; here: if p is even, so is p^2. (local (defthm lemma-3 (implies (and (integerp p) (evenp p)) (evenp (* p p))) :rule-classes nil)) ;; Now, we simply collect the results above to find that p^2 is even ;; if and only if p is even. This is the only theorem that is ;; exported from this event. (defthm even-square-implies-even (implies (integerp p) (equal (evenp (* p p)) (evenp p))) :hints (("Goal" :use ((:instance lemma-1) (:instance lemma-2) (:instance lemma-3))))) ) ;; Step 2. Suppose p^2 is even. Then, p is even, so p^2 is more than ;; even -- it is a multiple of 4. We prove this here, since it is the ;; key fact allowing us to conclude that q^2 is even when we know that ;; p^2 = 2 * q^2. (defthm even-square-implies-even-square-multiple-of-4 (implies (and (integerp p) (evenp (* p p))) (evenp (* 1/2 p p))) :hints (("Goal" :use ((:instance even-square-implies-even) (:instance (:theorem (implies (integerp x) (integerp (* x x)))) (x (* 1/2 p)))) :in-theory (disable even-square-implies-even)))) ;; In the proofs below, we disable ACL2's definition of even, but we ;; need to remember that 2*n is always even. So we prove that rewrite ;; rule here. (defthm evenp-2x (implies (integerp x) (evenp (* 2 x)))) ;; Step 3. Suppose p^2 = 2 * q^2. Then we can conclude that p is ;; even, since p^2 is even. (defthm numerator-sqrt-2-is-even (implies (and (integerp p) (integerp q) (equal (* p p) (* 2 (* q q)))) (evenp p)) :hints (("Goal" :use ((:instance even-square-implies-even) (:instance evenp-2x (x (* q q)))) :in-theory (disable even-square-implies-even evenp-2x evenp)))) ;; Step 4. Suppose p^2 = 2 * q^2. Then we can conclude that q is ;; even, since p^2 is a multiple of 4, so q^2 is even. (defthm denominator-sqrt-2-is-even (implies (and (integerp p) (integerp q) (equal (* p p) (* 2 (* q q)))) (evenp q)) :hints (("Goal" :use ((:instance even-square-implies-even-square-multiple-of-4) (:instance even-square-implies-even (p q)) (:instance evenp-2x (x (* q q))) (:instance equal-*-/-1 (x 2) (y (* p p)) (z (* q q)))) :in-theory (disable even-square-implies-even-square-multiple-of-4 even-square-implies-even evenp-2x evenp equal-*-/-1)))) ;; Step 5. Those are all the pieces we need to prove that sqrt(2) is ;; not rational. For we observe that if p=numerator(sqrt(2)) and ;; q=denominator(sqrt(2)), the theorems above show that both p and q ;; are even, and that's an absurdity. (encapsulate () ;; ACL2's algebraic prowess is modest. In the proof of the main ;; theorem below, it builds the expression p^2/q^2 where x=p/q, but ;; it does not reduce the expression further to x^2. We add a ;; rewrite rule to take care of that. (local (defthm lemma-1 (implies (rationalp x) (equal (* (/ (denominator x)) (/ (denominator x)) (numerator x) (numerator x)) (* x x))) :hints (("Goal" :use ((:instance Rational-implies2) (:instance *-r-denominator-r (r x))) :in-theory (disable Rational-implies2 *-r-denominator-r))))) ;; Now we can prove that the square root of 2 is not rational. This ;; involves using the theorems defined above, as well as some ;; algebraic lemmas to help reduce the terms. The most important ;; hint, however, is the inclusion of the axiom Lowest-Terms, because ;; it is not enabled in the ACL2 world. (defthm sqrt-2-not-rational (implies (equal (* x x) 2) (not (rationalp x))) :hints (("Goal" :use ((:instance numerator-sqrt-2-is-even (p (numerator x)) (q (denominator x))) (:instance denominator-sqrt-2-is-even (p (numerator x)) (q (denominator x))) (:instance Lowest-Terms (n 2) (r (/ (numerator x) 2)) (q (/ (denominator x) 2))) (:instance equal-*-/-1 (x (/ (* (denominator x) (denominator x)))) (y 2) (z (* (numerator x) (numerator x))))) :in-theory (disable equal-*-/-1 numerator-sqrt-2-is-even denominator-sqrt-2-is-even)))) ) ;; Step 6. Now that the rationals are ruled out, we need to weed out ;; the remaining sqrt(2) suspects. One possibility is that sqrt(2) is ;; a complex number. We explore that here. Because ACL2 has very ;; little knowledge of the complex numbers, we have to start with some ;; basic facts. First, we show that (a+bi)^2 = (a^2-b^2)+(ab+ab)i. (encapsulate () ;; We start out with the desired theorem when the complex number is ;; written as a+bi instead of (complex a b). Here, the result ;; follows from simple algebra and the fact that i^2=-1. (local (defthm lemma-1 (equal (* (+ x (* #c(0 1) y)) (+ x (* #c(0 1) y))) (+ (- (* x x) (* y y)) (* #c(0 1) (+ (* x y) (* x y))))) :rule-classes nil)) ;; Now we rewrite the right-hand side of the rewrite rule into the ;; final form of (complex (a^2-b^2) (ab+ab)) (local (defthm lemma-2 (implies (and (realp x) (realp y)) (equal (* (+ x (* #c(0 1) y)) (+ x (* #c(0 1) y))) (complex (- (* x x) (* y y)) (+ (* x y) (* x y))))) :hints (("Goal" :use ((:instance lemma-1) (:instance complex-definition (x (- (* x x) (* y y))) (y (+ (* x y) (* x y))))))) :rule-classes nil)) ;; And finally we rewrite the left-hand side of the rewrite rule into ;; the final form of (complex a b)^2. (defthm complex-square-definition (implies (and (realp x) (realp y)) (equal (* (complex x y) (complex x y)) (complex (- (* x x) (* y y)) (+ (* x y) (* x y))))) :hints (("Goal" :use ((:instance complex-definition) (:instance lemma-2)))) :rule-classes nil) ) ;; Step 7. Since (a+bi)^2 = (a^2-b^2)+(ab+ab)i, it follows that it is ;; real if and only if a or b is zero, i.e., if and only if the number ;; is real or pure imaginary. Since we're interested only in the ;; non-real complex numbers (the ones for which complexp is true), we ;; can conlude that only pure imaginaries have real squares. (encapsulate () ;; First we show that (a+bi)^2 = (a^2-b^2)+(ab+ab)i is real if and ;; only ab+ab is zero. (local (defthm lemma-1 (implies (and (complexp x) (realp (* x x))) (equal (+ (* (realpart x) (imagpart x)) (* (realpart x) (imagpart x))) 0)) :hints (("Goal" :use (:instance complex-square-definition (x (realpart x)) (y (imagpart x))))) :rule-classes nil)) ;; The following rewrite rule allows us to conclude that a real ;; number x is zero whenever x+x is zero. (local (defthm lemma-2 (implies (and (realp x) (equal (+ x x) 0)) (= x 0)))) ;; The two lemmas above conclude that ab is zero whenever (a+bi)^2 is ;; zero, and since b is assumed non-zero (because a+bi is complex), ;; we have that a must be zero, and a+bi=bi is a pure imaginary ;; number. (defthm complex-squares-real-iff-imaginary (implies (and (complexp x) (realp (* x x))) (equal (realpart x) 0)) :hints (("Goal" :use ((:instance lemma-1) (:instance lemma-2 (x (* (realpart x) (imagpart x)))))))) ) ;; Step 7. Trivially, the square of a pure imaginary number bi is a ;; negative real, since bi^2 = -b^2. (defthm imaginary-squares-are-negative (implies (and (complexp x) (equal (realpart x) 0)) (< (* x x) 0)) :hints (("Goal" :use (:instance complex-square-definition (x 0) (y (imagpart x)))))) ;; Step 8. From the theorems above, we can conclude that sqrt(2) is ;; not a complex number, because the only candidates are the pure ;; imaginary numbers, and their squares are all negative. (defthm sqrt-2-not-complexp (implies (complexp x) (not (equal (* x x) 2))) :hints (("Goal" :use ((:instance complex-squares-real-iff-imaginary) (:instance imaginary-squares-are-negative))))) ;; Step 9. That means sqrt(2) is not rational, and neither is it a ;; complex number. The only remaining candidates (in ACL2's universe) ;; are the non-rational reals, so we can prove the main result: the ;; square root of two (if it exists) is irrational. (defthm irrational-sqrt-2 (implies (equal (* x x) 2) (and (realp x) (not (rationalp x)))) :hints (("Goal" :cases ((rationalp x) (complexp x))))) ;; Step 10. Next, it would be nice to show that sqrt(2) actually ;; exists! See the book nonstd/nsa/sqrt.lisp for a proof of that, ;; using non-standard analysis.