floor - ACL2 Book

Included Books

numerator denominator times plus minus divide times-and-divide nonnegative-integer-quotient integerp equal-of-booleans quotient-remainder-lemmas inequalities

other

(in-package "ACL2")

local

(local (include-book "numerator"))

local

(local (include-book "denominator"))

local

(local (include-book "times"))

local

(local (include-book "plus"))

local

(local (include-book "minus"))

local

(local (include-book "divide"))

local

(local (include-book "times-and-divide"))

local

(local (include-book "nonnegative-integer-quotient"))

local

(local (include-book "integerp"))

local

(local (include-book "kestrel/utilities/equal-of-booleans" :dir :system))

local

(local (defthm floor-bound-hack-eric
    (implies (and (<= 1 j) (<= 0 i) (rationalp i) (rationalp j))
      (<= (* i (/ j)) i))))

<-of-numerator-and-denominator-sametheorem

(defthm <-of-numerator-and-denominator-same
  (implies (rationalp x)
    (equal (< (numerator x) (denominator x))
      (if (<= x 0)
        t
        (< x 1))))
  :hints (("Goal" :use rational-implies2
     :in-theory (disable rational-implies2))))

<-of---of-numerator-and-denominator-sametheorem

(defthm <-of---of-numerator-and-denominator-same
  (implies (rationalp x)
    (equal (< (- (numerator x)) (denominator x))
      (or (<= 0 x) (< -1 x))))
  :hints (("Goal" :use (:instance <-of-numerator-and-denominator-same (x (- x)))
     :in-theory (disable <-of-numerator-and-denominator-same))))

in-theory

(in-theory (disable floor))

floor-of-0-arg1theorem

(defthm floor-of-0-arg1
  (equal (floor 0 j) 0)
  :hints (("Goal" :in-theory (enable floor))))

floor-of-0-arg2theorem

(defthm floor-of-0-arg2
  (equal (floor i 0) 0)
  :hints (("Goal" :in-theory (enable floor))))

floor-of-1-when-integerptheorem

(defthm floor-of-1-when-integerp
  (implies (integerp i) (equal (floor i 1) i))
  :hints (("Goal" :in-theory (enable floor))))

floor-selftheorem

(defthm floor-self
  (equal (floor i i)
    (if (equal (fix i) 0)
      0
      1))
  :hints (("Goal" :in-theory (enable floor) :cases ((acl2-numberp i)))))

floor-normalize-denominatortheorem

(defthmd floor-normalize-denominator
  (implies (syntaxp (not (equal j ''1)))
    (equal (floor i j) (floor (/ i j) 1)))
  :hints (("Goal" :in-theory (enable floor))))

floor-weak-monotonetheorem

(defthm floor-weak-monotone
  (implies (and (<= i1 i2)
      (<= 0 j)
      (rationalp i1)
      (rationalp i2)
      (rationalp j))
    (<= (floor i1 j) (floor i2 j)))
  :hints (("Goal" :in-theory (e/d (floor <=-of-*-and-*-same-linear)
       (nonnegative-integer-quotient-lower-bound-linear2))
     :cases ((rationalp i2))
     :use ((:instance nonnegative-integer-quotient-lower-bound-linear2
        (i (numerator (* i2 (/ j))))
        (j (denominator (* i2 (/ j))))) (:instance nonnegative-integer-quotient-lower-bound-linear2
         (i (- (numerator (* i1 (/ j)))))
         (j (denominator (* i1 (/ j)))))))))

floor-weak-monotone-linear-1theorem

(defthm floor-weak-monotone-linear-1
  (implies (and (<= free i)
      (<= 0 j)
      (rationalp free)
      (rationalp i)
      (rationalp j))
    (<= (floor free j) (floor i j)))
  :rule-classes ((:linear :trigger-terms ((floor i j)))))

floor-weak-monotone-linear=-2theorem

(defthm floor-weak-monotone-linear=-2
  (implies (and (<= i free)
      (<= 0 j)
      (rationalp free)
      (rationalp i)
      (rationalp j))
    (<= (floor i j) (floor free j)))
  :rule-classes ((:linear :trigger-terms ((floor i j)))))

floor-when-multipletheorem

(defthmd floor-when-multiple
  (implies (integerp (* i (/ j))) (equal (floor i j) (/ i j)))
  :hints (("Goal" :in-theory (enable floor))))

floor-uniquetheorem

(defthmd floor-unique
  (implies (and (integerp n)
      (<= n (/ i j))
      (< (+ -1 (/ i j)) n)
      (< 0 j)
      (rationalp i)
      (rationalp j))
    (equal (floor i j) n))
  :hints (("Goal" :in-theory (enable floor))))

floor-unique-equal-versiontheorem

(defthm floor-unique-equal-version
  (implies (and (<= n (/ i j))
      (< (+ -1 (/ i j)) n)
      (< 0 j)
      (rationalp i)
      (rationalp j))
    (equal (equal (floor i j) n) (integerp n)))
  :hints (("Goal" :use floor-unique :in-theory (disable floor-unique))))

my-floor-lower-boundtheorem

(defthmd my-floor-lower-bound
  (implies (and (rationalp i) (rationalp j) (not (equal 0 j)))
    (< (+ -1 (/ i j)) (floor i j)))
  :hints (("Goal" :in-theory (e/d (floor) (<-of-*-of-/-arg1)))))

my-floor-lower-bound-lineartheorem

(defthm my-floor-lower-bound-linear
  (implies (and (not (equal 0 j)) (rationalp i) (rationalp j))
    (< (+ -1 (/ i j)) (floor i j)))
  :rule-classes ((:linear :trigger-terms ((floor i j))))
  :hints (("Goal" :by my-floor-lower-bound)))

my-floor-lower-bound-alttheorem

(defthm my-floor-lower-bound-alt
  (implies (and (< 0 j) (rationalp i) (rationalp j))
    (< i (+ j (* j (floor i j)))))
  :hints (("Goal" :use ((:instance my-floor-lower-bound) (:instance <-of-*-and-*-cancel
         (x1 (+ -1 (* i (/ j))))
         (x2 (floor i j))
         (y j)))
     :in-theory (disable my-floor-lower-bound <-of-*-and-*-cancel))))

my-floor-lower-bound-alt-lineartheorem

(defthm my-floor-lower-bound-alt-linear
  (implies (and (< 0 j) (rationalp i) (rationalp j))
    (< i (+ j (* j (floor i j)))))
  :rule-classes ((:linear :trigger-terms ((* j (floor i j)))))
  :hints (("Goal" :by my-floor-lower-bound-alt)))

my-floor-lower-bound-alt-negtheorem

(defthm my-floor-lower-bound-alt-neg
  (implies (and (< j 0) (rationalp i) (rationalp j))
    (< (+ j (* j (floor i j))) i))
  :hints (("Goal" :use ((:instance my-floor-lower-bound) (:instance <-of-*-and-*-cancel
         (x1 (+ -1 (* i (/ j))))
         (x2 (floor i j))
         (y j)))
     :in-theory (disable my-floor-lower-bound <-of-*-and-*-cancel))))

my-floor-lower-bound-alt-neg-lineartheorem

(defthm my-floor-lower-bound-alt-neg-linear
  (implies (and (< j 0) (rationalp i) (rationalp j))
    (< (+ j (* j (floor i j))) i))
  :rule-classes :linear)

my-floor-upper-boundtheorem

(defthmd my-floor-upper-bound
  (implies (and (rationalp i) (rationalp j))
    (<= (floor i j) (* i (/ j))))
  :hints (("Goal" :in-theory (e/d (floor) (<-of-*-of-/-arg1)))))

floor-upper-bound-lineartheorem

(defthm floor-upper-bound-linear
  (implies (and (rationalp i) (rationalp j))
    (<= (floor i j) (* i (/ j))))
  :rule-classes ((:linear :trigger-terms ((floor i j))))
  :hints (("Goal" :by my-floor-upper-bound)))

*-of-floor-upper-bound-lineartheorem

(defthm *-of-floor-upper-bound-linear
  (implies (and (< 0 j) (rationalp i) (rationalp j))
    (<= (* j (floor i j)) i))
  :rule-classes :linear :hints (("Goal" :in-theory (enable floor))))

floor-upper-bound-alt-lineartheorem

(defthm floor-upper-bound-alt-linear
  (implies (and (<= 0 i) (rationalp i) (<= 0 j) (rationalp j))
    (<= (* j (floor i j)) i))
  :rule-classes :linear :hints (("Goal" :cases ((equal j 0)))))

*-of-floor-upper-boundtheorem

(defthmd *-of-floor-upper-bound
  (implies (and (< 0 j) (rationalp i) (rationalp j))
    (<= (* j (floor i j)) i)))

floor-upper-bound-stricttheorem

(defthm floor-upper-bound-strict
  (implies (and (not (integerp (/ i j))) (rationalp i) (rationalp j))
    (< (floor i j) (/ i j))))

floor-upper-bound-strong-linear-cheaptheorem

(defthm floor-upper-bound-strong-linear-cheap
  (implies (and (not (integerp (* (/ j) i)))
      (rationalp i)
      (rationalp j))
    (< (floor i j) (* (/ j) i)))
  :rule-classes ((:linear :backchain-limit-lst (0 nil nil)))
  :hints (("Goal" :in-theory (disable <-of-*-of-/-arg2))))

floor-when-not-rationalp-arg1theorem

(defthm floor-when-not-rationalp-arg1
  (implies (and (not (rationalp i)) (rationalp j))
    (equal (floor i j) 0))
  :hints (("Goal" :in-theory (enable floor))))

floor-when-rationalp-and-complex-rationalptheorem

(defthmd floor-when-rationalp-and-complex-rationalp
  (implies (and (rationalp i) (complex-rationalp j))
    (equal (floor i j) 0))
  :hints (("Goal" :in-theory (enable floor))))

divisibility-in-terms-of-floortheorem

(defthmd divisibility-in-terms-of-floor
  (implies (and (rationalp i) (rationalp j) (not (equal 0 j)))
    (equal (integerp (/ i j)) (equal (* j (floor i j)) i)))
  :hints (("Goal" :in-theory (enable floor-when-multiple))))

floor-of---arg1theorem

(defthmd floor-of---arg1
  (implies (and (rationalp i) (rationalp j))
    (equal (floor (- i) j)
      (if (integerp (* i (/ j)))
        (- (floor i j))
        (+ -1 (- (floor i j))))))
  :hints (("Goal" :in-theory (enable floor))))

floor-of---special-casetheorem

(defthmd floor-of---special-case
  (implies (and (not (rationalp j)) (acl2-numberp i) (acl2-numberp j))
    (equal (floor (- i) j)
      (if (rationalp (* i (/ j)))
        (if (integerp (* i (/ j)))
          (- (floor i j))
          (+ -1 (- (floor i j))))
        0)))
  :hints (("Goal" :in-theory (enable floor))))

floor-minus-arg1-bettertheorem

(defthm floor-minus-arg1-better
  (implies (and (rationalp x) (rationalp y) (not (equal 0 y)))
    (equal (floor (- x) y)
      (if (equal (floor x y) (/ x y))
        (- (floor x y))
        (- (- (floor x y)) 1)))))

encapsulate

(encapsulate nil
  (local (defthm floor-of-sum-case-1
      (implies (and (< (+ (mod i1 j) (mod i2 j)) j)
          (rationalp j)
          (< 0 j)
          (rationalp i1)
          (rationalp i2))
        (equal (floor (+ i1 i2) j) (+ (floor i1 j) (floor i2 j))))
      :hints (("Goal" :in-theory (e/d (mod) (floor-upper-bound-linear <-of-*-and-*-cancel))
         :use ((:instance <-of-*-and-*-cancel
            (x1 (+ -1 (* i1 (/ j)) (* i2 (/ j))))
            (x2 (+ (floor i1 j) (floor i2 j)))
            (y j)) (:instance floor-upper-bound-linear (i i1) (j j))
           (:instance floor-upper-bound-linear (i i2) (j j))
           (:instance floor-unique
             (i (+ i1 i2))
             (n (+ (floor i1 j) (floor i2 j)))))
         :do-not '(generalize eliminate-destructors)))))
  (local (defthm floor-of-sum-case-2
      (implies (and (<= j (+ (mod i1 j) (mod i2 j)))
          (rationalp j)
          (< 0 j)
          (rationalp i1)
          (rationalp i2))
        (equal (floor (+ i1 i2) j) (+ 1 (floor i1 j) (floor i2 j))))
      :hints (("Goal" :in-theory (e/d (mod) (<-of-*-and-*-cancel))
         :use ((:instance <-of-*-and-*-cancel
            (x1 (+ (* i1 (/ j)) (* i2 (/ j))))
            (x2 (+ 1 (floor i1 j) (floor i2 j)))
            (y j)) (:instance <-of-*-and-*-cancel
             (x1 (+ -1 (* i1 (/ j)) (* i2 (/ j))))
             (x2 (+ 1 (floor i1 j) (floor i2 j)))
             (y j))
           (:instance my-floor-lower-bound-alt (i i1) (j j))
           (:instance my-floor-lower-bound-alt (i i2) (j j))
           (:instance floor-unique
             (i (+ i1 i2))
             (n (+ 1 (floor i1 j) (floor i2 j)))))
         :do-not '(generalize eliminate-destructors)))))
  (defthmd floor-of-sum
    (implies (and (rationalp j) (< 0 j) (rationalp i1) (rationalp i2))
      (equal (floor (+ i1 i2) j)
        (if (< (+ (mod i1 j) (mod i2 j)) j)
          (+ (floor i1 j) (floor i2 j))
          (+ 1 (floor i1 j) (floor i2 j)))))
    :hints (("Goal" :do-not '(generalize eliminate-destructors)))))

floor-of-+-when-mult-arg1theorem

(defthm floor-of-+-when-mult-arg1
  (implies (and (equal i (/ i1 j))
      (integerp i)
      (rationalp i2)
      (rationalp j))
    (equal (floor (+ i1 i2) j) (+ i (floor i2 j))))
  :hints (("Goal" :cases ((and (acl2-numberp i2) (acl2-numberp i1)) (and (acl2-numberp i2) (not (acl2-numberp i1)))
       (and (not (acl2-numberp i2)) (not (acl2-numberp i1))))
     :in-theory (enable floor))))

floor-of-+-when-mult-arg2theorem

(defthm floor-of-+-when-mult-arg2
  (implies (and (equal i (/ i2 j))
      (integerp i)
      (rationalp i1)
      (rationalp j))
    (equal (floor (+ i1 i2) j) (+ i (floor i1 j))))
  :hints (("Goal" :use (:instance floor-of-+-when-mult-arg1 (i1 i2) (i2 i1))
     :in-theory (disable floor-of-+-when-mult-arg1))))

equal-of-0-and-floortheorem

(defthm equal-of-0-and-floor
  (implies (and (rationalp i) (rationalp j) (< 0 j))
    (equal (equal 0 (floor i j)) (and (< i j) (<= 0 i))))
  :hints (("Goal" :in-theory (enable floor))))

equal-of-0-and-floor-gentheorem

(defthm equal-of-0-and-floor-gen
  (implies (and (rationalp i) (rationalp j))
    (equal (equal 0 (floor i j))
      (if (< 0 j)
        (and (< i j) (<= 0 i))
        (if (equal 0 j)
          t
          (and (< j i) (<= i 0))))))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-1-arg1theorem

(defthm floor-of-1-arg1
  (implies (natp j)
    (equal (floor 1 j)
      (if (equal j 1)
        1
        0)))
  :hints (("Goal" :cases ((equal 0 j)))))

local

(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))

floor-of-floortheorem

(defthm floor-of-floor
  (implies (and (rationalp i) (natp j1) (natp j2))
    (equal (floor (floor i j1) j2) (floor i (* j1 j2))))
  :hints (("Goal" :cases ((and (equal j1 0) (equal j2 0)) (and (not (equal j1 0)) (equal j2 0))
       (and (not (equal j1 0)) (not (equal j2 0)))))))

in-theory

(in-theory (disable floor ceiling mod))

all-vars-negatedfunction

(defun all-vars-negated
  (term)
  (if (variablep term)
    nil
    (if (fquotep term)
      t
      (let ((fn (ffn-symb term)))
        (if (eq 'binary-+ fn)
          (and (all-vars-negated (second term))
            (all-vars-negated (third term)))
          (if (eq 'unary-- fn)
            (variablep (second term))
            nil))))))

floor-minus-eric-bettertheorem

(defthmd floor-minus-eric-better
  (implies (and (syntaxp (and (all-vars-negated i) (not (quotep i))))
      (rationalp i)
      (rationalp j)
      (not (equal j 0)))
    (equal (floor i j)
      (if (integerp (* i (/ j)))
        (- (floor (- i) j))
        (+ (- (floor (- i) j)) -1))))
  :hints (("Goal" :use floor-of---arg1
     :in-theory (disable floor-of---arg1))))

floor-of-plus-normalize-negative-constanttheorem

(defthm floor-of-plus-normalize-negative-constant
  (implies (and (syntaxp (and (quotep k) (quotep y)))
      (<= k 0)
      (rationalp y)
      (not (equal 0 y))
      (rationalp n)
      (rationalp k))
    (equal (floor (+ k n) y)
      (+ (- (ceiling (- k) y))
        (floor (+ (+ (* y (ceiling (- k) y)) k) n) y))))
  :hints (("Goal" :use (:instance floor-of-+-when-mult-arg1
       (i (ceiling (- k) y))
       (i1 (* y (ceiling (- k) y)))
       (i2 (+ k n))
       (j y))
     :in-theory (disable floor-of-+-when-mult-arg1))))

<-*-/-left-with-addends-middletheorem

(defthm <-*-/-left-with-addends-middle
  (implies (and (< 0 y)
      (real/rationalp x)
      (rationalp k)
      (rationalp k2)
      (real/rationalp y)
      (real/rationalp a))
    (equal (< (+ k (* x (/ y)) k2) a)
      (< (+ (* k y) (* k2 y) x) (* a y)))))

floor-bound-lemmatheorem

(defthm floor-bound-lemma
  (implies (and (posp y) (natp n) (< k y) (natp k))
    (<= (floor (+ k n) y) (+ 1 (floor n y))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (disable floor-weak-monotone)
     :use (:instance floor-weak-monotone
       (i1 (+ k n))
       (i2 (+ y n))
       (j y)))))

floor-peel-off-constanttheorem

(defthm floor-peel-off-constant
  (implies (and (syntaxp (quotep k))
      (< k y)
      (rationalp n)
      (natp y)
      (natp k))
    (equal (floor (+ k n) y)
      (if (< (mod n y) (- y k))
        (floor n y)
        (+ 1 (floor n y)))))
  :hints (("Goal" :in-theory (enable floor-of-sum))))

floor-of-times-1/2theorem

(defthm floor-of-times-1/2
  (equal (floor (* 1/2 a) 1) (floor a 2))
  :hints (("Goal" :in-theory (enable floor))))

equal-of-floor-sametheorem

(defthm equal-of-floor-same
  (implies (and (integerp j) (natp i))
    (equal (equal (floor i j) i) (or (equal i 0) (equal j 1))))
  :hints (("Goal" :use ((:instance my-floor-upper-bound))
     :in-theory (disable my-floor-upper-bound)
     :cases ((< 1 j) (< j 1)))))

floor-of-one-lesstheorem

(defthm floor-of-one-less
  (implies (natp i) (equal (floor (+ -1 i) i) 0))
  :hints (("Goal" :in-theory (disable floor-minus-eric-better)
     :cases ((equal i 0)))))

floor-of-minus-and-minustheorem

(defthm floor-of-minus-and-minus
  (implies (and (rationalp i) (rationalp j))
    (equal (floor (- i) (- j)) (floor i j)))
  :hints (("Goal" :in-theory (disable floor-minus))))

floor-when-<theorem

(defthm floor-when-<
  (implies (and (< i j) (>= i 0) (force (rationalp j)))
    (equal (floor i j) 0))
  :hints (("Goal" :cases ((rationalp i)))))

<-of-floor-and-0-when-negative-and-positive-typetheorem

(defthm <-of-floor-and-0-when-negative-and-positive-type
  (implies (and (< i 0) (< 0 j) (rationalp i) (rationalp j))
    (< (floor i j) 0))
  :rule-classes :type-prescription)

<-of-floor-and-0-when-positive-and-negative-typetheorem

(defthm <-of-floor-and-0-when-positive-and-negative-type
  (implies (and (< 0 i) (< j 0) (rationalp i) (rationalp j))
    (< (floor i j) 0))
  :rule-classes :type-prescription)

<=-of-floor-when-<-typetheorem

(defthm <=-of-floor-when-<-type
  (implies (and (< i j) (<= 0 j) (rationalp i) (rationalp j))
    (<= (floor i j) 0))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (enable floor))))

floor-minus-arg2theorem

(defthm floor-minus-arg2
  (implies (and (force (rationalp x)) (rationalp y) (not (equal 0 y)))
    (equal (floor x (- y))
      (if (integerp (* x (/ y)))
        (- (floor x y))
        (- (- (floor x y)) 1)))))

floor-minus-arg1-hacktheorem

(defthm floor-minus-arg1-hack
  (implies (and (syntaxp (quotep k))
      (rationalp x)
      (rationalp k)
      (rationalp y))
    (equal (floor (+ k (- x)) y)
      (if (integerp (* (- x k) (/ y)))
        (- (floor (- x k) y))
        (- (- (floor (- x k) y)) 1))))
  :hints (("Goal" :use (:instance floor-of---arg1 (i (- k x)) (j y))
     :in-theory (disable floor-of---arg1))))

floor-minus-arg2-hacktheorem

(defthm floor-minus-arg2-hack
  (implies (and (syntaxp (quotep k))
      (rationalp x)
      (rationalp k)
      (rationalp y))
    (equal (floor x (+ k (- y)))
      (if (integerp (* x (/ (- y k))))
        (- (floor x (- y k)))
        (- (- (floor x (- y k))) 1))))
  :hints (("Goal" :use (:instance floor-minus-arg2 (y (- y k)))
     :in-theory (disable floor-minus-arg2))))

floor-minus-negative-constanttheorem

(defthm floor-minus-negative-constant
  (implies (and (syntaxp (quotep k))
      (< k 0)
      (rationalp x)
      (rationalp k)
      (rationalp y))
    (equal (floor k y)
      (if (integerp (* (- k) (/ y)))
        (- (floor (- k) y))
        (- (- (floor (- k) y)) 1))))
  :hints (("Goal" :use (:instance floor-of---arg1 (i (- k)) (j y))
     :in-theory (disable floor-of---arg1))))

<-of-floor-and-0theorem

(defthm <-of-floor-and-0
  (implies (rationalp j)
    (equal (< (floor i j) 0)
      (and (rationalp i)
        (or (and (< i 0) (> j 0)) (and (> i 0) (< j 0))))))
  :hints (("Goal" :use (:instance floor-type-1 (x i) (y j))
     :in-theory (disable floor-type-1))))

equal-of-i-and-*-of-floortheorem

(defthmd equal-of-i-and-*-of-floor
  (implies (and (rationalp i) (rationalp j) (not (equal 0 j)))
    (equal (equal i (* j (floor i j))) (integerp (* i (/ j))))))

natp-of-floortheorem

(defthm natp-of-floor
  (implies (and (natp i) (natp j)) (natp (floor i j)))
  :hints (("Goal" :in-theory (e/d (natp) (floor-bounded-by-/)))))

floor-of-+-of-minustheorem

(defthm floor-of-+-of-minus
  (implies (and (not (equal 0 j)) (rationalp j) (rationalp i))
    (equal (floor (+ i (- j)) j) (+ -1 (floor i j)))))

floor-bound-lemma-1theorem

(defthmd floor-bound-lemma-1
  (implies (and (rationalp x)
      (< 0 j)
      (rationalp j)
      (rationalp k)
      (<= (+ 1 k) (floor x j)))
    (<= (+ j (* j k)) x)))

floor-bound-lemma-2theorem

(defthmd floor-bound-lemma-2
  (implies (and (< (floor i j) (+ 1 k))
      (rationalp i)
      (rationalp j)
      (< 0 j)
      (integerp k))
    (< i (+ j (* j k)))))

<-of-floor-arg2theorem

(defthmd <-of-floor-arg2
  (implies (and (rationalp i) (rationalp j) (< 0 j) (integerp k))
    (equal (< k (floor i j))
      (if (integerp k)
        (<= (* j (+ 1 k)) i)
        (<= (+ 1 (floor k 1)) (/ i j)))))
  :hints (("Goal" :use ((:instance floor-bound-lemma-1 (x i)) (:instance floor-bound-lemma-2)))))

<-of-constant-and-floortheorem

(defthmd <-of-constant-and-floor
  (implies (and (syntaxp (and (quotep k) (quotep j)))
      (integerp k)
      (rationalp i)
      (rationalp j)
      (< 0 j))
    (equal (< k (floor i j)) (<= (* j (+ 1 k)) i)))
  :hints (("Goal" :use <-of-floor-arg2)))

<-of-0-and-floortheorem

(defthm <-of-0-and-floor
  (implies (and (integerp i) (posp j))
    (equal (< 0 (floor i j)) (<= j i))))

bound-from-floor-boundtheorem

(defthmd bound-from-floor-bound
  (implies (and (<= k (floor i j))
      (< 0 j)
      (rationalp i)
      (rationalp k)
      (rationalp j))
    (<= (* k j) i)))

bound-from-floor-bound-backtheorem

(defthmd bound-from-floor-bound-back
  (implies (and (<= (* k j) i)
      (< 0 j)
      (rationalp i)
      (integerp k)
      (integerp j))
    (<= k (floor i j)))
  :hints (("Goal" :in-theory (disable my-floor-lower-bound-alt)
     :use ((:instance floor-weak-monotone (i1 (* k j)) (i2 i))))))

<-of-floor-arg1theorem

(defthmd <-of-floor-arg1
  (implies (and (< 0 j) (rationalp i) (integerp k) (integerp j))
    (equal (< (floor i j) k) (< i (* k j))))
  :hints (("Goal" :use (bound-from-floor-bound bound-from-floor-bound-back))))

<-of-floor-arg1-gentheorem

(defthmd <-of-floor-arg1-gen
  (implies (and (< 0 j) (rationalp i) (rationalp k) (integerp j))
    (equal (< (floor i j) k)
      (if (integerp k)
        (< i (* k j))
        (< (/ i j) (+ 1 (floor k 1))))))
  :hints (("Goal" :use ((:instance <-of-floor-arg1) (:instance <-of-floor-arg1 (k (floor k 1))))
     :cases ((equal (floor k 1) (floor i j))))))

<-of-floor-and-constanttheorem

(defthmd <-of-floor-and-constant
  (implies (and (syntaxp (and (quotep k) (quotep j)))
      (< 0 j)
      (rationalp i)
      (integerp k)
      (integerp j))
    (equal (< (floor i j) k) (< i (* k j))))
  :hints (("Goal" :use <-of-floor-arg1
     :in-theory (disable <-of-floor-arg1))))

<-of-times-of-floor-and-sametheorem

(defthm <-of-times-of-floor-and-same
  (implies (and (rationalp i) (rationalp j) (< 0 j))
    (equal (< (* j (floor i j)) i) (not (integerp (/ i j)))))
  :hints (("Goal" :use my-floor-upper-bound
     :in-theory (disable my-floor-upper-bound))))

<-of-*-of-floor-and-sametheorem

(defthmd <-of-*-of-floor-and-same
  (implies (and (rationalp i) (rationalp j) (< 0 j))
    (equal (< (* j (floor i j)) i) (not (equal 0 (mod i j))))))

floor-when-i-is-not-an-acl2-numberptheorem

(defthm floor-when-i-is-not-an-acl2-numberp
  (implies (not (acl2-numberp i)) (equal (floor i j) 0))
  :hints (("Goal" :in-theory (enable floor))))

floor-divide-by-sametheorem

(defthmd floor-divide-by-same
  (implies (and (rationalp i)
      (rationalp k)
      (not (equal 0 k))
      (rationalp j)
      (not (equal 0 j)))
    (equal (floor (/ i k) (/ j k)) (floor i j))))

equal-of-constant-and-floortheorem

(defthmd equal-of-constant-and-floor
  (implies (and (syntaxp (and (quotep k) (quotep y)))
      (posp y)
      (integerp k)
      (integerp x))
    (equal (equal k (floor x y))
      (and (<= (* k y) x) (< x (* (+ 1 k) y)))))
  :hints (("Goal" :in-theory (disable my-floor-lower-bound-alt)
     :use ((:instance my-floor-lower-bound) (:instance my-floor-upper-bound)))))

<=-of-0-and-floor-when-both-nonnegativetheorem

(defthm <=-of-0-and-floor-when-both-nonnegative
  (implies (and (<= 0 i) (<= 0 j) (or (rationalp i) (rationalp j)))
    (<= 0 (floor i j)))
  :hints (("Goal" :in-theory (enable floor) :cases ((rationalp j)))))

<=-of-0-and-floor-when-both-nonnegative-typetheorem

(defthm <=-of-0-and-floor-when-both-nonnegative-type
  (implies (and (<= 0 i) (<= 0 j) (or (rationalp i) (rationalp j)))
    (<= 0 (floor i j)))
  :rule-classes :type-prescription)

<=-of-0-and-floor-when-both-nonpositive-typetheorem

(defthm <=-of-0-and-floor-when-both-nonpositive-type
  (implies (and (<= i 0) (<= j 0) (or (rationalp i) (rationalp j)))
    (<= 0 (floor i j)))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (disable floor-type-1))))

<=-of-floor-and-0-when-nonpositive-and-nonnegative-typetheorem

(defthm <=-of-floor-and-0-when-nonpositive-and-nonnegative-type
  (implies (and (<= i 0) (<= 0 j) (or (rationalp i) (rationalp j)))
    (<= (floor i j) 0))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (enable floor) :cases ((rationalp j)))))

<=-of-floor-and-0-when-nonnegative-and-nonpositive-typetheorem

(defthm <=-of-floor-and-0-when-nonnegative-and-nonpositive-type
  (implies (and (<= 0 i) (<= j 0) (or (rationalp i) (rationalp j)))
    (<= (floor i j) 0))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (enable floor) :cases ((rationalp j)))))

floor-bound-arg1theorem

(defthm floor-bound-arg1
  (implies (and (<= 0 i) (integerp j)) (<= (floor i j) i))
  :hints (("Goal" :cases ((rationalp i))
     :use (floor-bound-hack-eric (:instance my-floor-upper-bound))
     :in-theory (e/d (posp)
       (floor-bounded-by-/ my-floor-upper-bound
         floor-bound-hack-eric
         <-of-*-of-/-arg1
         <-of-*-of-/-arg2
         <-of-*-same-arg2)))))

floor-bound-arg1-lineartheorem

(defthm floor-bound-arg1-linear
  (implies (and (<= 0 i)
      (or (integerp j) (<= 1 j) (<= j 0))
      (rationalp i))
    (<= (floor i j) i))
  :rule-classes ((:linear :trigger-terms ((floor i j))))
  :hints (("Goal" :cases ((< j 0)))))

<=-of-floor-same-when-negative-integerencapsulate

(encapsulate nil
  (local (include-book "arithmetic/inequalities" :dir :system))
  (defthm <=-of-floor-same-when-negative-integer
    (implies (and (<= i 0)
        (integerp i)
        (rationalp i)
        (rationalp j)
        (or (<= 1 j) (<= j 0)))
      (<= i (floor i j)))
    :hints (("Goal" :use (:instance <=-of---of-nonnegative-integer-quotient-of---of-numerator-and-denominator-same
         (x (/ i j)))
       :in-theory (disable <=-of---of-nonnegative-integer-quotient-of---of-numerator-and-denominator-same
         <-*-/-left-commuted
         <-*-/-right
         <-of-*-of-/-arg1-arg1
         <-of-*-of-/-arg2-arg2
         <-of-*-of-/-arg2
         <-of-*-of-/-arg1-alt)))))

<=-of-floor-same-when-negative-integer-2theorem

(defthm <=-of-floor-same-when-negative-integer-2
  (implies (and (<= i 0) (integerp i) (integerp j))
    (<= i (floor i j))))

<-of-floor-of-constant-and-constant-gentheorem

(defthm <-of-floor-of-constant-and-constant-gen
  (implies (and (syntaxp (and (quotep k1) (quotep k)))
      (rationalp i)
      (integerp k)
      (posp k1))
    (equal (< (floor i k1) k) (< i (* k k1))))
  :hints (("Goal" :use ((:instance bound-from-floor-bound (j k1) (k k)) (:instance bound-from-floor-bound-back (j k1) (k k))))))

*-of-floor-of-same-when-multipletheorem

(defthm *-of-floor-of-same-when-multiple
  (implies (and (equal 0 (mod y x)) (rationalp y) (rationalp x))
    (equal (* x (floor y x)) y))
  :hints (("Goal" :cases ((equal 0 x)))))

floor-of-*-sametheorem

(defthm floor-of-*-same
  (implies (and (rationalp i) (rationalp j) (not (equal 0 j)))
    (equal (floor (* j i) j) (floor i 1))))

floor-of-/-arg2theorem

(defthm floor-of-/-arg2
  (equal (floor i (/ j)) (floor (* i j) 1))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-*-of-/-arg2theorem

(defthm floor-of-*-of-/-arg2
  (implies (and (rationalp i) (rationalp j1) (rationalp j2))
    (equal (floor i (* j1 (/ j2))) (floor (* i j2) j1))))

floor-when-negative-and-smalltheorem

(defthmd floor-when-negative-and-small
  (implies (and (< i 0) (<= (- j) i) (rationalp i) (rationalp j))
    (equal (floor i j) -1)))

floor-when-negative-and-small-cheaptheorem

(defthm floor-when-negative-and-small-cheap
  (implies (and (< i 0) (<= (- j) i) (rationalp i) (rationalp j))
    (equal (floor i j) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (0 0 nil nil))))

floor-of-one-less-gentheorem

(defthm floor-of-one-less-gen
  (implies (and (syntaxp (not (quotep i))) (natp i) (posp j))
    (equal (floor (+ -1 i) j)
      (if (equal 0 (mod i j))
        (+ -1 (floor i j))
        (floor i j))))
  :hints (("Goal" :in-theory (enable floor-of-sum))))

floor-of-1-move-integer-addendtheorem

(defthm floor-of-1-move-integer-addend
  (implies (and (integerp n) (rationalp x))
    (equal (floor (+ x n) 1) (+ n (floor x 1)))))

nonnegative-integer-quotient-of-numerator-and-denominatortheorem

(defthmd nonnegative-integer-quotient-of-numerator-and-denominator
  (implies (and (rationalp x) (<= 0 x))
    (equal (nonnegative-integer-quotient (numerator x) (denominator x))
      (floor x 1)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

floor-of-*-of-/-and-1theorem

(defthm floor-of-*-of-/-and-1
  (implies (and (integerp i) (<= 0 pos) (integerp pos))
    (equal (floor (* i (/ j)) 1) (floor i j)))
  :hints (("Goal" :in-theory (enable floor))))

other

(theory-invariant (incompatible (:rewrite floor-of-*-of-/-and-1)
    (:rewrite floor-normalize-denominator)))

my-floor-lower-bound-2theorem

(defthmd my-floor-lower-bound-2
  (implies (and (integerp i) (<= 0 i) (posp j))
    (<= (+ -1 (/ i j) (/ j)) (floor i j)))
  :rule-classes ((:linear :trigger-terms ((floor i j))))
  :hints (("Goal" :use (<=-of-denominator-of-*-of-/ (:instance <=-of-/-linear
         (x0 (denominator (* i (/ j))))
         (x (* i (/ j))))
       (:instance nonnegative-integer-quotient-lower-bound-linear2
         (i (numerator (* i (/ j))))
         (j (denominator (* i (/ j))))))
     :in-theory (e/d (floor)
       (<=-of-denominator-of-*-of-/ <-of-+-arg2-when-negative-constant)))))

floor-when-integerp-of-quotienttheorem

(defthmd floor-when-integerp-of-quotient
  (implies (integerp (* x (/ y)))
    (equal (floor x y) (* x (/ y))))
  :hints (("Goal" :in-theory (enable floor))))

floor-when-not-rationalp-of-quotienttheorem

(defthm floor-when-not-rationalp-of-quotient
  (implies (not (rationalp (* x (/ y))))
    (equal (floor x y) 0))
  :hints (("Goal" :in-theory (enable floor))))

split-low-bittheorem

(defthm split-low-bit
  (implies (rationalp i)
    (equal i (+ (* 2 (floor i 2)) (mod i 2))))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable mod))))

floor-of-2-casestheorem

(defthmd floor-of-2-cases
  (implies (integerp i)
    (equal (floor i 2)
      (if (equal 0 (mod i 2))
        (/ i 2)
        (+ -1/2 (/ i 2)))))
  :hints (("Goal" :use ((:instance floor-unique
        (j 2)
        (n (if (equal 0 (mod i 2))
            (/ i 2)
            (+ 1/2 (/ i 2))))) (:instance split-low-bit)))))

floor-when-evenptheorem

(defthmd floor-when-evenp
  (implies (evenp x) (equal (floor x 2) (/ x 2)))
  :hints (("Goal" :in-theory (enable floor evenp))))

floor-of-2-cases-2theorem

(defthmd floor-of-2-cases-2
  (implies (integerp i)
    (equal (floor i 2)
      (if (evenp i)
        (/ i 2)
        (+ -1/2 (/ i 2)))))
  :hints (("Goal" :in-theory (enable floor-of-2-cases evenp))))

unsigned-byte-p-of-floor-by-2-strongencapsulate

(encapsulate nil
  (local (defthm integerp-of-expt2
      (implies (integerp i)
        (equal (integerp (expt 2 i)) (<= 0 i)))))
  (defthm unsigned-byte-p-of-floor-by-2-strong
    (implies (integerp x)
      (equal (unsigned-byte-p n (floor x 2))
        (and (natp n) (unsigned-byte-p (+ 1 n) x))))
    :hints (("Goal" :in-theory (enable unsigned-byte-p expt <-of-floor-arg1)))))

equal-of-floor-and-*-of-/theorem

(defthm equal-of-floor-and-*-of-/
  (equal (equal (floor i j) (* i (/ j)))
    (integerp (* i (/ j)))))

equal-of-floortheorem

(defthmd equal-of-floor
  (implies (and (rationalp i) (rationalp j))
    (equal (equal val (floor i j))
      (and (integerp val) (<= val (/ i j)) (< (/ i j) (+ 1 val)))))
  :hints (("Goal" :in-theory (disable <-of-*-of-/-arg1 <-of-*-of-/-arg1-alt))))

equal-x-times-2-floor-xtheorem

(defthm equal-x-times-2-floor-x
  (implies (rationalp x)
    (equal (equal x (* 2 (floor x 2))) (evenp x)))
  :hints (("Goal" :in-theory (enable evenp floor))))

unsigned-byte-p-of-floortheorem

(defthm unsigned-byte-p-of-floor
  (implies (and (unsigned-byte-p size x) (natp y))
    (unsigned-byte-p size (floor x y)))
  :hints (("Goal" :cases ((equal 0 y))
     :in-theory (enable unsigned-byte-p))))

floor-of-*-and-*-cancel-arg2-arg2theorem

(defthm floor-of-*-and-*-cancel-arg2-arg2
  (equal (floor (* x z) (* y z))
    (if (equal (fix z) 0)
      0
      (floor x y)))
  :hints (("Goal" :in-theory (enable floor))))

local

(local (defthm helper1
    (implies (and (rationalp i)
        (rationalp j)
        (< 0 j)
        (rationalp k)
        (< k (floor i j)))
      (<= (+ 1 (floor k 1)) (floor i j)))))

local

(local (defthm helper2
    (implies (and (rationalp i)
        (rationalp j)
        (< 0 j)
        (integerp kup)
        (< kup (/ i j)))
      (<= kup (floor i j)))))

<-of-floor-arg2-gentheorem

(defthmd <-of-floor-arg2-gen
  (implies (and (rationalp i) (rationalp j) (< 0 j) (rationalp k))
    (equal (< k (floor i j)) (<= (+ 1 (floor k 1)) (/ i j))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :use (helper1 (:instance helper2 (kup (+ 1 (floor k 1)))))
     :in-theory (disable <-of-*-of-/-arg1-arg2 <-of-*-of-/-arg1 helper1))))

floor-bound-strict-lineartheorem

(defthm floor-bound-strict-linear
  (implies (and (< 1 j) (< 0 i) (rationalp i) (rationalp j))
    (< (floor i j) i))
  :rule-classes :linear)

floor-bound-stricttheorem

(defthm floor-bound-strict
  (implies (and (< 1 j) (<= 0 i) (rationalp i) (rationalp j))
    (equal (< (floor i j) i) (not (equal i 0)))))

floor-of-*-same-2+-1theorem

(defthm floor-of-*-same-2+-1
  (equal (floor (* i1 j i2) j)
    (if (equal (fix j) 0)
      0
      (floor (* i1 i2) 1)))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-*-same-2-1theorem

(defthm floor-of-*-same-2-1
  (implies (and (rationalp i) (rationalp j) (not (equal 0 j)))
    (equal (floor (* i j) j) (floor i 1)))
  :hints (("Goal" :use floor-of-*-same
     :in-theory (disable floor-of-*-same))))

floor-of-2-arg1theorem

(defthm floor-of-2-arg1
  (implies (natp j)
    (equal (floor 2 j)
      (if (equal j 0)
        0
        (if (equal j 1)
          2
          (if (equal j 2)
            1
            0)))))
  :hints (("Goal" :in-theory (disable floor-type-3))))

local

(local (defthm <-of-floor-same-arg2-when-negative
    (implies (and (< i 0) (integerp i) (integerp j))
      (equal (< i (floor i j))
        (if (<= j 0)
          t
          (if (equal 1 j)
            nil
            (if (equal -1 i)
              nil
              t)))))
    :hints (("Goal" :cases ((< j 0) (equal j 0) (and (< 0 j) (<= i -3)))))))

<-of-floor-same-arg2theorem

(defthm <-of-floor-same-arg2
  (implies (and (integerp i) (integerp j))
    (equal (< i (floor i j))
      (if (<= 0 i)
        nil
        (if (<= j 0)
          t
          (if (equal 1 j)
            nil
            (if (equal -1 i)
              nil
              t)))))))

nonnegative-integer-quotient-becomes-floortheorem

(defthmd nonnegative-integer-quotient-becomes-floor
  (implies (and (natp i) (natp j))
    (equal (nonnegative-integer-quotient i j) (floor i j)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient-of-2))))

floor-becomes-nonnegative-integer-quotienttheorem

(defthmd floor-becomes-nonnegative-integer-quotient
  (implies (and (natp i) (natp j))
    (equal (floor i j) (nonnegative-integer-quotient i j)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient-of-2))))

other

(theory-invariant (incompatible (:rewrite floor-becomes-nonnegative-integer-quotient)
    (:rewrite nonnegative-integer-quotient-becomes-floor)))

equal-of-nonnegative-integer-quotient-and-floortheorem

(defthmd equal-of-nonnegative-integer-quotient-and-floor
  (implies (and (natp i) (natp j))
    (equal (equal (nonnegative-integer-quotient i j) (floor i j))
      t))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient-of-2))))