floor-mod - ACL2 Book

Included Books

other

(in-package "ACL2")

other

(table acl2-defaults-table :state-ok t)

include-book

(include-book "../bind-free/top")

other

(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
     hist
     pspv)))

include-book

(include-book "../bind-free/building-blocks")

rationalp-guard-fnfunction

(defun rationalp-guard-fn
  (args)
  (if (endp (cdr args))
    `((rationalp ,(CAR ARGS)))
    (cons `(rationalp ,(CAR ARGS))
      (rationalp-guard-fn (cdr args)))))

rationalp-guardmacro

(defmacro rationalp-guard
  (&rest args)
  (if (endp (cdr args))
    `(rationalp ,(CAR ARGS))
    (cons 'and (rationalp-guard-fn args))))

local

(local (defthm niq-bounds
    (implies (and (integerp i) (<= 0 i) (integerp j) (< 0 j))
      (and (<= (nonnegative-integer-quotient i j) (/ i j))
        (< (+ (/ i j) -1) (nonnegative-integer-quotient i j))))
    :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))))

truncate-to-floortheorem

(defthm truncate-to-floor
  (implies (and (rationalp x) (rationalp y))
    (equal (truncate x y)
      (cond ((integerp (/ x y)) (/ x y))
        ((and (< 0 x) (< 0 y)) (floor x y))
        ((and (< x 0) (< y 0)) (floor x y))
        (t (+ 1 (floor x y))))))
  :hints (("Goal" :in-theory (e/d (floor) (nonnegative-integer-quotient)))))

rem-to-modtheorem

(defthm rem-to-mod
  (implies (and (rationalp x) (rationalp y))
    (equal (rem x y)
      (cond ((integerp (/ x y)) (if (equal y 0)
            x
            0))
        ((and (< 0 x) (< 0 y)) (mod x y))
        ((and (< x 0) (< y 0)) (mod x y))
        (t (- (mod x y) y)))))
  :hints (("Goal" :in-theory (e/d (mod) (truncate)))))

ceiling-to-floortheorem

(defthm ceiling-to-floor
  (implies (and (rationalp x) (rationalp y))
    (equal (ceiling x y)
      (if (integerp (/ x y))
        (/ x y)
        (+ 1 (floor x y)))))
  :hints (("Goal" :in-theory (e/d (floor) (nonnegative-integer-quotient)))))

round-to-floortheorem

(defthm round-to-floor
  (implies (and (rationalp x) (rationalp y))
    (equal (round x y)
      (cond ((< (mod (/ x y) 1) 1/2) (floor x y))
        ((< 1/2 (mod (/ x y) 1)) (+ 1 (floor x y)))
        (t (if (evenp (floor x y))
            (floor x y)
            (+ 1 (floor x y)))))))
  :hints (("Goal" :in-theory (e/d (floor mod) (nonnegative-integer-quotient)))))

ash-to-floortheorem

(defthmd ash-to-floor
  (implies (and (rationalp i) (rationalp n))
    (equal (ash i n)
      (cond ((and (integerp i) (integerp n)) (floor i (expt 2 (- n))))
        ((integerp i) (floor i 1))
        (t 0))))
  :hints (("Goal" :in-theory (e/d (floor) (nonnegative-integer-quotient)))))

in-theory

(in-theory (disable truncate rem ceiling round))

integerp-modtheorem

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

rationalp-modtheorem

(defthm rationalp-mod
  (implies (and (rationalp x)) (rationalp (mod x y)))
  :hints (("Goal" :cases ((rationalp y))))
  :rule-classes (:rewrite :type-prescription))

floor-completiontheorem

(defthm floor-completion
  (implies (or (not (acl2-numberp x)) (not (acl2-numberp y)))
    (equal (floor x y) 0)))

local

(local (defthm floor-0-local
    (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)))))

local

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

local

(local (defthm floor-x-1-local
    (implies (integerp x) (equal (floor x 1) x))))

local

(local (defthm mod-x-1-local
    (implies (integerp x) (equal (mod x 1) 0))))

floor-mod-elim-weaktheorem

(defthm floor-mod-elim-weak
  (implies (rationalp-guard x y)
    (equal (+ (mod x y) (* y (floor x y))) x))
  :hints (("Goal" :in-theory (disable floor)))
  :rule-classes ((:rewrite) (:elim)))

floor-induct-fnfunction

(defun floor-induct-fn
  (x y)
  (declare (xargs :measure (abs (floor x y))))
  (cond ((not (rationalp x)) t)
    ((not (rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (1- (floor-induct-fn (+ x y) y)))
        ((< y x) t)
        (t (1+ (floor-induct-fn (- x y) y)))))
    (t (cond ((< x 0) (1- (floor-induct-fn (+ x y) y)))
        ((< x y) t)
        (t (1+ (floor-induct-fn (- x y) y)))))))

mod-induct-fnfunction

(defun mod-induct-fn
  (x y)
  (declare (xargs :measure (abs (floor x y))))
  (cond ((not (rationalp x)) t)
    ((not (rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (mod-induct-fn (+ x y) y))
        ((< y x) t)
        (t (mod-induct-fn (- x y) y))))
    (t (cond ((< x 0) (mod-induct-fn (+ x y) y))
        ((< x y) t)
        (t (mod-induct-fn (- x y) y))))))

floor-indtheorem

(defthm floor-ind
  t
  :rule-classes ((:induction :pattern (floor x y)
     :scheme (floor-induct-fn x y))))

mod-indtheorem

(defthm mod-ind
  t
  :rule-classes ((:induction :pattern (mod x y) :scheme (mod-induct-fn x y))))

in-theory

(in-theory (disable floor-ind mod-ind))

floor-bounds-1theorem

(defthm floor-bounds-1
  (implies (rationalp-guard x y)
    (and (< (+ (/ x y) -1) (floor x y))
      (<= (floor x y) (/ x y))))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

floor-bounds-2theorem

(defthm floor-bounds-2
  (implies (and (rationalp-guard x y) (integerp (/ x y)))
    (equal (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

floor-bounds-3theorem

(defthm floor-bounds-3
  (implies (and (rationalp-guard x y) (not (integerp (/ x y))))
    (< (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

mod-bounds-1theorem

(defthm mod-bounds-1
  (implies (and (rationalp-guard x y) (< 0 y))
    (and (<= 0 (mod x y)) (< (mod x y) y)))
  :rule-classes ((:generalize) (:linear)))

mod-bounds-2theorem

(defthm mod-bounds-2
  (implies (and (rationalp-guard x y) (< y 0))
    (and (<= (mod x y) 0) (< y (mod x y))))
  :rule-classes ((:generalize) (:linear)))

mod-bounds-3theorem

(defthm mod-bounds-3
  (implies (and (rationalp-guard x y)
      (not (equal y 0))
      (integerp (/ x y)))
    (equal 0 (mod x y)))
  :rule-classes ((:generalize) (:linear)))

other

(deftheory floor-bounds
  '((:linear floor-bounds-1) (:linear floor-bounds-2)
    (:linear floor-bounds-1)))

other

(deftheory mod-bounds
  '((:linear mod-bounds-1) (:linear mod-bounds-2)
    (:linear mod-bounds-3)))

other

(deftheory floor-mod-bounds
  '((:linear floor-bounds-1) (:linear floor-bounds-2)
    (:linear floor-bounds-1)
    (:linear mod-bounds-1)
    (:linear mod-bounds-2)
    (:linear mod-bounds-3)))

in-theory

(in-theory (disable floor mod))

floor-nonnegative-1theorem

(defthm floor-nonnegative-1
  (implies (and (rationalp-guard x y) (<= 0 y) (<= 0 x))
    (<= 0 (floor x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

floor-nonnegative-2theorem

(defthm floor-nonnegative-2
  (implies (and (rationalp-guard x y) (<= y 0) (<= x 0))
    (<= 0 (floor x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

floor-nonpositive-1theorem

(defthm floor-nonpositive-1
  (implies (and (rationalp-guard x y) (<= 0 y) (<= x 0))
    (<= (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

floor-nonpositive-2theorem

(defthm floor-nonpositive-2
  (implies (and (rationalp-guard x y) (<= y 0) (<= 0 x))
    (<= (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

floor-positivetheorem

(defthm floor-positive
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (< 0 (floor x y))
      (or (and (< 0 y) (<= y x)) (and (< y 0) (<= x y)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y) (< 0 y) (<= y x))
        (< 0 (floor x y))))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (< y 0) (<= x y))
        (< 0 (floor x y))))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< 0 y)
          (<= y x))
        (< 0 (floor x y))))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< y 0)
          (<= x y))
        (< 0 (floor x y))))))

floor-negativetheorem

(defthm floor-negative
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (< (floor x y) 0)
      (or (and (< 0 x) (< y 0)) (and (< x 0) (< 0 y)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y) (< 0 x) (< y 0))
        (< (floor x y) 0)))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (< x 0) (< 0 y))
        (< (floor x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< 0 x)
          (< y 0))
        (< (floor x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< x 0)
          (< 0 y))
        (< (floor x y) 0)))))

floor-zerotheorem

(defthm floor-zero
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (equal (floor x y) 0)
      (or (equal y 0)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y) (equal y 0))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (<= 0 x) (< x y))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (<= x 0) (< y x))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (equal y 0))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (<= 0 x) (< x y))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (<= x 0) (< y x))
        (equal (floor x y) 0)))))

floor-=-x/y-1theorem

(defthm floor-=-x/y-1
  (implies (rationalp-guard x y)
    (equal (equal (floor x y) (* x (/ y))) (integerp (/ x y)))))

floor-=-x/y-2theorem

(defthm floor-=-x/y-2
  (implies (rationalp-guard x y)
    (equal (equal (floor x y) (* (/ y) x)) (integerp (/ x y)))))

mod-nonnegativetheorem

(defthm mod-nonnegative
  (implies (and (rationalp-guard x y) (< 0 y))
    (<= 0 (mod x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

mod-nonpositivetheorem

(defthm mod-nonpositive
  (implies (and (rationalp-guard x y) (< y 0))
    (<= (mod x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))

mod-positivetheorem

(defthm mod-positive
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (< 0 (mod x y))
      (or (and (equal y 0) (< 0 x))
        (and (< 0 y) (not (integerp (/ x y)))))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y) (equal y 0) (< 0 x))
        (< 0 (mod x y))))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (< 0 y) (not (integerp (/ x y))))
        (< 0 (mod x y))))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (equal y 0)
          (< 0 x))
        (< 0 (mod x y))))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< 0 y)
          (not (integerp (/ x y))))
        (< 0 (mod x y))))))

mod-negativetheorem

(defthm mod-negative
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (< (mod x y) 0)
      (or (and (equal y 0) (< x 0))
        (and (< y 0) (not (integerp (/ x y)))))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y) (equal y 0) (< x 0))
        (< (mod x y) 0)))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (< y 0) (not (integerp (/ x y))))
        (< (mod x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (equal y 0)
          (< x 0))
        (< (mod x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (< y 0)
          (not (integerp (/ x y))))
        (< (mod x y) 0)))))

mod-zerotheorem

(defthm mod-zero
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (equal (mod x y) 0)
      (or (equal x 0) (and (not (equal y 0)) (integerp (/ x y))))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp-guard x y)
          (not (equal y 0))
          (integerp (/ x y)))
        (equal (mod x y) 0)))
    (:type-prescription :corollary (implies (and (rationalp-guard x y) (equal x 0))
        (equal (mod x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y)
          (not (equal y 0))
          (integerp (/ x y)))
        (equal (mod x y) 0)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (equal x 0))
        (equal (mod x y) 0)))))

mod-x-y-=-xtheorem

(defthm mod-x-y-=-x
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp-guard x y))
    (equal (equal (mod x y) x)
      (or (equal y 0)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (rationalp-guard x y)
          (equal y 0))
        (equal (mod x y) x)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (<= 0 x) (< x y))
        (equal (mod x y) x)))
    (:rewrite :backchain-limit-lst 1
      :corollary (implies (and (rationalp-guard x y) (<= x 0) (< y x))
        (equal (mod x y) x)))))

justify-floor-recursiontheorem

(defthm justify-floor-recursion
  (and (implies (and (integerp x) (< 0 x) (integerp y) (< 1 y))
      (< (floor x y) x))
    (implies (and (integerp x) (< x -1) (integerp y) (<= 2 y))
      (< x (floor x y)))))

floor-+-weaktheorem

(defthmd floor-+-weak
  (implies (and (rationalp-guard x y z)
      (syntaxp (not (equal (fn-symb x) 'mod)))
      (syntaxp (not (equal (fn-symb x) 'mod))))
    (equal (floor (+ x y) z)
      (+ (floor (+ (mod x z) (mod y z)) z)
        (+ (floor x z) (floor y z))))))

mod-+-weaktheorem

(defthmd mod-+-weak
  (implies (and (rationalp-guard x y z)
      (syntaxp (not (equal (fn-symb x) 'mod)))
      (syntaxp (not (equal (fn-symb x) 'mod))))
    (equal (mod (+ x y) z) (mod (+ (mod x z) (mod y z)) z)))
  :hints (("Goal" :in-theory (enable mod))))

rewrite-floor-x*y-z-right-weaktheorem

(defthmd rewrite-floor-x*y-z-right-weak
  (implies (rationalp-guard x y z)
    (equal (floor (* x y) z) (floor x (/ z y)))))

rewrite-mod-x*y-z-righttheorem

(defthmd rewrite-mod-x*y-z-right
  (implies (rationalp-guard x y z)
    (equal (mod (* x y) z) (* y (mod x (/ z y)))))
  :hints (("Goal" :in-theory (enable mod))))

floor-minus-weaktheorem

(defthm floor-minus-weak
  (implies (and (rationalp-guard x y) (syntaxp (negative-addends-p x)))
    (equal (floor x y)
      (if (integerp (* x (/ y)))
        (- (floor (- x) y))
        (+ (- (floor (- x) y)) -1)))))

floor-minus-2theorem

(defthm floor-minus-2
  (implies (and (rationalp-guard x y) (syntaxp (negative-addends-p y)))
    (equal (floor x y)
      (if (integerp (* x (/ y)))
        (- (floor x (- y)))
        (+ (- (floor x (- y))) -1)))))

mod-negtheorem

(defthm mod-neg
  (implies (and (rationalp-guard x y) (syntaxp (negative-addends-p x)))
    (equal (mod x y)
      (if (and (not (equal y 0)) (integerp (/ x y)))
        0
        (- y (mod (- x) y)))))
  :hints (("Goal" :in-theory (enable mod))))

mod-minus-2theorem

(defthm mod-minus-2
  (implies (and (rationalp-guard x y) (syntaxp (negative-addends-p y)))
    (equal (mod x y)
      (if (and (not (equal y 0)) (integerp (/ x y)))
        0
        (- (mod x (- y)) (- y)))))
  :hints (("Goal" :in-theory (enable mod))))

rewrite-floor-mod-weaktheorem

(defthm rewrite-floor-mod-weak
  (implies (and (rationalp-guard x y z) (equal i (/ y z)) (integerp i))
    (equal (floor (mod x y) z)
      (- (floor x z) (* i (floor x y))))))

rewrite-mod-mod-weaktheorem

(defthm rewrite-mod-mod-weak
  (implies (and (rationalp-guard x y z)
      (not (equal z 0))
      (equal i (/ y z))
      (integerp i))
    (equal (mod (mod x y) z) (mod x z)))
  :hints (("Goal" :in-theory (enable mod-+-weak)
     :cases ((equal (floor x y) 0)))))

mod-+-cancel-0-fn-1function

(defun mod-+-cancel-0-fn-1
  (x z)
  (declare (xargs :guard (and (pseudo-termp x) (eq (fn-symb x) 'binary-+))))
  (cond ((equal (fargn x 1) z) t)
    ((eq (fn-symb (fargn x 2)) 'binary-+) (mod-+-cancel-0-fn-1 (fargn x 2) z))
    ((equal (fargn x 2) z) t)
    (t nil)))

mod-+-cancel-0-fnfunction

(defun mod-+-cancel-0-fn
  (x z)
  (declare (xargs :guard (pseudo-termp x)))
  (if (and (eq (fn-symb x) 'binary-+)
      (not (eq (fn-symb z) 'binary-+)))
    (mod-+-cancel-0-fn-1 x z)
    nil))

local

(local (defthm local-mod-+-cancel-0
    (implies (rationalp-guard x y z)
      (equal (equal (mod (+ x y) z) x)
        (and (equal (mod y z) 0) (equal (mod x z) x))))
    :hints (("Goal" :cases ((< 0 z) (< z 0) (equal z 0))) ("Subgoal 3.10" :in-theory (enable mod))
      ("Subgoal 3.4" :in-theory (enable mod-+-weak))
      ("Subgoal 2.5" :in-theory (enable mod))
      ("Subgoal 2.2" :in-theory (enable mod-+-weak)))
    :rule-classes nil))

mod-+-cancel-0-weaktheorem

(defthm mod-+-cancel-0-weak
  (implies (and (rationalp-guard x y z)
      (syntaxp (mod-+-cancel-0-fn x z)))
    (equal (equal (mod x y) z)
      (and (equal (mod (- x z) y) 0) (equal (mod z y) z))))
  :hints (("Goal" :use ((:instance local-mod-+-cancel-0 (x z) (z y) (y (- x z)))))))

factors-cccfunction

(defun factors-ccc
  (product)
  (declare (xargs :guard (pseudo-termp product)))
  (if (eq (fn-symb product) 'binary-*)
    (cons (fargn product 1) (factors-ccc (fargn product 2)))
    (list product)))

non-zero-intersection-equalfunction

(defun non-zero-intersection-equal
  (x y mfc state)
  (declare (xargs :guard (and (pseudo-term-listp x) (pseudo-term-listp y))))
  (cond ((endp x) nil)
    ((and (member-equal (car x) y)
       (proveably-non-zero-rational (car x) mfc state)) (cons (car x)
        (non-zero-intersection-equal (cdr x) y mfc state)))
    (t (non-zero-intersection-equal (cdr x) y mfc state))))

make-product-cccfunction

(defun make-product-ccc
  (factors)
  (declare (xargs :guard (true-listp factors)))
  (cond ((null factors) ''1)
    ((null (cdr factors)) (car factors))
    ((null (cddr factors)) (list 'binary-* (car factors) (cadr factors)))
    (t (list 'binary-*
        (car factors)
        (make-product-ccc (cdr factors))))))

find-common-factorsfunction

(defun find-common-factors
  (x y mfc state)
  (declare (xargs :guard (and (pseudo-termp x) (pseudo-termp y))))
  (let* ((x-factors (factors-ccc x)) (y-factors (factors-ccc y))
      (common-factors (non-zero-intersection-equal x-factors y-factors mfc state)))
    (if common-factors
      (list (cons 'common-factors (make-product-ccc common-factors)))
      nil)))

floor-cancel-*-weaktheorem

(defthm floor-cancel-*-weak
  (implies (and (rationalp-guard x y)
      (bind-free (find-common-factors x y mfc state)
        (common-factors))
      (rationalp common-factors)
      (not (equal common-factors 0)))
    (equal (floor x y)
      (floor (* x (/ common-factors)) (* y (/ common-factors))))))

mod-cancel-*theorem

(defthm mod-cancel-*
  (implies (and (rationalp-guard x y)
      (bind-free (find-common-factors x y mfc state)
        (common-factors))
      (rationalp common-factors)
      (not (equal common-factors 0)))
    (equal (mod x y)
      (* common-factors
        (mod (* x (/ common-factors)) (* y (/ common-factors))))))
  :hints (("Goal" :in-theory (enable mod))))

find-cancelling-addendsfunction

(defun find-cancelling-addends
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (cond ((proveably-integer `(binary-* ,(FARGN X 1) (unary-/ ,Y))
           mfc
           state) (list (cons 'addend (fargn x 1))))
        ((eq (fn-symb (fargn x 2)) 'binary-+) (find-cancelling-addends (fargn x 2) y mfc state))
        ((proveably-integer `(binary-* ,(FARGN X 2) (unary-/ ,Y))
           mfc
           state) (list (cons 'addend (fargn x 2))))
        (t nil)))
    ((proveably-integer `(binary-* ,X (unary-/ ,Y)) mfc state) (list (cons 'addend x)))
    (t nil)))

cancel-floor-+theorem

(defthm cancel-floor-+
  (implies (and (bind-free (find-cancelling-addends x y mfc state) (addend))
      (rationalp-guard x y addend)
      (equal i (/ addend y))
      (integerp i))
    (equal (floor x y) (+ i (floor (- x addend) y)))))

cancel-mod-+theorem

(defthm cancel-mod-+
  (implies (and (not (equal y 0))
      (bind-free (find-cancelling-addends x y mfc state) (addend))
      (rationalp-guard x y addend)
      (equal i (/ addend y))
      (integerp i))
    (equal (mod x y) (mod (- x addend) y))))

simplify-mod-+-mod-fnfunction

(defun simplify-mod-+-mod-fn
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
        (cond ((and (eq (fn-symb arg1) 'mod)
             (proveably-integer `(binary-* ,(FARGN ARG1 2) (unary-/ ,Y))
               mfc
               state)) (list (cons 'w (fargn arg1 1)) (cons 'z (fargn arg1 2))))
          ((eq (fn-symb arg2) 'binary-+) (simplify-mod-+-mod-fn arg2 y mfc state))
          ((and (eq (fn-symb arg2) 'mod)
             (proveably-integer `(binary-* ,(FARGN ARG2 2) (unary-/ ,Y))
               mfc
               state)) (list (cons 'w (fargn arg2 1)) (cons 'z (fargn arg2 2))))
          (t nil))))
    ((and (eq (fn-symb x) 'mod)
       (proveably-integer `(binary-* ,(FARGN X 2) (unary-/ ,Y))
         mfc
         state)) (list (cons 'w (fargn x 1)) (cons 'z (fargn x 2))))
    (t nil)))

simplify-mod-+-mod-weaktheorem

(defthm simplify-mod-+-mod-weak
  (implies (and (not (equal y 0))
      (bind-free (simplify-mod-+-mod-fn x y mfc state) (w z))
      (rationalp-guard w x y z)
      (integerp (/ z y)))
    (equal (mod x y) (mod (+ x w (- (mod w z))) y))))

simplify-mod-+-minus-mod-fnfunction

(defun simplify-mod-+-minus-mod-fn
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
        (cond ((and (eq (fn-symb arg1) 'unary--)
             (eq (fn-symb (fargn arg1 1)) 'mod)
             (proveably-integer `(binary-* ,(FARGN (FARGN ARG1 1) 2) (unary-/ ,Y))
               mfc
               state)) (list (cons 'w (fargn (fargn arg1 1) 1))
              (cons 'z (fargn (fargn arg1 1) 2))))
          ((eq (fn-symb arg2) 'binary-+) (simplify-mod-+-minus-mod-fn arg2 y mfc state))
          ((and (eq (fn-symb arg2) 'unary--)
             (eq (fn-symb (fargn arg2 1)) 'mod)
             (proveably-integer `(binary-* ,(FARGN (FARGN ARG2 1) 2) (unary-/ ,Y))
               mfc
               state)) (list (cons 'w (fargn (fargn arg2 1) 1))
              (cons 'z (fargn (fargn arg2 1) 2))))
          (t nil))))
    ((and (eq (fn-symb x) 'unary--)
       (eq (fn-symb (fargn x 1)) 'mod)
       (proveably-integer `(binary-* ,(FARGN (FARGN X 1) 2) (unary-/ ,Y))
         mfc
         state)) (list (cons 'w (fargn (fargn x 1) 1))
        (cons 'z (fargn (fargn x 1) 2))))
    (t nil)))

simplify-mod-+-minus-modtheorem

(defthm simplify-mod-+-minus-mod
  (implies (and (not (equal y 0))
      (bind-free (simplify-mod-+-minus-mod-fn x y mfc state)
        (w z))
      (rationalp-guard w x y z)
      (integerp (/ z y)))
    (equal (mod x y) (mod (+ x (- w) (mod w z)) y))))

local

(local (defthm floor-0-local-2 (equal (floor 0 x) 0)))

floor-floor-integer-alttheorem

(defthm floor-floor-integer-alt
  (implies (and (rationalp x) (integerp i) (integerp j) (<= 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)))

floor-0theorem

(defthm floor-0
  (and (equal (floor x 0) 0) (equal (floor 0 y) 0)))

mod-0theorem

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

floor-x-1theorem

(defthm floor-x-1
  (implies (integerp x) (equal (floor x 1) x)))

mod-x-1theorem

(defthm mod-x-1 (implies (integerp x) (equal (mod x 1) 0)))