• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
        • Register-Transfer Logic
          • Bit Vectors
          • Logical Operations
          • Basic Arithmetic Functions
            • Modulus
            • Floor and Ceiling
            • Chop
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Basic Arithmetic Functions

Modulus

Modulus

Definitions and Theorems

Theorem: mod-def

(defthm mod-def
  (implies (case-split (acl2-numberp x))
           (equal (mod x y)
                  (- x (* y (fl (/ x y))))))
  :rule-classes nil)

Theorem: mod-0

(defthm mod-0
  (and (equal (mod 0 y) 0)
       (equal (mod x 0) (fix x))))

Theorem: rationalp-mod

(defthm rationalp-mod
  (implies (rationalp x)
           (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

Theorem: integerp-mod

(defthm integerp-mod
  (implies (and (integerp m) (integerp n))
           (integerp (mod m n)))
  :rule-classes (:rewrite :type-prescription))

Theorem: natp-mod

(defthm natp-mod
  (implies (and (natp m) (natp n))
           (natp (mod m n)))
  :rule-classes ((:type-prescription :typed-term (mod m n))))

Theorem: natp-mod-2

(defthm natp-mod-2
  (implies (and (integerp m) (integerp n) (> n 0))
           (natp (mod m n)))
  :rule-classes ((:type-prescription :typed-term (mod m n))))

Theorem: mod-bnd-1

(defthm 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)

Theorem: mod-by-1

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

Theorem: mod-bnd-2

(defthm mod-bnd-2
  (implies (and (<= 0 m)
                (case-split (rationalp m)))
           (<= (mod m n) m))
  :rule-classes :linear)

Theorem: mod-does-nothing

(defthm mod-does-nothing
  (implies (and (< m n)
                (<= 0 m)
                (case-split (rationalp m)))
           (equal (mod m n) m)))

Theorem: mod-0-fl

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

Theorem: mod-0-int

(defthm mod-0-int
  (implies (and (integerp m)
                (integerp n)
                (not (= n 0)))
           (iff (= (mod m n) 0)
                (integerp (/ m n))))
  :rule-classes nil)

Theorem: mod-mult-n

(defthm mod-mult-n
  (equal (mod (* a n) n) (* n (mod a 1))))

Theorem: mod-mult-n-alt

(defthm mod-mult-n-alt
  (equal (mod (* n a) n) (* n (mod a 1))))

Theorem: mod-squeeze

(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)))
  :rule-classes nil)

Theorem: mod-must-be-n

(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)

Theorem: fl-mod

(defthm fl-mod
  (implies (not (zp m))
           (equal (fl (/ (mod a (* m n)) n))
                  (mod (fl (/ a n)) m))))

Theorem: mod-0-0

(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)

Theorem: mod-equal-int

(defthm mod-equal-int
  (implies (and (= (mod a n) (mod b n))
                (rationalp a)
                (rationalp b))
           (integerp (/ (- a b) n)))
  :rule-classes nil)

Theorem: mod-equal-int-reverse

(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)

Theorem: mod-force-equal

(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)

Function: congruent

(defun congruent (a b n)
  (declare (xargs :guard (and (real/rationalp a)
                              (real/rationalp b)
                              (real/rationalp n)
                              (not (= n 0)))))
  (equal (mod a n) (mod b n)))

Theorem: mod-mult

(defthm mod-mult
  (implies (and (integerp a)
                (rationalp m)
                (rationalp n))
           (equal (mod (+ m (* a n)) n)
                  (mod m n))))

Theorem: mod-force

(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)

Theorem: mod-bnd-3

(defthm 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)

Theorem: mod-sum

(defthm mod-sum
  (implies (and (rationalp a) (rationalp b))
           (equal (mod (+ a (mod b n)) n)
                  (mod (+ a b) n))))

Theorem: mod-diff

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

Theorem: mod-of-mod

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

Theorem: mod-of-mod-cor

(defthm mod-of-mod-cor
  (implies (and (<= b a)
                (case-split (integerp b))
                (case-split (integerp a)))
           (equal (mod (mod x (expt 2 a)) (expt 2 b))
                  (mod x (expt 2 b)))))

Theorem: mod-prod

(defthm mod-prod
  (implies (and (rationalp m)
                (rationalp n)
                (rationalp k))
           (equal (mod (* k m) (* k n))
                  (* k (mod m n)))))

Theorem: mod-mod-times

(defthm mod-mod-times
  (implies (and (integerp a)
                (integerp b)
                (integerp n)
                (> n 0))
           (= (mod (* (mod a n) b) n)
              (mod (* a b) n)))
  :rule-classes nil)

Theorem: mod-plus-mod-iff

(defthm mod-plus-mod-iff
  (implies (and (integerp a)
                (integerp b)
                (integerp c)
                (not (zp n)))
           (iff (= (mod a n) (mod b n))
                (= (mod (+ a c) n) (mod (+ b c) n))))
  :rule-classes nil)

Theorem: mod-times-mod

(defthm mod-times-mod
  (implies (and (integerp a)
                (integerp b)
                (integerp c)
                (not (zp n))
                (= (mod a n) (mod b n)))
           (= (mod (* a c) n) (mod (* b c) n)))
  :rule-classes nil)

Theorem: mod012

(defthm mod012
  (implies (integerp m)
           (or (equal (mod m 2) 0)
               (equal (mod m 2) 1)))
  :rule-classes nil)

Theorem: mod-plus-mod-2

(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)

Theorem: mod-mod-2-not-equal

(defthm mod-mod-2-not-equal
  (implies (acl2-numberp m)
           (not (= (mod m 2) (mod (1+ m) 2))))
  :rule-classes nil)

Theorem: mod-2*m+1-rewrite

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

Theorem: mod-neg

(defthm mod-neg
  (implies (and (posp n) (integerp m))
           (equal (mod (- m) n)
                  (- (1- n) (mod (1- m) n)))))