grcd - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "int-division")

include-book

(include-book "ordinals/e0-ordinal" :dir :system)

other

(set-well-founded-relation e0-ord-<)

npmacro

(defmacro np
  (x)
  (list 'and (list 'integerp x) (list '<= 0 x)))

pintpmacro

(defmacro pintp
  (x)
  (list 'and (list 'integerp x) (list '< 0 x)))

euclid-alg-natfunction

(defun euclid-alg-nat
  (a b)
  (declare (xargs :measure (if (and (np a) (np b))
        (cons (+ a 1) (+ b 1))
        0)))
  (if (and (np a) (np b))
    (cond ((equal a b) (mv a 1 0 1 1))
      ((equal b 0) (mv a 1 0 1 0))
      ((equal a 0) (mv b 0 1 0 1))
      ((< b a) (mv-let (g x y u v) (euclid-alg-nat b a) (mv g y x v u)))
      (t (mv-let (g x y u v)
          (euclid-alg-nat a (- b a))
          (mv g (- x y) y u (+ u v)))))
    (mv 0 0 0 0 0)))

euclid-algfunction

(defun euclid-alg
  (a b)
  (if (and (integerp a) (integerp b))
    (cond ((and (<= 0 a) (<= 0 b)) (euclid-alg-nat a b))
      ((and (> 0 a) (<= 0 b)) (mv-let (g x y u v)
          (euclid-alg-nat (- a) b)
          (mv g (- x) y (- u) v)))
      ((and (<= 0 a) (> 0 b)) (mv-let (g x y u v)
          (euclid-alg-nat a (- b))
          (mv g x (- y) u (- v))))
      (t (mv-let (g x y u v)
          (euclid-alg-nat (- a) (- b))
          (mv g (- x) (- y) (- u) (- v)))))
    (mv 0 0 0 0 0)))

local

(local (defthm euclid-alg-nat-gives-gcd
    (implies (and (np a) (np b))
      (mv-let (g x y u v)
        (euclid-alg-nat a b)
        (and (equal (* g u) a)
          (equal (* g v) b)
          (equal (+ (* x a) (* y b)) g))))))

local

(local (in-theory (disable mv-nth)))

local

(local (defthm euclid-alg-nat-commutes-with-*
    (implies (and (np a) (np b) (pintp c))
      (equal (euclid-alg-nat (* a c) (* b c))
        (mv-let (g x y u v)
          (euclid-alg-nat a b)
          (mv (* g c) x y u v))))))

local

(local (defthm euclid-alg-nat-type
    (implies (and (np a) (np b))
      (mv-let (g x y u v)
        (euclid-alg-nat a b)
        (and (np g) (integerp x) (integerp y) (np u) (np v))))
    :rule-classes ((:type-prescription :corollary (np (mv-nth 0 (euclid-alg-nat a b)))) (:type-prescription :corollary (integerp (mv-nth 1 (euclid-alg-nat a b))))
      (:type-prescription :corollary (integerp (mv-nth 2 (euclid-alg-nat a b))))
      (:type-prescription :corollary (np (mv-nth 3 (euclid-alg-nat a b))))
      (:type-prescription :corollary (np (mv-nth 4 (euclid-alg-nat a b)))))))

local

(local (defthm euclid-alg-nat-0-0
    (implies (and (np a) (np b) (or (< 0 a) (< 0 b)))
      (and (integerp (mv-nth 0 (euclid-alg-nat a b)))
        (< 0 (mv-nth 0 (euclid-alg-nat a b)))))
    :rule-classes :type-prescription))

local

(local (defun ind-int
    (n)
    (if (integerp n)
      (if (< 0 n)
        (ind-int (+ -1 n))
        t)
      t)))

local

(local (defthm euclid-alg-nat-spec-1-a
    (implies (np a) (equal (euclid-alg-nat 1 a) (mv 1 1 0 1 a)))
    :hints (("Goal" :induct (ind-int a)) ("Subgoal *1/2''" :expand (euclid-alg-nat a 1)))))

local

(local (defthm euclid-alg-nat-is-commutative
    (implies (and (np a) (np b) (or (< a b) (< b a)))
      (equal (euclid-alg-nat a b)
        (mv-let (g x y u v) (euclid-alg-nat b a) (mv g y x v u))))
    :rule-classes ((:rewrite :loop-stopper ((a b))))))

grcdfunction

(defun grcd
  (a b)
  (mv-let (g x y u v)
    (euclid-alg a b)
    (declare (ignore x y u v))
    g))

grcd-lin-1function

(defun grcd-lin-1
  (a b)
  (mv-let (g x y u v)
    (euclid-alg a b)
    (declare (ignore g y u v))
    x))

grcd-lin-2function

(defun grcd-lin-2
  (a b)
  (mv-let (g x y u v)
    (euclid-alg a b)
    (declare (ignore g x u v))
    y))

grcd-quotient-1function

(defun grcd-quotient-1
  (a b)
  (mv-let (g x y u v)
    (euclid-alg a b)
    (declare (ignore g x y v))
    u))

grcd-quotient-2function

(defun grcd-quotient-2
  (a b)
  (mv-let (g x y u v)
    (euclid-alg a b)
    (declare (ignore g x y u))
    v))

grcd-type-inttheorem

(defthm grcd-type-int
  (np (grcd a b))
  :rule-classes :type-prescription)

grcd-positivetheorem

(defthm grcd-positive
  (implies (and (integerp a)
      (integerp b)
      (case-split (not (and (equal 0 a) (equal 0 b)))))
    (pintp (grcd a b)))
  :rule-classes :type-prescription)

grcd-lin-1-typetheorem

(defthm grcd-lin-1-type
  (integerp (grcd-lin-1 a b))
  :rule-classes :type-prescription)

grcd-lin-2-typetheorem

(defthm grcd-lin-2-type
  (integerp (grcd-lin-2 a b))
  :rule-classes :type-prescription)

grcd-quotient-1-typetheorem

(defthm grcd-quotient-1-type
  (integerp (grcd-quotient-1 a b))
  :rule-classes :type-prescription)

grcd-quotient-2-typetheorem

(defthm grcd-quotient-2-type
  (integerp (grcd-quotient-2 a b))
  :rule-classes :type-prescription)

grcd-spec-a-0theorem

(defthm grcd-spec-a-0 (equal (grcd a 0) (abs (ifix a))))

grcd-spec-a-atheorem

(defthm grcd-spec-a-a (equal (grcd a a) (abs (ifix a))))

grcd-spec-a-1theorem

(defthm grcd-spec-a-1
  (equal (grcd 1 a)
    (if (integerp a)
      1
      0)))

in-theory

(in-theory (disable euclid-alg-nat))

grcd-commutativitytheorem

(defthm grcd-commutativity
  (implies (and (integerp a) (integerp b))
    (equal (grcd a b) (grcd b a)))
  :hints (("Goal" :cases ((and (<= a 0) (<= b 0) (< (- a) (- b))) (and (<= a 0) (<= b 0) (< (- b) (- a)))
       (and (<= a 0) (<= 0 b) (< (- a) b))
       (and (<= a 0) (<= 0 b) (< b (- a)))
       (and (<= 0 a) (<= b 0) (< a (- b)))
       (and (<= 0 a) (<= b 0) (< (- b) a))
       (and (<= 0 a) (<= 0 b) (< a b))
       (and (<= 0 a) (<= 0 b) (< b a))))))

local

(local (in-theory (disable euclid-alg-nat-gives-gcd)))

local

(local (defthm euclid-alg-nat-gives-gcd-alternate
    (implies (and (np a) (np b))
      (equal (mv-nth 0 (euclid-alg-nat a b))
        (+ (* (mv-nth 1 (euclid-alg-nat a b)) a)
          (* (mv-nth 2 (euclid-alg-nat a b)) b))))
    :hints (("Goal" :use euclid-alg-nat-gives-gcd))))

grcd-is-linear-combinationtheorem

(defthm grcd-is-linear-combination
  (equal (grcd a b)
    (+ (* a (grcd-lin-1 a b)) (* b (grcd-lin-2 a b)))))

local

(local (in-theory (disable euclid-alg-nat-gives-gcd-alternate)))

local

(local (in-theory (disable euclid-alg-nat-commutes-with-*)))

grcd-commutes-with-*theorem

(defthm grcd-commutes-with-*
  (implies (and (integerp a) (integerp b) (np c))
    (equal (grcd (* a c) (* b c)) (* (grcd a b) c)))
  :hints (("Goal" :use (euclid-alg-nat-commutes-with-* (:instance euclid-alg-nat-commutes-with-*
         (a (- a))
         (b (- b)))
       (:instance euclid-alg-nat-commutes-with-* (b (- b)))
       (:instance euclid-alg-nat-commutes-with-* (b (- b)))
       (:instance euclid-alg-nat-commutes-with-* (a (- a)))))))

local

(local (in-theory (enable euclid-alg-nat-gives-gcd)))

local

(local (in-theory (disable euclid-alg-nat-gives-gcd-alternate)))

grcd-divides-op-1-lemmatheorem

(defthm grcd-divides-op-1-lemma
  (implies (and (integerp a) (integerp b))
    (equal (* (grcd a b) (grcd-quotient-1 a b)) a)))

grcd-divides-op-2-lemmatheorem

(defthm grcd-divides-op-2-lemma
  (implies (and (integerp a) (integerp b))
    (equal (* (grcd a b) (grcd-quotient-2 a b)) b)))

in-theory

(in-theory (disable grcd))

in-theory

(in-theory (disable grcd-lin-1))

in-theory

(in-theory (disable grcd-lin-2))

in-theory

(in-theory (disable grcd-quotient-1))

in-theory

(in-theory (disable grcd-quotient-2))

grcd-quotient-1-not-zerotheorem

(defthm grcd-quotient-1-not-zero
  (implies (and (integerp a)
      (integerp b)
      (equal 0 (grcd-quotient-1 a b)))
    (equal (equal 0 (grcd-quotient-1 a b)) (equal 0 a)))
  :hints (("Goal" :in-theory (disable grcd-divides-op-1-lemma)
     :use grcd-divides-op-1-lemma)))

grcd-quotient-2-not-zerotheorem

(defthm grcd-quotient-2-not-zero
  (implies (and (integerp a)
      (integerp b)
      (equal 0 (grcd-quotient-2 a b)))
    (equal (equal 0 (grcd-quotient-2 a b)) (equal 0 b)))
  :hints (("Goal" :in-theory (disable grcd-divides-op-2-lemma)
     :use grcd-divides-op-2-lemma)))

common-divisor-divides-grcdtheorem

(defthm common-divisor-divides-grcd
  (implies (and (divides d a) (divides d b))
    (divides d (grcd a b))))

in-theory

(in-theory (disable grcd-is-linear-combination))

local

(local (defthm grcd-quotients-give-a-/-b-lemma
    (implies (and (integerp a) (integerp b) (not (equal 0 b)))
      (equal (/ (* (grcd a b) (grcd-quotient-1 a b))
          (* (grcd a b) (grcd-quotient-2 a b)))
        (/ a b)))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable associativity-of-*
         distributivity-of-/-over-*
         /-cancellation-on-left)))))

grcd-quotients-gives-a-/-btheorem

(defthm grcd-quotients-gives-a-/-b
  (implies (and (integerp a) (integerp b) (not (equal 0 b)))
    (equal (/ (grcd-quotient-1 a b) (grcd-quotient-2 a b))
      (/ a b)))
  :hints (("Goal" :use grcd-quotients-give-a-/-b-lemma)))

local

(local (defthm grcd-quotients-are-relative-prime-lemma-1
    (implies (and (integerp a) (integerp b))
      (equal (grcd a b)
        (grcd (* (grcd-quotient-1 a b) (grcd a b))
          (* (grcd-quotient-2 a b) (grcd a b)))))
    :rule-classes nil))

local

(local (defthm grcd-quotients-are-relative-prime-lemma-2
    (implies (and (integerp a) (integerp b))
      (equal (grcd (* (grcd-quotient-1 a b) (grcd a b))
          (* (grcd-quotient-2 a b) (grcd a b)))
        (* (grcd a b)
          (grcd (grcd-quotient-1 a b) (grcd-quotient-2 a b)))))
    :rule-classes nil
    :hints (("Goal" :use ((:instance grcd-commutes-with-*
          (a (grcd-quotient-1 a b))
          (b (grcd-quotient-2 a b))
          (c (grcd a b))))))))

grcd-quotients-are-relative-primestheorem

(defthm grcd-quotients-are-relative-primes
  (implies (and (integerp a) (integerp b))
    (equal (grcd (grcd-quotient-1 a b) (grcd-quotient-2 a b)) 1))
  :hints (("Goal" :use (grcd-quotients-are-relative-prime-lemma-1 grcd-quotients-are-relative-prime-lemma-2))))

grcd-quotient-1-descriptiontheorem

(defthm grcd-quotient-1-description
  (implies (and (integerp a) (integerp b))
    (equal (integer-quotient (grcd a b) a)
      (grcd-quotient-1 a b)))
  :hints (("Goal" :use ((:instance integer-quotient-*-cancellation
        (a (grcd a b))
        (q (grcd-quotient-1 a b)))))))

grcd-quotient-2-descriptiontheorem

(defthm grcd-quotient-2-description
  (implies (and (integerp a) (integerp b))
    (equal (integer-quotient (grcd a b) b)
      (grcd-quotient-2 a b)))
  :hints (("Goal" :use ((:instance integer-quotient-*-cancellation
        (a (grcd a b))
        (q (grcd-quotient-2 a b)))))))

in-theory

(in-theory (enable divides-integer-quotient-equivalence))

grcd-divides-op-1theorem

(defthm grcd-divides-op-1
  (implies (and (integerp a) (integerp b))
    (divides (grcd a b) a)))

grcd-divides-op-2theorem

(defthm grcd-divides-op-2
  (implies (and (integerp a) (integerp b))
    (divides (grcd a b) b)))

in-theory

(in-theory (disable divides-integer-quotient-equivalence))

grcd-addition-lemma-1theorem

(defthm grcd-addition-lemma-1
  (implies (and (integerp a) (integerp b) (integerp c))
    (divides (grcd a b) (grcd a (+ b (* a c))))))

grcd-addition-lemma-2theorem

(defthm grcd-addition-lemma-2
  (implies (and (integerp a) (integerp b) (integerp c))
    (divides (grcd a (+ b (* a c))) (grcd a b)))
  :hints (("Goal" :use ((:instance grcd-addition-lemma-1
        (b (+ b (* a c)))
        (c (- c)))))))

grcd-addition-lemmatheorem

(defthm grcd-addition-lemma
  (implies (and (integerp a) (integerp b) (integerp c))
    (equal (grcd a (+ b (* a c))) (grcd a b)))
  :hints (("Goal" :use ((:instance equality-from-division
        (a (grcd a (+ b (* a c))))
        (b (grcd a b)))))))

grcd-a-b-divides-a-bctheorem

(defthm grcd-a-b-divides-a-bc
  (implies (and (integerp a) (integerp b) (integerp c))
    (divides (grcd a b) (grcd a (* b c)))))

local

(local (defthm grcd-multiplication-lemma-1
    (implies (and (integerp a)
        (integerp b)
        (integerp c)
        (equal 1 (grcd a c)))
      (equal (grcd a (* b c (grcd-lin-2 a c)))
        (grcd a
          (+ (* b a (grcd-lin-1 a c)) (* b c (grcd-lin-2 a c))))))
    :hints (("Goal" :use ((:instance grcd-addition-lemma
          (b (* b c (grcd-lin-2 a c)))
          (c (* b (grcd-lin-1 a c)))))))))

local

(local (encapsulate nil
    (local (defthm grcd-multiplication-lemma-2
        (implies (and (integerp a) (integerp c) (equal 1 (grcd a c)))
          (equal (+ (* a (grcd-lin-1 a c)) (* c (grcd-lin-2 a c))) 1))
        :hints (("Goal" :in-theory (enable grcd-is-linear-combination)))))
    (defthm grcd-multiplication-lemma-3
      (implies (and (integerp a)
          (integerp b)
          (integerp c)
          (equal 1 (grcd a c)))
        (equal (* b (+ (* a (grcd-lin-1 a c)) (* c (grcd-lin-2 a c))))
          b))
      :rule-classes nil)))

local

(local (defthm grcd-multiplication-lemma-4
    (implies (and (integerp a)
        (integerp b)
        (integerp c)
        (equal 1 (grcd a c)))
      (equal (+ (* b a (grcd-lin-1 a c)) (* b c (grcd-lin-2 a c)))
        b))
    :hints (("Goal" :use grcd-multiplication-lemma-3))))

local

(local (defthm grcd-multiplication-lemma-5
    (implies (and (integerp a)
        (integerp b)
        (integerp c)
        (equal 1 (grcd a c)))
      (equal (grcd a
          (+ (* b a (grcd-lin-1 a c)) (* b c (grcd-lin-2 a c))))
        (grcd a b)))
    :rule-classes nil
    :hints (("Goal" :use grcd-multiplication-lemma-4))))

local

(local (defthm grcd-multiplication-lemma-6
    (implies (and (integerp a)
        (integerp b)
        (integerp c)
        (equal 1 (grcd a c)))
      (equal (grcd a (* b c (grcd-lin-2 a c))) (grcd a b)))
    :rule-classes nil
    :hints (("Goal" :use grcd-multiplication-lemma-5))))

in-theory

(in-theory (disable common-divisor-divides-grcd))

grcd-multiplication-with-relative-primetheorem

(defthm grcd-multiplication-with-relative-prime
  (implies (and (integerp a)
      (integerp b)
      (integerp c)
      (equal 1 (grcd a c)))
    (equal (grcd a (* b c)) (grcd a b)))
  :hints (("Goal" :use ((:instance grcd-a-b-divides-a-bc
        (b (* b c))
        (c (grcd-lin-2 a c))) grcd-multiplication-lemma-6
       (:instance equality-from-division
         (a (grcd a b))
         (b (grcd a (* b c))))))))

in-theory

(in-theory (enable divides-integer-quotient-equivalence))

grcd-*-cancellationtheorem

(defthm grcd-*-cancellation
  (implies (and (equal b (* a (integer-quotient a b)))
      (np a)
      (integerp b))
    (equal (grcd a b) a))
  :hints (("Goal" :use (:instance grcd-commutes-with-*
       (a 1)
       (b (integer-quotient a b))
       (c a)))))

grcd-divides-connection-lemma-1theorem

(defthm grcd-divides-connection-lemma-1
  (implies (and (np a) (integerp b))
    (implies (divides a b) (equal (grcd a b) a)))
  :hints (("Goal'''" :use grcd-*-cancellation)))

in-theory

(in-theory (disable divides-integer-quotient-equivalence))

grcd-divides-connection-lemma-2theorem

(defthm grcd-divides-connection-lemma-2
  (implies (and (np a) (integerp b))
    (implies (equal (grcd a b) a) (divides a b)))
  :hints (("Goal'''" :use grcd-divides-op-2)))

grcd-divides-connectiontheorem

(defthm grcd-divides-connection
  (implies (and (np a) (integerp b))
    (equal (divides a b) (equal (grcd a b) a))))

in-theory

(in-theory (disable grcd-*-cancellation))

in-theory

(in-theory (disable grcd-divides-connection-lemma-1))

in-theory

(in-theory (disable grcd-divides-connection-lemma-2))

divide-with-relative-prime-lemma-1theorem

(defthm divide-with-relative-prime-lemma-1
  (implies (and (np a)
      (integerp b)
      (integerp c)
      (divides a (* b c))
      (equal (grcd a c) 1))
    (equal (grcd a (* b c)) a))
  :rule-classes nil)

divide-with-relative-prime-lemma-2theorem

(defthm divide-with-relative-prime-lemma-2
  (implies (and (np a)
      (integerp b)
      (integerp c)
      (divides a (* b c))
      (equal (grcd a c) 1))
    (equal (grcd a b) a))
  :rule-classes nil
  :hints (("Goal" :use divide-with-relative-prime-lemma-1)))

divide-with-relative-primetheorem

(defthm divide-with-relative-prime
  (implies (and (np a)
      (integerp b)
      (integerp c)
      (divides a (* b c))
      (equal (grcd a c) 1))
    (divides a b))
  :hints (("Goal" :use divide-with-relative-prime-lemma-2)))