From f691c12b5bf83e8149415b014f1de82efced75bc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 16 Apr 2004 09:39:48 +0000 Subject: New file --- acl2/root2.acl2 | 347 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 347 insertions(+) create mode 100644 acl2/root2.acl2 diff --git a/acl2/root2.acl2 b/acl2/root2.acl2 new file mode 100644 index 00000000..f93d688b --- /dev/null +++ b/acl2/root2.acl2 @@ -0,0 +1,347 @@ +(* Example proof by Ruben Gamboa. See http://www.cs.kun.nl/~freek/comparison/ *) + + +(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. + -- cgit v1.2.3