• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Number-theory
        • Euler
        • Euclid
        • Fermat
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

• Number-theory

Euclid

Definition of prime number and two theorems of Euclid

Overview

This book contains proofs of two theorems of Euclid:

1. There exist infinitely many primes.
2. If p is a prime divisor of a*b, then p divides either a or b.

Definitions and Theorems

We first list some basic properties of divisibility.

Function: divides

(defun divides (x y)
       (declare (xargs :guard t))
       (and (acl2-numberp x)
            (not (= x 0))
            (acl2-numberp y)
            (integerp (/ y x))))

Theorem: divides-leq

(defthm divides-leq
        (implies (and (> x 0) (> y 0) (divides x y))
                 (<= x y))
        :rule-classes nil)

Theorem: divides-minus

(defthm divides-minus
        (implies (divides x y)
                 (divides x (- y)))
        :rule-classes nil)

Theorem: divides-sum

(defthm divides-sum
        (implies (and (divides x y) (divides x z))
                 (divides x (+ y z)))
        :rule-classes nil)

Theorem: divides-product

(defthm divides-product
        (implies (and (integerp z) (divides x y))
                 (divides x (* y z)))
        :rule-classes nil)

Theorem: divides-transitive

(defthm divides-transitive
        (implies (and (divides x y) (divides y z))
                 (divides x z))
        :rule-classes nil)

Theorem: divides-self

(defthm divides-self
        (implies (and (acl2-numberp x) (not (= x 0)))
                 (divides x x)))

Theorem: divides-0

(defthm divides-0
        (implies (and (acl2-numberp x) (not (= x 0)))
                 (divides x 0)))

Theorem: divides-mod-equal

(defthm divides-mod-equal
        (implies (and (real/rationalp a)
                      (real/rationalp b)
                      (real/rationalp n)
                      (not (= n 0)))
                 (iff (divides n (- a b))
                      (= (mod a n) (mod b n))))
        :rule-classes nil)

Theorem: divides-mod-0

(defthm divides-mod-0
        (implies (and (acl2-numberp a)
                      (acl2-numberp n)
                      (not (= n 0)))
                 (iff (divides n a) (= (mod a n) 0)))
        :rule-classes nil)

Our definition of primality is based on the following function, which computes the least divisor of a natural number n that is greater than or equal to k. (In the book mersenne, in which we are concerned with efficiency, we shall introduce an equivalent version that checks for divisors only up to sqrt(n).)

Function: least-divisor

(defun least-divisor (k n)
       (declare (xargs :guard t))
       (if (and (integerp n)
                (integerp k)
                (< 1 k)
                (<= k n))
           (if (divides k n)
               k (least-divisor (1+ k) n))
           nil))

Theorem: least-divisor-divides

(defthm least-divisor-divides
        (implies (and (integerp n)
                      (integerp k)
                      (< 1 k)
                      (<= k n))
                 (and (integerp (least-divisor k n))
                      (divides (least-divisor k n) n)
                      (<= k (least-divisor k n))
                      (<= (least-divisor k n) n)))
        :rule-classes nil)

Theorem: least-divisor-is-least

(defthm least-divisor-is-least
        (implies (and (integerp n)
                      (integerp k)
                      (< 1 k)
                      (<= k n)
                      (integerp d)
                      (divides d n)
                      (<= k d))
                 (<= (least-divisor k n) d))
        :rule-classes nil)

Function: primep

(defun primep (n)
       (declare (xargs :guard t))
       (and (integerp n)
            (>= n 2)
            (equal (least-divisor 2 n) n)))

Theorem: primep-gt-1

(defthm primep-gt-1
        (implies (primep p)
                 (and (integerp p) (>= p 2)))
        :rule-classes :forward-chaining)

Theorem: primep-no-divisor

(defthm primep-no-divisor
        (implies (and (primep p)
                      (integerp d)
                      (divides d p)
                      (> d 1))
                 (= d p))
        :rule-classes nil)

Theorem: primep-least-divisor

(defthm primep-least-divisor
        (implies (and (integerp n) (>= n 2))
                 (primep (least-divisor 2 n)))
        :rule-classes nil)

Our formulation of the infinitude of the set of primes is based on a function that returns a prime that is greater than its argument:

Function: fact

(defun fact (n)
       (declare (xargs :guard (natp n)))
       (if (zp n) 1 (* n (fact (1- n)))))

Function: greater-prime

(defun greater-prime (n)
       (declare (xargs :guard (natp n)))
       (least-divisor 2 (1+ (fact n))))

Theorem: greater-prime-divides

(defthm greater-prime-divides
        (divides (greater-prime n)
                 (1+ (fact n)))
        :rule-classes nil)

Theorem: divides-fact

(defthm divides-fact
        (implies (and (integerp n)
                      (integerp k)
                      (<= 1 k)
                      (<= k n))
                 (divides k (fact n))))

Theorem: not-divides-fact-plus1

(defthm not-divides-fact-plus1
        (implies (and (integerp n)
                      (integerp k)
                      (< 1 k)
                      (<= k n))
                 (not (divides k (1+ (fact n)))))
        :rule-classes nil)

Theorem: infinitude-of-primes

(defthm infinitude-of-primes
        (implies (integerp n)
                 (and (primep (greater-prime n))
                      (> (greater-prime n) n)))
        :rule-classes nil)

Our main theorem of Euclid depends on the properties of the greatest common divisor, which we define according to Euclid's algorithm.

Function: g-c-d-nat

(defun g-c-d-nat (x y)
       (declare (xargs :guard (and (natp x) (natp y))))
       (if (zp x)
           y
           (if (zp y)
               x
               (if (<= x y)
                   (g-c-d-nat x (- y x))
                   (g-c-d-nat (- x y) y)))))

Function: g-c-d

(defun g-c-d (x y)
       (declare (xargs :guard (and (integerp x) (integerp y))))
       (g-c-d-nat (abs x) (abs y)))

Theorem: g-c-d-nat-pos

(defthm g-c-d-nat-pos
        (implies (and (natp x)
                      (natp y)
                      (not (and (= x 0) (= y 0))))
                 (> (g-c-d-nat x y) 0))
        :rule-classes nil)

Theorem: g-c-d-pos

(defthm g-c-d-pos
        (implies (and (integerp x)
                      (integerp y)
                      (not (and (= x 0) (= y 0))))
                 (and (integerp (g-c-d x y))
                      (> (g-c-d x y) 0)))
        :rule-classes nil)

Theorem: divides-g-c-d-nat

(defthm divides-g-c-d-nat
        (implies (and (natp x) (natp y))
                 (and (or (= x 0) (divides (g-c-d-nat x y) x))
                      (or (= y 0)
                          (divides (g-c-d-nat x y) y))))
        :rule-classes nil)

Theorem: g-c-d-divides

(defthm g-c-d-divides
        (implies (and (integerp x) (integerp y))
                 (and (or (= x 0) (divides (g-c-d x y) x))
                      (or (= y 0) (divides (g-c-d x y) y))))
        :rule-classes nil)

It remains to be shown that the gcd of x and y is divisible by any common divisor of x and y. This depends on the observation that the gcd may be expressed as a linear combination

r*x + s*y

. We construct the coefficients r and s explicitly.

Function: r-nat

(defun r-nat (x y)
       (declare (xargs :guard (and (natp x) (natp y))))
       (if (zp x)
           0
           (if (zp y)
               1
               (if (<= x y)
                   (- (r-nat x (- y x)) (s-nat x (- y x)))
                   (r-nat (- x y) y)))))

Function: s-nat

(defun s-nat (x y)
       (declare (xargs :guard (and (natp x) (natp y))))
       (if (zp x)
           1
           (if (zp y)
               0
               (if (<= x y)
                   (s-nat x (- y x))
                   (- (s-nat (- x y) y)
                      (r-nat (- x y) y))))))

Theorem: r-s-nat

(defthm r-s-nat
        (implies (and (natp x) (natp y))
                 (= (+ (* (r-nat x y) x) (* (s-nat x y) y))
                    (g-c-d-nat x y)))
        :rule-classes nil)

Function: r-int

(defun r-int (x y)
       (declare (xargs :guard (and (integerp x) (integerp y))))
       (if (< x 0)
           (- (r-nat (abs x) (abs y)))
           (r-nat (abs x) (abs y))))

Function: s-int

(defun s-int (x y)
       (declare (xargs :guard (and (integerp x) (integerp y))))
       (if (< y 0)
           (- (s-nat (abs x) (abs y)))
           (s-nat (abs x) (abs y))))

Theorem: g-c-d-linear-combination

(defthm g-c-d-linear-combination
        (implies (and (integerp x) (integerp y))
                 (= (+ (* (r-int x y) x) (* (s-int x y) y))
                    (g-c-d x y)))
        :rule-classes nil)

Theorem: divides-g-c-d

(defthm divides-g-c-d
        (implies (and (integerp x)
                      (integerp y)
                      (integerp d)
                      (not (= d 0))
                      (divides d x)
                      (divides d y))
                 (divides d (g-c-d x y))))

Theorem: g-c-d-prime

(defthm g-c-d-prime
        (implies (and (primep p)
                      (integerp a)
                      (not (divides p a)))
                 (= (g-c-d p a) 1))
        :rule-classes nil)

The main theorem:

Theorem: euclid

(defthm euclid
        (implies (and (primep p)
                      (integerp a)
                      (integerp b)
                      (not (divides p a))
                      (not (divides p b)))
                 (not (divides p (* a b))))
        :rule-classes nil)