Filtering...

floor-mod

books/arithmetic-2/floor-mod/floor-mod

Included Books

floor-mod-helper
other
(in-package "ACL2")
local
(local (include-book "floor-mod-helper"))
local
(local (in-theory (disable (:executable-counterpart force))))
fm-y-guardfunction
(defun fm-y-guard
  (y)
  (cond ((atom y) `((real/rationalp ,Y) (not (equal ,Y 0))))
    ((endp (cdr y)) `((real/rationalp ,(CAR Y)) (not (equal ,(CAR Y) 0))))
    (t (list* `(real/rationalp ,(CAR Y))
        `(not (equal ,(CAR Y) 0))
        (fm-y-guard (cdr y))))))
fm-x-guardfunction
(defun fm-x-guard
  (x)
  (cond ((atom x) `((real/rationalp ,X)))
    ((endp (cdr x)) `((real/rationalp ,(CAR X))))
    (t (cons `(real/rationalp ,(CAR X)) (fm-x-guard (cdr x))))))
fm-guardmacro
(defmacro fm-guard
  (x y)
  (cons 'and (append (fm-x-guard x) (fm-y-guard y))))
integerp-modtheorem
(defthm integerp-mod
  (implies (and (integerp x) (integerp y))
    (integerp (mod x y)))
  :rule-classes :type-prescription)
rationalp-modtheorem
(defthm rationalp-mod
  (implies (and (rationalp x) (rationalp y))
    (rationalp (mod x y)))
  :rule-classes :type-prescription)
floor-completiontheorem
(defthm floor-completion
  (implies (or (not (acl2-numberp x)) (not (acl2-numberp y)))
    (equal (floor x y) 0)))
floor-0theorem
(defthm floor-0
  (and (equal (floor x 0) 0) (equal (floor 0 y) 0)))
mod-completiontheorem
(defthm mod-completion
  (and (implies (not (acl2-numberp x)) (equal (mod x y) 0))
    (implies (not (acl2-numberp y)) (equal (mod x y) (fix x)))))
mod-0theorem
(defthm mod-0
  (and (equal (mod 0 y) 0) (equal (mod x 0) (fix x))))
floor-mod-elimtheorem
(defthm floor-mod-elim
  (implies (acl2-numberp x)
    (equal (+ (mod x y) (* y (floor x y))) x))
  :hints (("Goal" :in-theory (disable floor)))
  :rule-classes ((:rewrite) (:elim)))
floor*function
(defun floor*
  (x y)
  (declare (xargs :measure (abs (floor x y))))
  (cond ((not (real/rationalp x)) t)
    ((not (real/rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (1- (floor* (+ x y) y)))
        ((< y x) t)
        (t (1+ (floor* (- x y) y)))))
    (t (cond ((< x 0) (1- (floor* (+ x y) y)))
        ((< x y) t)
        (t (1+ (floor* (- x y) y)))))))
mod*function
(defun mod*
  (x y)
  (declare (xargs :measure (abs (floor x y))))
  (cond ((not (real/rationalp x)) t)
    ((not (real/rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (mod* (+ x y) y))
        ((< y x) t)
        (t (mod* (- x y) y))))
    (t (cond ((< x 0) (mod* (+ x y) y))
        ((< x y) t)
        (t (mod* (- x y) y))))))
ifloor-indtheorem
(defthm ifloor-ind
  t
  :rule-classes ((:induction :pattern (floor x y) :scheme (floor* x y))))
imod-indtheorem
(defthm imod-ind
  t
  :rule-classes ((:induction :pattern (mod x y) :scheme (mod* x y))))
floor-bounds-1theorem
(defthm floor-bounds-1
  (implies (fm-guard x y)
    (and (< (+ (/ x y) -1) (floor x y))
      (<= (floor x y) (/ x y))))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))
    (:forward-chaining :trigger-terms ((floor x y)))))
floor-bounds-2theorem
(defthm floor-bounds-2
  (implies (and (fm-guard x y) (integerp (/ x y)))
    (equal (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))
    (:forward-chaining :trigger-terms ((floor x y)))))
floor-bounds-3theorem
(defthm floor-bounds-3
  (implies (and (fm-guard x y) (not (integerp (/ x y))))
    (< (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))
    (:forward-chaining :trigger-terms ((floor x y)))))
in-theory
(in-theory (disable floor))
mod-bounds-1theorem
(defthm mod-bounds-1
  (implies (and (fm-guard x y) (< 0 y))
    (and (<= 0 (mod x y)) (< (mod x y) y)))
  :rule-classes ((:generalize) (:linear) (:forward-chaining)))
mod-bounds-2theorem
(defthm mod-bounds-2
  (implies (and (fm-guard x y) (< y 0))
    (and (<= (mod x y) 0) (< y (mod x y))))
  :rule-classes ((:generalize) (:linear) (:forward-chaining)))
mod-bounds-3theorem
(defthm mod-bounds-3
  (implies (and (fm-guard x y) (integerp (/ x y)))
    (equal 0 (mod x y)))
  :rule-classes ((:generalize) (:linear) (:forward-chaining)))
in-theory
(in-theory (disable floor mod))
floor-nonnegativetheorem
(defthm floor-nonnegative
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (<= 0 x)
        (<= x 0)))
    (<= 0 (floor x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:type-prescription)))
floor-nonpositivetheorem
(defthm floor-nonpositive
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (<= x 0)
        (<= 0 x)))
    (<= (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:type-prescription)))
floor-positivetheorem
(defthm floor-positive
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (<= y x)
        (<= x y)))
    (< 0 (floor x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (< 0 (floor x y))
          (if (< 0 y)
            (<= y x)
            (<= x y)))))))
floor-negativetheorem
(defthm floor-negative
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (< x 0)
        (< 0 x)))
    (< (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (< (floor x y) 0)
          (if (< 0 y)
            (< x 0)
            (< 0 x)))))))
floor-=-x/ytheorem
(defthm floor-=-x/y
  (implies (and (fm-guard x y) (integerp (/ x y)))
    (equal (floor x y) (/ x y)))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (floor x y) (/ x y)) (integerp (/ x y)))))))
floor-zerotheorem
(defthm floor-zero
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x))))
    (equal (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (floor x y) 0)
          (if (< 0 y)
            (and (<= 0 x) (< x y))
            (and (<= x 0) (< y x))))))))
floor-onetheorem
(defthm floor-one
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (<= y x) (< x (* 2 y)))
        (and (<= x y) (< (* 2 y) x))))
    (equal (floor x y) 1))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (floor x y) 1)
          (if (< 0 y)
            (and (<= y x) (< x (* 2 y)))
            (and (<= x y) (< (* 2 y) x))))))))
floor-minus-onetheorem
(defthm floor-minus-one
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (< x 0) (<= (- x) y))
        (and (< 0 x) (<= y (- x)))))
    (equal (floor x y) -1))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (floor x y) -1)
          (if (< 0 y)
            (and (< x 0) (<= (- x) y))
            (and (< 0 x) (<= y (- x)))))))))
mod-nonnegativetheorem
(defthm mod-nonnegative
  (implies (and (fm-guard x y) (< 0 y)) (<= 0 (mod x y)))
  :rule-classes ((:rewrite) (:type-prescription)))
mod-nonpositivetheorem
(defthm mod-nonpositive
  (implies (and (fm-guard x y) (< y 0)) (<= (mod x y) 0))
  :rule-classes ((:rewrite) (:type-prescription)))
mod-positivetheorem
(defthm mod-positive
  (implies (and (fm-guard x y) (< 0 y) (not (integerp (/ x y))))
    (< 0 (mod x y)))
  :rule-classes ((:rewrite) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (< 0 (mod x y))
          (and (< 0 y) (not (integerp (/ x y)))))))))
mod-negativetheorem
(defthm mod-negative
  (implies (and (fm-guard x y) (< y 0) (not (integerp (/ x y))))
    (< (mod x y) 0))
  :rule-classes ((:rewrite) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (< (mod x y) 0)
          (and (< y 0) (not (integerp (/ x y)))))))))
mod-zerotheorem
(defthm mod-zero
  (implies (and (fm-guard x y) (integerp (/ x y)))
    (equal (mod x y) 0))
  :rule-classes ((:rewrite) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (mod x y) 0) (integerp (/ x y)))))))
mod-x-y-=-xtheorem
(defthm mod-x-y-=-x
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x))))
    (equal (mod x y) x))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)
    (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (mod x y) x)
          (if (< 0 y)
            (and (<= 0 x) (< x y))
            (and (<= x 0) (< y x))))))))
mod-x-y-=-x-+-ytheorem
(defthm mod-x-y-=-x-+-y
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (< x 0) (<= (- x) y))
        (and (< 0 x) (<= y (- x)))))
    (equal (mod x y) (+ x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (mod x y) (+ x y))
          (if (< 0 y)
            (and (< x 0) (<= (- x) y))
            (and (< 0 x) (<= y (- x)))))))))
mod-x-y-=-x---ytheorem
(defthm mod-x-y-=-x---y
  (implies (and (fm-guard x y)
      (if (< 0 y)
        (and (<= y x) (< x (* 2 y)))
        (and (<= x y) (< (* 2 y) x))))
    (equal (mod x y) (- x y)))
  :hints (("Goal" :in-theory (enable mod)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:rewrite :corollary (implies (fm-guard x y)
        (equal (equal (mod x y) (- x y))
          (if (< 0 y)
            (and (<= y x) (< x (* 2 y)))
            (and (<= x y) (< (* 2 y) x))))))))
justify-floor-recursiontheorem
(defthm justify-floor-recursion
  (and (implies (and (real/rationalp x) (< 0 x) (real/rationalp y) (< 1 y))
      (< (floor x y) x))
    (implies (and (real/rationalp x)
        (< x -1)
        (real/rationalp y)
        (<= 2 y))
      (< x (floor x y)))))
rewrite-floor-x*y-z-righttheorem
(defthm rewrite-floor-x*y-z-right
  (implies (fm-guard x (y z))
    (equal (floor (* x y) z) (floor x (/ z y))))
  :hints (("Goal" :by rewrite-floor-x*y-z-rightxxx)))
in-theory
(in-theory (disable rewrite-floor-x*y-z-right))
rewrite-mod-x*y-z-righttheorem
(defthm rewrite-mod-x*y-z-right
  (implies (fm-guard x (y z))
    (equal (mod (* x y) z) (* y (mod x (/ z y)))))
  :hints (("Goal" :by rewrite-mod-x*y-z-rightxxx)))
in-theory
(in-theory (disable rewrite-mod-x*y-z-right))
floor-minustheorem
(defthm floor-minus
  (implies (fm-guard x y)
    (equal (floor (- x) y)
      (if (integerp (* x (/ y)))
        (- (floor x y))
        (+ (- (floor x y)) -1)))))
floor-minus-2theorem
(defthm floor-minus-2
  (implies (fm-guard x y)
    (equal (floor x (- y))
      (if (integerp (* x (/ y)))
        (- (floor x y))
        (+ (- (floor x y)) -1)))))
mod-minustheorem
(defthm mod-minus
  (implies (fm-guard x y)
    (equal (mod (- x) y)
      (if (integerp (/ x y))
        0
        (- y (mod x y)))))
  :hints (("Goal" :in-theory (enable mod))))
mod-minus-2theorem
(defthm mod-minus-2
  (implies (fm-guard x y)
    (equal (mod x (- y))
      (if (integerp (/ x y))
        0
        (- (mod x y) y))))
  :hints (("Goal" :in-theory (enable mod))))
floor-+theorem
(defthm floor-+
  (implies (fm-guard (x y) z)
    (equal (floor (+ x y) z)
      (+ (floor (+ (mod x z) (mod y z)) z)
        (+ (floor x z) (floor y z)))))
  :hints (("Goal" :by floor-plusxxx)))
in-theory
(in-theory (disable floor-+))
mod-+theorem
(defthm mod-+
  (implies (fm-guard (x y) z)
    (equal (mod (+ x y) z) (mod (+ (mod x z) (mod y z)) z)))
  :hints (("Goal" :by mod-plusxxx)))
in-theory
(in-theory (disable mod-+))
rewrite-floor-modtheorem
(defthm rewrite-floor-mod
  (implies (and (equal i (/ y z)) (integerp i) (fm-guard x (y z)))
    (equal (floor (mod x y) z)
      (- (floor x z) (* i (floor x y))))))
rewrite-mod-modtheorem
(defthm rewrite-mod-mod
  (implies (and (equal i (/ y z)) (integerp i) (fm-guard x (y z)))
    (equal (mod (mod x y) z) (mod x z))))
mod-+-cancel-0theorem
(defthm mod-+-cancel-0
  (implies (and (fm-guard (x y) z))
    (equal (equal (mod (+ x y) z) x)
      (and (equal (mod y z) 0) (equal (mod x z) x)))))
floor-cancel-*theorem
(defthm floor-cancel-*
  (implies (and (fm-guard x y) (integerp x))
    (and (equal (floor (* x y) y) x)
      (equal (floor (* y x) y) x))))
floor-cancel-*-2theorem
(defthm floor-cancel-*-2
  (implies (and (fm-guard x (y z)) (integerp z))
    (equal (floor (* x z) (* y z)) (floor x y))))
mod-minustheorem
(defthm mod-minus
  (implies (fm-guard x y)
    (equal (mod (- x) y)
      (if (integerp (/ x y))
        0
        (- y (mod x y)))))
  :hints (("Goal" :in-theory (enable mod))))
simplify-mod-*theorem
(defthm simplify-mod-*
  (implies (fm-guard x (y z))
    (equal (mod (* x y) (* y z)) (* y (mod x z))))
  :hints (("Goal" :in-theory (enable mod))))
cancel-floor-+theorem
(defthm cancel-floor-+
  (implies (and (equal i (/ x z)) (integerp i) (fm-guard (x y) z))
    (and (equal (floor (+ x y) z) (+ i (floor y z)))
      (equal (floor (+ y x) z) (+ i (floor y z))))))
cancel-floor-+-3theorem
(defthm cancel-floor-+-3
  (implies (and (equal i (/ w z)) (integerp i) (fm-guard (w x y) z))
    (equal (floor (+ x y w) z) (+ i (floor (+ x y) z)))))
cancel-mod-+theorem
(defthm cancel-mod-+
  (implies (and (equal i (/ x z)) (integerp i) (fm-guard (x y) z))
    (and (equal (mod (+ x y) z) (mod y z))
      (equal (mod (+ y x) z) (mod y z))))
  :hints (("Goal" :in-theory (enable mod))))
cancel-mod-+-3theorem
(defthm cancel-mod-+-3
  (implies (and (equal i (/ w z)) (integerp i) (fm-guard (w x y) z))
    (equal (mod (+ x y w) z) (mod (+ x y) z)))
  :hints (("Goal" :by cancel-mod-+-3xxx)))
rewrite-floor-modtheorem
(defthm rewrite-floor-mod
  (implies (and (equal i (/ y z)) (integerp i) (fm-guard x (y z)))
    (equal (floor (mod x y) z)
      (- (floor x z) (* i (floor x y))))))
rewrite-mod-modtheorem
(defthm rewrite-mod-mod
  (implies (and (equal i (/ y z)) (integerp i) (fm-guard x (y z)))
    (equal (mod (mod x y) z) (mod x z))))
simplify-mod-+-modtheorem
(defthm simplify-mod-+-mod
  (implies (and (equal i (/ y z)) (integerp i) (fm-guard (w x) (y z)))
    (and (equal (mod (+ w (mod x y)) z) (mod (+ w x) z))
      (equal (mod (+ (mod x y) w) z) (mod (+ w x) z))
      (equal (mod (+ w (- (mod x y))) z) (mod (+ w (- x)) z))
      (equal (mod (+ (mod x y) (- w)) z) (mod (+ x (- w)) z)))))
mod-+-cancel-0theorem
(defthm mod-+-cancel-0
  (implies (and (fm-guard (x y) z))
    (equal (equal (mod (+ x y) z) x)
      (and (equal (mod y z) 0) (equal (mod x z) x))))
  :hints (("Subgoal 5" :expand (mod (+ x y) z))))
floor-floor-integertheorem
(defthm floor-floor-integer
  (implies (and (real/rationalp x)
      (integerp i)
      (integerp j)
      (< 0 i)
      (< 0 j))
    (equal (floor (floor x i) j) (floor x (* i j)))))
mod-twotheorem
(defthm mod-two
  (implies (integerp x)
    (or (equal (mod x 2) 0) (equal (mod x 2) 1)))
  :rule-classes ((:forward-chaining :corollary (implies (integerp x)
       (and (<= 0 (mod x 2)) (< (mod x 2) 2)))
     :trigger-terms ((mod x 2))) (:generalize)))
in-theory
(in-theory (disable floor-+))
in-theory
(in-theory (disable mod-+))