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

• Number-theory

Euler

This book contains a proof of Euler's Criterion for quadratic residues

This book contains a proof of Euler's Criterion for quadratic residues: If p is an odd prime and m is not divisible by p, then

mod(m^((p-1)/2),p) = 1 if m is a quadratic residue mod p
                     p-1 if not.

Along the way, we also prove Wilson's Theorem: If p is prime, then mod((p-1)!,p) = p-1. Finally, as a consequence of Euler's Criterion, we derive the First Supplement to the Law of Quadratic Reciprocity: -1 is a quadratic residue mod p iff mod(p,4) = 1. The proof depends on Fermat's Theorem:

Definitions and Theorems

Let p be a prime, let m be relatively prime to p, and let 0 < j < p. Then there exists a unique j' such that 0 < j' < p and

mod(j*j',p) = mod(m,p), 

called the associate of j w.r.t. a mod p.

Function: associate

(defun associate (j m p)
  (mod (* m (expt j (- p 2))) p))

Theorem: associate-property

(defthm associate-property
  (implies (and (primep p)
                (integerp m)
                (not (zp j))
                (< j p)
                (not (divides p m)))
           (equal (mod (* (associate j m p) j) p)
                  (mod m p)))
  :rule-classes nil)

Theorem: associate-bnds

(defthm associate-bnds
  (implies (and (primep p)
                (integerp m)
                (not (zp j))
                (< j p)
                (not (divides p m)))
           (and (not (zp (associate j m p)))
                (< (associate j m p) p)))
  :rule-classes (:forward-chaining))

Theorem: associate-is-unique

(defthm associate-is-unique
  (implies (and (primep p)
                (integerp m)
                (not (zp j))
                (< j p)
                (not (divides p m))
                (integerp x)
                (equal (mod m p) (mod (* j x) p)))
           (equal (associate j m p) (mod x p)))
  :rule-classes nil)

Theorem: associate-of-associate

(defthm associate-of-associate
  (implies (and (primep p)
                (integerp m)
                (not (zp j))
                (< j p)
                (not (divides p m)))
           (equal (associate (associate j m p) m p)
                  (mod j p))))

Theorem: associate-equal

(defthm associate-equal
  (implies (and (primep p)
                (integerp m)
                (integerp j)
                (not (divides p m))
                (not (zp j))
                (< j p)
                (not (zp i))
                (< i p))
           (equal (equal (associate j m p)
                         (associate i m p))
                  (equal i j))))

Theorem: associate-square

(defthm associate-square
  (implies (and (primep p)
                (integerp m)
                (not (divides p m))
                (not (zp j))
                (< j p))
           (iff (= (associate j m p) j)
                (= (mod (* j j) p) (mod m p))))
  :rule-classes nil)

If there exists x such that mod(x*x,p) = mod(m,p), then m is said to be a (quadratic) residue mod p.If m is a residue mod p, then there are exactly 2 roots of mod(x*x,p) = mod(m,p) in the range 0 < x < p.

Function: root1

(defun root1 (m p)
  (find-root (1- p) m p))

Theorem: res-root1

(defthm res-root1
  (implies (and (primep p) (residue m p))
           (and (not (zp (root1 m p)))
                (< (root1 m p) p)
                (equal (mod (* (root1 m p) (root1 m p)) p)
                       (mod m p))))
  :rule-classes nil)

Function: root2

(defun root2 (m p) (- p (root1 m p)))

Theorem: res-root2

(defthm res-root2
  (implies (and (primep p) (residue m p))
           (and (not (zp (root2 m p)))
                (< (root2 m p) p)
                (equal (mod (* (root2 m p) (root2 m p)) p)
                       (mod m p))))
  :rule-classes nil)

Theorem: associate-roots

(defthm associate-roots
  (implies (and (primep p)
                (integerp m)
                (not (divides p m))
                (residue m p))
           (and (equal (associate (root1 m p) m p)
                       (root1 m p))
                (equal (associate (root2 m p) m p)
                       (root2 m p))))
  :rule-classes nil)

Theorem: only-2-roots

(defthm only-2-roots
  (implies (and (primep p)
                (integerp m)
                (not (divides p m))
                (residue m p)
                (not (zp j))
                (< j p)
                (= (associate j m p) j))
           (or (= j (root1 m p))
               (= j (root2 m p))))
  :rule-classes nil)

Theorem: roots-distinct

(defthm roots-distinct
  (implies (and (primep p)
                (not (= p 2))
                (residue m p))
           (not (= (root1 m p) (root2 m p))))
  :rule-classes nil)

For 0 <= n < p, we construct a list associates(n,m,p) of distinct integers between 1 and p-1 with the following properties:

• If 1 <= j <= n, then j is in associates(n,m,p).
• If j is in associates(n,m,p), then so is associate(j,m,p).

Function: associates

(defun associates (n m p)
  (if (zp n)
      (if (residue m p)
          (cons (root2 m p)
                (cons (root1 m p) nil))
        nil)
    (if (member n (associates (1- n) m p))
        (associates (1- n) m p)
      (cons (associate n m p)
            (cons n (associates (1- n) m p))))))

Theorem: member-associates

(defthm member-associates
  (implies (and (primep p)
                (integerp m)
                (not (divides p m))
                (integerp n)
                (< n p)
                (not (zp j))
                (< j p))
           (iff (member (associate j m p)
                        (associates n m p))
                (member j (associates n m p)))))

We shall show that associates(p-1,m,p) is a permutation of positives(p-1).

Theorem: subset-positives-associates

(defthm subset-positives-associates
  (subsetp (positives n)
           (associates n m p)))

Theorem: member-self-associate

(defthm member-self-associate
  (implies (and (primep p)
                (integerp m)
                (not (divides p m))
                (not (zp j))
                (< j p)
                (equal (associate j m p) j))
           (member j (associates n m p))))

Theorem: distinct-positives-associates-lemma

(defthm distinct-positives-associates-lemma
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m))
                (integerp n)
                (< n p))
           (distinct-positives (associates n m p)
                               (1- p)))
  :rule-classes nil)

Theorem: distinct-positives-associates

(defthm distinct-positives-associates
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (distinct-positives (associates (1- p) m p)
                               (1- p)))
  :rule-classes nil)

We shall require a variation of the pigeonhole principle.

Theorem: pigeonhole-principle-2

(defthm pigeonhole-principle-2
  (implies (and (natp n)
                (distinct-positives l n)
                (subsetp (positives n) l))
           (perm (positives n) l))
  :rule-classes nil)

Theorem: perm-associates-positives

(defthm perm-associates-positives
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (perm (positives (1- p))
                 (associates (1- p) m p)))
  :rule-classes nil)

It follows that the product of associates(p-1,m,p) is (p-1)! and its length is p-1.

Theorem: times-list-associates-fact

(defthm times-list-associates-fact
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (equal (times-list (associates (1- p) m p))
                  (fact (1- p))))
  :rule-classes nil)

Theorem: perm-len

(defthm perm-len
  (implies (perm l1 l2)
           (= (len l1) (len l2)))
  :rule-classes nil)

Theorem: len-positives

(defthm len-positives
  (equal (len (positives n)) (nfix n)))

Theorem: len-associates

(defthm len-associates
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (equal (len (associates (+ -1 p) m p))
                  (1- p))))

Theorem: len-associates-even

(defthm len-associates-even
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m))
                (integerp n)
                (< n p))
           (integerp (* 1/2 (len (associates n m p)))))
  :rule-classes (:type-prescription))

On the other hand, we can compute the product of associates(p-1,a,p) as follows.

Theorem: times-list-associates

(defthm times-list-associates
  (implies
       (and (primep p)
            (not (= p 2))
            (integerp m)
            (not (divides p m))
            (< n p))
       (equal (mod (times-list (associates n m p)) p)
              (if (residue m p)
                  (mod (- (expt m (/ (len (associates n m p)) 2)))
                       p)
                (mod (expt m (/ (len (associates n m p)) 2))
                     p))))
  :rule-classes nil)

Both Wilson's Theorem and Euler's Criterion now follow easily.

Theorem: euler-lemma

(defthm euler-lemma
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (equal (mod (fact (1- p)) p)
                  (if (residue m p)
                      (mod (- (expt m (/ (1- p) 2))) p)
                    (mod (expt m (/ (1- p) 2)) p))))
  :rule-classes nil)

Theorem: wilson

(defthm wilson
  (implies (primep p)
           (equal (mod (fact (1- p)) p) (1- p)))
  :rule-classes nil)

Theorem: euler-criterion

(defthm euler-criterion
  (implies (and (primep p)
                (not (= p 2))
                (integerp m)
                (not (divides p m)))
           (equal (mod (expt m (/ (1- p) 2)) p)
                  (if (residue m p) 1 (1- p))))
  :rule-classes nil)

The First Supplement is the case a = 1

Theorem: first-supplement

(defthm first-supplement
  (implies (and (primep p) (not (= p 2)))
           (iff (residue -1 p) (= (mod p 4) 1)))
  :rule-classes nil)