(* 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.