mod-proofs - ACL2 Book

Included Books

ground-zero negative-syntaxp floor arith2 power2p fp2 arith integerp product complex-rationalp meta-plus-equal meta-plus-lessp predicate rationalp fl

other

(in-package "ACL2")

flfunction

(defun fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

include-book

(include-book "ground-zero")

include-book

(include-book "negative-syntaxp")

local

(local (include-book "floor"))

local

(local (include-book "arith2"))

local

(local (include-book "power2p"))

local

(local (include-book "fp2"))

local

(local (include-book "arith"))

local

(local (include-book "integerp"))

local

(local (include-book "product"))

local

(local (include-book "complex-rationalp"))

local

(local (include-book "../../../meta/meta-plus-equal"))

local

(local (include-book "../../../meta/meta-plus-lessp"))

local

(local (include-book "predicate"))

local

(local (include-book "rationalp"))

mod-rational-when-y-is-rational-rewritetheorem

(defthm mod-rational-when-y-is-rational-rewrite
  (implies (and (rationalp y) (case-split (acl2-numberp x)))
    (equal (rationalp (mod x y)) (rationalp x)))
  :hints (("Goal" :in-theory (enable mod))))

mod-with-x-a-non-acl2-number-is-zerotheorem

(defthm mod-with-x-a-non-acl2-number-is-zero
  (implies (not (acl2-numberp x)) (equal (mod x y) 0))
  :hints (("Goal" :in-theory (enable mod))))

mod-when-y-is-complex-rationalptheorem

(defthmd mod-when-y-is-complex-rationalp
  (implies (complex-rationalp y)
    (equal (mod x y)
      (if (not (complex-rationalp x))
        (fix x)
        (if (not (rationalp (/ x y)))
          x
          (if (integerp (/ x y))
            0
            (+ x (* -1 y (floor (* x (/ y)) 1))))))))
  :otf-flg t
  :hints (("Goal" :in-theory (enable mod))))

mod-when-y-is-not-an-acl2-numberptheorem

(defthmd mod-when-y-is-not-an-acl2-numberp
  (implies (not (acl2-numberp y)) (equal (mod x y) (fix x)))
  :otf-flg t
  :hints (("Goal" :in-theory (enable mod))))

mod-acl2-numberp-type-prescriptiontheorem

(defthm mod-acl2-numberp-type-prescription
  (acl2-numberp (mod x y))
  :rule-classes (:type-prescription))

mod-acl2-numberptheorem

(defthm mod-acl2-numberp (acl2-numberp (mod x y)))

mod-rationalptheorem

(defthm mod-rationalp
  (implies (case-split (not (complex-rationalp x)))
    (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :cases ((rationalp x)) :in-theory (enable mod))))

mod-non-negativetheorem

(defthm mod-non-negative
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= 0 (mod x y)))
  :hints (("Goal" :cases ((acl2-numberp y)) :in-theory (enable mod))))

mod-non-negative-rationalp-type-prescriptiontheorem

(defthm mod-non-negative-rationalp-type-prescription
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (and (<= 0 (mod x y)) (rationalp (mod x y))))
  :rule-classes ((:type-prescription :typed-term (mod x y))))

mod-non-negative-lineartheorem

(defthm mod-non-negative-linear
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= 0 (mod x y)))
  :rule-classes ((:linear :trigger-terms ((mod x y)))))

mod-upper-boundtheorem

(defthm mod-upper-bound
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) y))
  :hints (("Goal" :in-theory (enable mod) :cases ((rationalp x)))))

mod-upper-bound-lineartheorem

(defthm mod-upper-bound-linear
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) y))
  :rule-classes ((:linear :trigger-terms ((mod x y)))))

mod-upper-bound-less-tight-rewritetheorem

(defthm mod-upper-bound-less-tight-rewrite
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= (mod x y) y)))

mod-upper-bound-3theorem

(defthm mod-upper-bound-3
  (implies (and (<= y z)
      (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) z)))

mod-upper-bound-2theorem

(defthm mod-upper-bound-2
  (implies (and (<= 0 x) (case-split (not (complex-rationalp x))))
    (<= (mod x y) x))
  :rule-classes (:rewrite (:linear :trigger-terms ((mod x y))))
  :hints (("Goal" :in-theory (enable mod))))

mod-integerptheorem

(defthm mod-integerp
  (implies (and (integerp x) (integerp y))
    (integerp (mod x y)))
  :hints (("Goal" :in-theory (enable mod)))
  :rule-classes (:rewrite :type-prescription))

mod-integerp-2theorem

(defthm mod-integerp-2
  (implies (and (integerp y) (case-split (acl2-numberp x)))
    (equal (integerp (mod x y)) (integerp x)))
  :hints (("Goal" :in-theory (enable mod))))

mod-0theorem

(defthm mod-0
  (and (equal (mod 0 y) 0) (equal (mod x 0) (fix x)))
  :hints (("Goal" :in-theory (enable mod))))

mod-complex-rationalp-rewritetheorem

(defthm mod-complex-rationalp-rewrite
  (implies (case-split (rationalp y))
    (equal (complex-rationalp (mod x y)) (complex-rationalp x)))
  :hints (("Goal" :in-theory (enable mod))))

mod-non-positive-type-prescriptiontheorem

(defthm mod-non-positive-type-prescription
  (implies (and (< y 0) (rationalp x) (rationalp y))
    (and (rationalp (mod x y)) (<= (mod x y) 0)))
  :hints (("Goal" :in-theory (enable mod)))
  :rule-classes (:type-prescription))

mod-non-positivetheorem

(defthm mod-non-positive
  (implies (and (< y 0)
      (case-split (rationalp x))
      (case-split (rationalp y)))
    (<= (mod x y) 0)))

local

(local (include-book "fl"))

mod-drop-irrelevant-first-termtheorem

(defthm mod-drop-irrelevant-first-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x))))
    (equal (mod (+ k x) y) (mod x y)))
  :hints (("Goal" :in-theory (enable mod))))

mod-drop-irrelevant-second-termtheorem

(defthm mod-drop-irrelevant-second-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x))))
    (equal (mod (+ x k) y) (mod x y))))

mod-drop-irrelevant-second-term-with-more-termstheorem

(defthm mod-drop-irrelevant-second-term-with-more-terms
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x k x2) y) (mod (+ x x2) y))))

mod-drop-irrelevant-third-termtheorem

(defthm mod-drop-irrelevant-third-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x x2 k) y) (mod (+ x x2) y))))

mod-mult-erictheorem

(defthm mod-mult-eric
  (implies (and (integerp a)
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (+ x (* a y)) y) (mod x y))))

mod-sum-elim-secondtheorem

(defthm mod-sum-elim-second
  (implies (and (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x1 (mod x2 y)) y) (mod (+ x1 x2) y)))
  :hints (("Goal" :in-theory (enable mod)
     :cases ((and (rationalp x2) (equal y 0) (rationalp x1)) (and (rationalp x2) (equal y 0) (not (rationalp x1)))
       (and (rationalp x2) (not (equal y 0)) (rationalp x1))
       (and (rationalp x2) (not (equal y 0)) (not (rationalp x1)))
       (and (not (acl2-numberp x2)) (equal y 0) (rationalp x1))
       (and (not (acl2-numberp x2))
         (equal y 0)
         (not (rationalp x1)))
       (and (not (acl2-numberp x2))
         (not (equal y 0))
         (rationalp x1))
       (and (not (acl2-numberp x2))
         (not (equal y 0))
         (not (rationalp x1)))))))

mod-sum-elim-second-gentheorem

(defthm mod-sum-elim-second-gen
  (implies (and (integerp (/ y2 y))
      (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y)))
    (equal (mod (+ x1 (mod x2 y2)) y) (mod (+ x1 x2) y)))
  :hints (("Goal" :in-theory (enable mod)
     :cases ((and (rationalp x2) (equal y 0) (rationalp x1)) (and (rationalp x2) (equal y 0) (not (rationalp x1)))
       (and (rationalp x2) (not (equal y 0)) (rationalp x1))
       (and (rationalp x2) (not (equal y 0)) (not (rationalp x1)))
       (and (not (acl2-numberp x2)) (equal y 0) (rationalp x1))
       (and (not (acl2-numberp x2))
         (equal y 0)
         (not (rationalp x1)))
       (and (not (acl2-numberp x2))
         (not (equal y 0))
         (rationalp x1))
       (and (not (acl2-numberp x2))
         (not (equal y 0))
         (not (rationalp x1)))))))

mod-sum-elim-firsttheorem

(defthm mod-sum-elim-first
  (implies (and (case-split (not (complex-rationalp a)))
      (case-split (not (complex-rationalp b))))
    (equal (mod (+ (mod b y) a) y) (mod (+ a b) y))))

mod-sum-elim-first-gentheorem

(defthm mod-sum-elim-first-gen
  (implies (and (integerp (/ y2 y))
      (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y)))
    (equal (mod (+ (mod x2 y2) x1) y) (mod (+ x1 x2) y))))

mod-sum-elim-boththeorem

(defthm mod-sum-elim-both
  (implies (and (case-split (not (complex-rationalp a)))
      (case-split (not (complex-rationalp b))))
    (equal (mod (+ (mod a y) (mod b y)) y) (mod (+ a b) y))))

mod-difference-elim-secondtheorem

(defthm mod-difference-elim-second
  (implies (and (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (mod (+ x1 (* -1 (mod x2 y))) y)
      (mod (+ x1 (* -1 x2)) y)))
  :hints (("Goal" :in-theory (enable mod))))

mod-sum-elim-negative-first-argtheorem

(defthm mod-sum-elim-negative-first-arg
  (implies (and (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (mod (+ (* -1 (mod x2 y)) x1) y)
      (mod (+ (* -1 x2) x1) y))))

mod-by-1theorem

(defthm mod-by-1 (implies (integerp m) (equal (mod m 1) 0)))

mod-mult-of-ntheorem

(defthmd mod-mult-of-n
  (implies (and (integerp (* x (/ y)))
      (not (equal y 0))
      (rationalp x)
      (rationalp y))
    (equal (mod x y) 0))
  :hints (("goal" :in-theory (enable mod))))

mod-negative-ytheorem

(defthmd mod-negative-y
  (implies (and (< 0 y) (integerp x) (integerp y))
    (equal (mod x (- y))
      (if (integerp (/ x y))
        0
        (+ (- y) (mod x y)))))
  :hints (("Goal" :in-theory (enable mod))))

mod-does-nothingtheorem

(defthm mod-does-nothing
  (implies (and (< m n) (<= 0 m) (case-split (rationalp m)))
    (equal (mod m n) m))
  :hints (("Goal" :in-theory (enable mod))))

mod-mod-etheorem

(defthm mod-mod-e
  (implies (and (integerp (/ y1 y2))
      (case-split (not (equal y2 0)))
      (case-split (rationalp y1))
      (case-split (rationalp y2)))
    (equal (mod (mod x y1) y2) (mod x y2)))
  :hints (("Goal" :in-theory (enable mod))))

mod-of-modtheorem

(defthm mod-of-mod
  (implies (and (case-split (natp k)) (case-split (natp n)))
    (equal (mod (mod x (* k n)) n) (mod x n))))

mod-idempotenttheorem

(defthm mod-idempotent
  (implies (and (case-split (rationalp x)) (case-split (rationalp y)))
    (equal (mod (mod x y) y) (mod x y))))

mod-fl-2theorem

(defthm mod-fl-2
  (implies (case-split (acl2-numberp x))
    (equal (+ (* y (fl (/ x y))) (mod x y)) x))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable floor-fl mod))))

mod-deftheorem

(defthm mod-def
  (implies (case-split (acl2-numberp x))
    (equal (mod x y) (- x (* y (fl (/ x y))))))
  :hints (("Goal" :in-theory (union-theories (current-theory :here)
       (theory 'ground-zero))))
  :rule-classes nil)

mod-force-erictheorem

(defthmd mod-force-eric
  (implies (and (<= (* a y) x)
      (< x (* (1+ a) y))
      (integerp a)
      (rationalp x)
      (rationalp y))
    (equal (mod x y) (- x (* a y))))
  :hints (("goal" :in-theory (enable mod)
     :use ((:instance fl-unique (x (/ x y)) (n a))))))

mod-force-chosen-a-negtheorem

(defthmd mod-force-chosen-a-neg
  (implies (and (< x 0) (<= (* -1 y) x) (rationalp x) (rationalp y))
    (equal (mod x y) (- x (* -1 y))))
  :hints (("Goal" :in-theory (disable mod-force-eric)
     :use (:instance mod-force-eric (a -1)))))

mod-eventheorem

(defthm mod-even
  (implies (rationalp x)
    (equal (integerp (* 1/2 (mod x 2))) (integerp (* 1/2 x))))
  :hints (("Goal" :in-theory (enable mod))))

mod-even-gentheorem

(defthm mod-even-gen
  (implies (and (rationalp x) (integerp n) (integerp (* 1/2 n)))
    (equal (integerp (* 1/2 (mod x n))) (integerp (* 1/2 x))))
  :hints (("Goal" :in-theory (enable mod))))

mod-canceltheorem

(defthmd mod-cancel
  (implies (syntaxp (not (and (quotep y) (equal (cadr y) 1))))
    (equal (mod x y)
      (if (acl2-numberp x)
        (if (acl2-numberp y)
          (if (equal 0 y)
            x
            (* y (mod (/ x y) 1)))
          x)
        0)))
  :hints (("Goal" :in-theory (enable mod inverse-of-*))))

mod-equal-0theorem

(defthmd mod-equal-0
  (implies (and (case-split (rationalp y))
      (case-split (not (equal y 0))))
    (equal (equal (mod x y) 0) (integerp (* (/ y) x))))
  :hints (("Goal" :in-theory (enable mod))))

mod-minus-case-non-integerptheorem

(defthmd mod-minus-case-non-integerp
  (implies (and (not (integerp (/ x y)))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (* -1 x) y) (- y (mod x y))))
  :hints (("Goal" :in-theory (enable mod))))

mod-minus-case-integerptheorem

(defthmd mod-minus-case-integerp
  (implies (and (integerp (/ x y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (* -1 x) y) (- (mod x y))))
  :hints (("Goal" :in-theory (enable mod))))

mod-minus-case-integerp-bettertheorem

(defthmd mod-minus-case-integerp-better
  (implies (and (integerp (/ x y))
      (case-split (not (equal 0 y)))
      (case-split (rationalp y)))
    (equal (mod (* -1 x) y) 0))
  :hints (("Goal" :use (mod-minus-case-integerp mod-equal-0))))

mod-minustheorem

(defthm mod-minus
  (implies (and (case-split (rationalp x)) (case-split (rationalp y)))
    (equal (mod (* -1 x) y)
      (if (equal 0 y)
        (- x)
        (if (integerp (/ x y))
          0
          (- y (mod x y))))))
  :hints (("Goal" :in-theory (e/d (mod-minus-case-integerp-better mod-minus-case-non-integerp)
       nil)
     :cases ((integerp (/ x y))))))

mod-minus-alttheorem

(defthm mod-minus-alt
  (implies (and (syntaxp (negative-syntaxp x))
      (case-split (rationalp x))
      (case-split (rationalp y)))
    (equal (mod x y)
      (if (equal 0 y)
        x
        (if (integerp (/ (- x) y))
          0
          (- y (mod (- x) y))))))
  :hints (("Goal" :in-theory (disable mod-minus)
     :use (:instance mod-minus (x (- x))))))

mod-1-integerptheorem

(defthm mod-1-integerp
  (implies (case-split (acl2-numberp x))
    (equal (integerp (mod x 1)) (integerp x)))
  :hints (("Goal" :in-theory (enable mod))))

mod-by-2-rewrite-to-eventheorem

(defthmd mod-by-2-rewrite-to-even
  (implies (integerp x)
    (equal (equal (mod x 2) 0) (integerp (* 1/2 x))))
  :otf-flg t
  :hints (("Goal" :in-theory (enable mod))))

fl-plus-mdtheorem

(defthm fl-plus-md
  (implies (rationalp x) (equal (+ (fl x) (mod x 1)) x))
  :hints (("Goal" :in-theory (enable mod))))

mod-1-sum-integertheorem

(defthm mod-1-sum-integer
  (implies (and (rationalp x) (rationalp y))
    (equal (integerp (+ x (mod y 1))) (integerp (+ x y))))
  :hints (("Goal" :in-theory (enable mod))))

mod-quotient-integerptheorem

(defthm mod-quotient-integerp
  (implies (and (integerp (* y k))
      (rationalp x)
      (rationalp y)
      (rationalp k))
    (equal (integerp (* k (mod x y))) (integerp (* k x))))
  :hints (("Goal" :in-theory (enable mod))))

mod-mod-2-thmtheorem

(defthm mod-mod-2-thm
  (implies (and (<= y1 y2)
      (case-split (< 0 y1))
      (case-split (acl2-numberp x))
      (case-split (rationalp y1))
      (case-split (rationalp y2))
      (case-split (not (equal y1 0))))
    (equal (mod (mod x y1) y2) (mod x y1)))
  :otf-flg t
  :hints (("Goal" :in-theory (enable mod))))

mod-2-1-means-oddtheorem

(defthmd mod-2-1-means-odd
  (implies (integerp x)
    (equal (equal (mod x 2) 1) (not (integerp (* 1/2 x)))))
  :hints (("Goal" :in-theory (enable mod))))

mod-integerp-2-2theorem

(defthm mod-integerp-2-2
  (implies (and (integerp y) (integerp x))
    (integerp (mod x (/ y))))
  :hints (("Goal" :cases ((equal 0 y)) :in-theory (enable mod))))

mod-cancel-special-1theorem

(defthm mod-cancel-special-1
  (implies (and (acl2-numberp x)
      (rationalp k)
      (acl2-numberp y)
      (not (equal y 0))
      (not (equal k 0)))
    (equal (mod (* k x) (* y k)) (* k (mod x y))))
  :hints (("goal" :in-theory (enable mod-cancel))))

mod-integerp-when-y-is-an-inversetheorem

(defthm mod-integerp-when-y-is-an-inverse
  (implies (and (integerp (/ y)) (integerp x))
    (integerp (mod x y)))
  :hints (("Goal" :in-theory (enable mod))))

mod-when-y-is-an-inversetheorem

(defthm mod-when-y-is-an-inverse
  (implies (and (integerp (/ y)) (integerp x) (case-split (< 0 y)))
    (equal (mod x y) 0))
  :hints (("Goal" :in-theory (enable mod))))

fl-mod-x-1theorem

(defthm fl-mod-x-1 (equal (fl (mod x 1)) 0))

mod-by-2theorem

(defthmd mod-by-2
  (implies (integerp x)
    (equal (mod x 2)
      (if (integerp (* 1/2 x))
        0
        1)))
  :hints (("Goal" :in-theory (enable mod-by-2-rewrite-to-even mod-2-1-means-odd))))

mod-sum-moveencapsulate

(encapsulate nil
  (local (defthm mod-sum-move-forward-implication
      (implies (and (case-split (<= 0 k1))
          (case-split (< k1 y))
          (rationalp y)
          (rationalp x)
          (rationalp k1))
        (implies (equal k1 (mod (+ k2 x) y))
          (equal (mod (+ k1 (- k2)) y) (mod x y))))
      :rule-classes nil))
  (local (defthm mod-sum-move-backward-implication
      (implies (and (case-split (<= 0 k1))
          (case-split (< k1 y))
          (rationalp y)
          (rationalp x)
          (rationalp k1))
        (implies (equal (mod (+ k1 (- k2)) y) (mod x y))
          (equal k1 (mod (+ k2 x) y))))
      :rule-classes nil
      :hints (("Goal" :use ((:instance mod-sum-move-forward-implication
            (k1 (mod x y))
            (x k1)
            (k2 (- k2))))))))
  (defthm mod-sum-move
    (implies (and (case-split (<= 0 k1))
        (case-split (< k1 y))
        (case-split (rationalp y))
        (case-split (rationalp x))
        (case-split (rationalp k1)))
      (equal (equal k1 (mod (+ k2 x) y))
        (equal (mod (+ k1 (- k2)) y) (mod x y))))
    :rule-classes nil
    :hints (("Goal" :use (mod-sum-move-forward-implication mod-sum-move-backward-implication)))))

mod-sum-move-constantstheorem

(defthm mod-sum-move-constants
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
      (case-split (<= 0 k1))
      (case-split (< k1 y))
      (rationalp y)
      (rationalp x)
      (rationalp k1))
    (equal (equal k1 (mod (+ k2 x) y))
      (equal (mod (+ k1 (- k2)) y) (mod x y))))
  :hints (("Goal" :use mod-sum-move)))

mod-sums-cancel-1theorem

(defthm mod-sums-cancel-1
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ k x1) y) (mod (+ k x2) y))
      (equal (mod x1 y) (mod x2 y))))
  :hints (("Goal" :use (:instance mod-sum-move (k2 k) (x x2) (k1 (mod (+ k x1) y))))))

mod-sums-cancel-2theorem

(defthm mod-sums-cancel-2
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ x1 k) y) (mod (+ k x2) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-3theorem

(defthm mod-sums-cancel-3
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ x1 k) y) (mod (+ x2 k) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-4theorem

(defthm mod-sums-cancel-4
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ k x1) y) (mod (+ x2 k) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-5theorem

(defthm mod-sums-cancel-5
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod k y) (mod (+ x k) y))
      (equal 0 (mod x y))))
  :hints (("Goal" :use (:instance mod-sums-cancel-4 (x1 0) (x2 x)))))

mod-sums-cancel-6theorem

(defthm mod-sums-cancel-6
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod k y) (mod (+ k x) y))
      (equal 0 (mod x y))))
  :hints (("Goal" :use (:instance mod-sums-cancel-4 (x1 0) (x2 x)))))

mod-sums-cancel-7theorem

(defthm mod-sums-cancel-7
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod (+ k x) y) (mod k y))
      (equal 0 (mod x y))))
  :hints (("Goal" :use (:instance mod-sums-cancel-4 (x1 0) (x2 x)))))

mod-sums-cancel-8theorem

(defthm mod-sums-cancel-8
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod (+ x k) y) (mod k y))
      (equal 0 (mod x y))))
  :hints (("Goal" :use (:instance mod-sums-cancel-4 (x1 0) (x2 x)))))

fl-mod-equaltheorem

(defthm fl-mod-equal
  (implies (and (equal (fl (/ x 2)) (fl (/ y 2)))
      (equal (mod x 2) (mod y 2))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal x y))
  :hints (("goal" :in-theory (enable mod)))
  :rule-classes nil)

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

mod-bnd-1theorem

(defthmd mod-bnd-1
  (implies (and (case-split (< 0 n))
      (case-split (not (complex-rationalp m)))
      (case-split (not (complex-rationalp n))))
    (< (mod m n) n))
  :rule-classes :linear)

quot-modtheorem

(defthm quot-mod
  (implies (case-split (acl2-numberp m))
    (equal (+ (* n (fl (/ m n))) (mod m n)) m))
  :rule-classes nil
  :hints (("Goal" :in-theory (e/d (mod floor-fl)))))

mod-mult-erictheorem

(defthm mod-mult-eric
  (implies (and (integerp a)
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (+ x (* a y)) y) (mod x y))))

integerp-modtheorem

(defthm integerp-mod
  (implies (and (integerp m) (integerp n))
    (integerp (mod m n)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (enable mod))))

rationalp-modtheorem

(defthm rationalp-mod
  (implies (rationalp x) (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (enable mod))))

rationalp-mod-case-splittheorem

(defthm rationalp-mod-case-split
  (implies (case-split (rationalp x)) (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (enable mod))))

in-theory

(in-theory (disable rationalp-mod))

mod-0-fltheorem

(defthm mod-0-fl
  (implies (acl2-numberp m)
    (iff (= (mod m n) 0) (= m (* (fl (/ m n)) n))))
  :rule-classes nil
  :hints (("goal" :use (quot-mod))))

mod-0-0theorem

(defthm mod-0-0
  (implies (and (integerp p) (rationalp m) (rationalp n))
    (iff (= (mod m (* n p)) 0)
      (and (= (mod m n) 0) (= (mod (fl (/ m n)) p) 0))))
  :rule-classes nil
  :hints (("goal" :in-theory (enable mod))))

mod-prodtheorem

(defthmd mod-prod
  (implies (and (rationalp m) (rationalp n) (rationalp k))
    (equal (mod (* k m) (* k n)) (* k (mod m n))))
  :hints (("goal" :in-theory (enable mod-cancel))))

mod012theorem

(defthm mod012
  (implies (integerp m)
    (or (equal (mod m 2) 0) (equal (mod m 2) 1)))
  :rule-classes nil
  :hints (("Goal" :use ((:instance mod-bnd-1 (m m) (n 2))))))

mod-mod-2-not-equaltheorem

(defthm mod-mod-2-not-equal
  (implies (acl2-numberp m)
    (not (= (mod m 2) (mod (1+ m) 2))))
  :rule-classes nil
  :hints (("Goal" :use ((:instance quot-mod (m m) (n 2)) (:instance quot-mod (m (1+ m)) (n 2))))))

mod-mod-sumencapsulate

(encapsulate nil
  (defthmd mod-sum
    (implies (and (rationalp a) (rationalp b))
      (equal (mod (+ a (mod b n)) n) (mod (+ a b) n))))
  (defthm mod-mod-sum
    (implies (and (rationalp a) (rationalp b))
      (equal (mod (+ (mod a n) (mod b n)) n) (mod (+ a b) n))))
  (defthmd mod-bnd-2
    (implies (and (<= 0 m) (case-split (rationalp m)))
      (<= (mod m n) m))
    :rule-classes :linear))

mod-plus-mod-2theorem

(defthm mod-plus-mod-2
  (implies (and (integerp a) (integerp b))
    (iff (= (mod (+ a b) 2) (mod a 2)) (= (mod b 2) 0)))
  :rule-classes nil
  :hints (("goal" :in-theory (e/d (mod-mult-of-n)
       (mod-sum-elim-second mod-drop-irrelevant-second-term
         mod-2-1-means-odd))
     :use ((:instance mod012 (m b)) (:instance mod-sum (a a) (b b) (n 2))
       (:instance mod-mod-2-not-equal)))))

mod-must-be-ntheorem

(defthm mod-must-be-n
  (implies (and (= (mod m n) 0)
      (< m (* 2 n))
      (< 0 m)
      (rationalp m)
      (rationalp n))
    (= m n))
  :rule-classes nil
  :hints (("goal" :in-theory (disable mod-does-nothing)
     :use ((:instance mod-does-nothing (m m) (n n)) (:instance mod-does-nothing (n n) (m (- m n)))))))

natp-compound-recognizertheorem

(defthm natp-compound-recognizer
  (equal (natp x) (and (integerp x) (<= 0 x)))
  :rule-classes :compound-recognizer)

natp-modtheorem

(defthm natp-mod
  (implies (and (natp m) (natp n)) (natp (mod m n)))
  :rule-classes ((:type-prescription :typed-term (mod m n)))
  :hints (("Goal" :use (:instance mod-non-negative (x m) (y n)))))

natp-mod-rewritetheorem

(defthm natp-mod-rewrite
  (implies (and (natp m) (natp n)) (natp (mod m n))))

mod-multtheorem

(defthmd mod-mult
  (implies (and (integerp a) (rationalp m) (rationalp n))
    (equal (mod (+ m (* a n)) n) (mod m n)))
  :hints (("Goal")))

mod-difftheorem

(defthmd mod-diff
  (implies (and (case-split (rationalp a)) (case-split (rationalp b)))
    (equal (mod (- a (mod b n)) n) (mod (- a b) n))))

mod-bnd-3theorem

(defthmd mod-bnd-3
  (implies (and (< m (+ (* a n) r))
      (<= (* a n) m)
      (integerp a)
      (case-split (rationalp m))
      (case-split (rationalp n)))
    (< (mod m n) r))
  :rule-classes :linear :hints (("goal" :in-theory (disable fl-<-integer)
     :use ((:instance quot-mod) (:instance n<=fl-linear (x (/ m n)) (n a))))))

mod-forcetheorem

(defthm mod-force
  (implies (and (<= (* a n) m)
      (< m (* (1+ a) n))
      (integerp a)
      (rationalp m)
      (rationalp n))
    (= (mod m n) (- m (* a n))))
  :rule-classes nil
  :hints (("goal" :use ((:instance quot-mod) (:instance fl-unique (x (/ m n)) (n a))))))

local

(local (defthm mod=mod-1
    (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b))
      (= (- a (* n (fl (/ a n)))) (- b (* n (fl (/ b n))))))
    :rule-classes nil
    :hints (("goal" :use ((:instance quot-mod (m a)) (:instance quot-mod (m b)))))))

local

(local (defthm mod=mod-2
    (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b))
      (= (- a b) (* n (- (fl (/ a n)) (fl (/ b n))))))
    :rule-classes nil
    :hints (("goal" :use ((:instance mod=mod-1))))))

local

(local (defthm hack-m10
    (implies (and (rationalp a)
        (rationalp b)
        (rationalp c)
        (> b 0)
        (= a (* b c)))
      (= (/ a b) c))
    :rule-classes nil))

local

(local (defthm mod=mod-3
    (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b))
      (= (/ (- a b) n) (- (fl (/ a n)) (fl (/ b n)))))
    :rule-classes nil
    :hints (("goal" :use ((:instance mod=mod-2) (:instance hack-m10
           (a (- a b))
           (b n)
           (c (- (fl (/ a n)) (fl (/ b n))))))))))

mod-equal-inttheorem

(defthm mod-equal-int
  (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b))
    (integerp (/ (- a b) n)))
  :rule-classes nil
  :hints (("goal" :use ((:instance mod=mod-3)))))

local

(local (defthm mod-equal-int-reverse-1
    (implies (and (rationalp a) (rationalp b))
      (equal (integerp (/ (- a b) n))
        (integerp (/ (- (mod a n) (mod b n)) n))))
    :rule-classes nil
    :hints (("goal" :use ((:instance mod-def (x a) (y n)) (:instance mod-def (x b) (y n)))))))

local

(local (defthm mod-equal-int-reverse-2
    (implies (and (rationalp a) (rationalp b))
      (equal (integerp (/ (- a b) n))
        (integerp (/ (- (mod a n) (mod b n)) n))))
    :rule-classes nil
    :hints (("goal" :use mod-equal-int-reverse-1))))

local

(local (defthm mod-equal-int-reverse-3-1-1-1
    (implies (and (rationalp i) (<= 0 i) (rationalp n) (< i n))
      (implies (integerp (/ i n)) (= i 0)))
    :rule-classes nil))

local

(local (defthm mod-equal-int-reverse-3-1-1
    (implies (and (rationalp i) (rationalp n) (< (abs i) n))
      (implies (integerp (/ i n)) (= i 0)))
    :hints (("Goal" :use (mod-equal-int-reverse-3-1-1-1 (:instance mod-equal-int-reverse-3-1-1-1 (i (- i))))))
    :rule-classes nil))

local

(local (defthm mod-equal-int-reverse-3-1
    (implies (and (rationalp i)
        (<= 0 i)
        (rationalp j)
        (<= 0 j)
        (rationalp n)
        (< i n)
        (< j n))
      (implies (integerp (/ (- i j) n)) (= i j)))
    :hints (("Goal" :use ((:instance mod-equal-int-reverse-3-1-1 (i (- i j))))))
    :rule-classes nil))

local

(local (defthm mod-equal-int-reverse-3
    (implies (and (rationalp a) (rationalp b) (rationalp n) (< 0 n))
      (implies (integerp (/ (- a b) n)) (= (mod a n) (mod b n))))
    :rule-classes nil
    :hints (("goal" :use (mod-equal-int-reverse-2 (:instance mod-equal-int-reverse-3-1
           (i (mod a n))
           (j (mod b n))))))))

local

(local (defthm mod-equal-int-reverse-4
    (implies (and (rationalp a) (rationalp b) (rationalp n) (< 0 n))
      (implies (= (mod a n) (mod b n)) (integerp (/ (- a b) n))))
    :rule-classes nil
    :hints (("goal" :use (mod=mod-3)))))

mod-equal-int-reversetheorem

(defthm mod-equal-int-reverse
  (implies (and (integerp (/ (- a b) n))
      (rationalp a)
      (rationalp b)
      (rationalp n)
      (< 0 n))
    (= (mod a n) (mod b n)))
  :rule-classes nil
  :hints (("goal" :use (mod-equal-int-reverse-3 mod-equal-int-reverse-4))))

mod-mult-2theorem

(defthmd mod-mult-2
  (implies (integerp a) (equal (mod (* a n) n) 0))
  :hints (("goal" :in-theory (enable mod-when-y-is-complex-rationalp)
     :use ((:instance mod-mult-eric (x 0) (y n))))))

mod-mult-2-alttheorem

(defthmd mod-mult-2-alt
  (implies (integerp a) (equal (mod (* n a) n) 0))
  :hints (("Goal" :in-theory (enable mod-mult-2))))

mod-mult-ntheorem

(defthmd mod-mult-n
  (equal (mod (* a n) n) (* n (mod a 1)))
  :hints (("Goal" :in-theory (enable mod))))

mod-mult-n-commutedtheorem

(defthmd mod-mult-n-commuted
  (equal (mod (* n a) n) (* n (mod a 1)))
  :hints (("Goal" :in-theory (enable mod))))

mod-0-inttheorem

(defthm mod-0-int
  (implies (and (integerp m) (integerp n) (not (= n 0)))
    (iff (= (mod m n) 0) (integerp (/ m n))))
  :hints (("Goal" :use ((:instance mod-equal-int (a m) (b 0) (n n)) quot-mod)))
  :rule-classes nil)

mod-2*itheorem

(defthm mod-2*i
  (implies (integerp i) (equal (mod (* 2 i) 2) 0))
  :hints (("Goal" :in-theory (enable mod-mult-2-alt))))

mod-2*m+1-rewritetheorem

(defthm mod-2*m+1-rewrite
  (implies (integerp m) (equal (mod (1+ (* 2 m)) 2) 1)))

mod-2*i+1theorem

(defthm mod-2*i+1
  (implies (integerp i) (not (equal (mod (1+ (* 2 i)) 2) 0))))

induct-natfunction

(defun induct-nat
  (x)
  (if (and (integerp x) (> x 0))
    (induct-nat (1- x))
    nil))

local

(local (defthm nk>=k-1
    (implies (and (integerp n)
        (>= n 0)
        (integerp k)
        (> k 0)
        (not (= (* n k) 0)))
      (>= (* n k) k))
    :rule-classes nil
    :hints (("goal" :induct (induct-nat n)))))

local

(local (defthm nk>=k-2
    (implies (and (integerp n)
        (>= n 0)
        (integerp k)
        (> k 0)
        (not (= (* n k) 0)))
      (>= (abs (* n k)) k))
    :rule-classes nil
    :hints (("goal" :use (nk>=k-1)))))

local

(local (defthm nk>=k-3
    (implies (and (integerp n)
        (<= n 0)
        (integerp k)
        (> k 0)
        (not (= (* n k) 0)))
      (>= (abs (* n k)) k))
    :rule-classes nil
    :hints (("goal" :use ((:instance nk>=k-2 (n (- n))))))))

nk>=ktheorem

(defthm nk>=k
  (implies (and (integerp n) (integerp k) (> k 0) (not (= (* n k) 0)))
    (>= (abs (* n k)) k))
  :rule-classes nil
  :hints (("goal" :use (nk>=k-2 nk>=k-3))))

mod-force-equaltheorem

(defthm mod-force-equal
  (implies (and (< (abs (- a b)) n)
      (rationalp a)
      (rationalp b)
      (integerp n))
    (iff (= (mod a n) (mod b n)) (= a b)))
  :rule-classes nil
  :hints (("goal" :use (mod-equal-int (:instance nk>=k (k n) (n (/ (- a b) n)))))))

nk>=k-lineartheorem

(defthm nk>=k-linear
  (implies (and (integerp n) (integerp k) (not (= n 0)))
    (>= (abs (* n k)) k))
  :rule-classes :linear :hints (("Goal" :use nk>=k)))

mod-mult-2-gentheorem

(defthm mod-mult-2-gen
  (equal (mod (* a n) n) (* n (mod a 1)))
  :hints (("Goal" :in-theory (enable mod-cancel))))

mod-mult-2-alt-gentheorem

(defthm mod-mult-2-alt-gen
  (equal (mod (* n a) n) (* n (mod a 1)))
  :hints (("Goal" :in-theory (enable mod-cancel))))

fl-modtheorem

(defthm fl-mod
  (implies (and (rationalp x) (natp y))
    (equal (fl (mod x y)) (mod (fl x) y)))
  :hints (("Goal" :in-theory (enable mod))))

mod-sum-casestheorem

(defthmd mod-sum-cases
  (implies (and (<= 0 y) (rationalp x) (rationalp y) (rationalp k))
    (equal (mod (+ k x) y)
      (if (< (+ (mod k y) (mod x y)) y)
        (+ (mod k y) (mod x y))
        (+ (mod k y) (mod x y) (* -1 y)))))
  :otf-flg t
  :hints (("Goal" :use ((:instance mod-does-nothing
        (m (+ (mod k y) (mod x y)))
        (n y)) (:instance mod-force-eric (a 1) (x (+ (mod k y) (mod x y)))))
     :in-theory (disable mod-does-nothing))))

mod-fl-erictheorem

(defthmd mod-fl-eric
  (implies (and (<= 0 y) (integerp y))
    (equal (mod (fl x) y) (fl (mod x y))))
  :hints (("Goal" :use (:instance fl/int-rewrite (n y))
     :in-theory (enable mod))))

mod-squeezetheorem

(defthm mod-squeeze
  (implies (and (= (mod m n) 0)
      (< m (* (1+ a) n))
      (< (* (1- a) n) m)
      (integerp a)
      (integerp m)
      (integerp n))
    (= m (* a n)))
  :hints (("Goal" :use (mod-0-int (:theorem (implies (and (< m (* (1+ a) n)) (< (* (1- a) n) m) (rationalp n))
           (and (< (1- a) (/ m n)) (< (/ m n) (1+ a))))))))
  :rule-classes nil)