floor-proofs - ACL2 Book

Included Books

ground-zero fp2 denominator numerator predicate nniq product unary-divide rationalp inverted-factor meta-plus-lessp

other

(in-package "ACL2")

local

(local (include-book "ground-zero"))

local

(local (include-book "fp2"))

local

(local (include-book "denominator"))

local

(local (include-book "numerator"))

local

(local (include-book "predicate"))

local

(local (include-book "nniq"))

local

(local (include-book "product"))

local

(local (include-book "unary-divide"))

local

(local (include-book "rationalp"))

local

(local (include-book "inverted-factor"))

local

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

floor-non-negative-integerp-type-prescriptiontheorem

(defthm floor-non-negative-integerp-type-prescription
  (implies (and (<= 0 i)
      (<= 0 j)
      (case-split (not (complex-rationalp j))))
    (and (<= 0 (floor i j)) (integerp (floor i j))))
  :rule-classes (:type-prescription)
  :hints (("Goal" :in-theory (set-difference-theories (enable floor) 'nil))))

floor-non-negativetheorem

(defthm floor-non-negative
  (implies (and (<= 0 i)
      (<= 0 j)
      (case-split (not (complex-rationalp i))))
    (<= 0 (floor i j)))
  :hints (("Goal" :in-theory (set-difference-theories (enable floor) 'nil))))

floor-with-i-not-rational-but-j-rationaltheorem

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

floor-compare-to-zerotheorem

(defthm floor-compare-to-zero
  (implies (and (case-split (rationalp i)) (case-split (rationalp j)))
    (equal (< (floor i j) 0)
      (or (and (< i 0) (< 0 j)) (and (< 0 i) (< j 0)))))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-non-acl2-numbertheorem

(defthm floor-of-non-acl2-number
  (implies (not (acl2-numberp i))
    (and (equal (floor i j) 0) (equal (floor j i) 0)))
  :hints (("Goal" :in-theory (enable floor))))

floor-upper-boundtheorem

(defthm floor-upper-bound
  (implies (and (case-split (rationalp i)) (case-split (rationalp j)))
    (<= (floor i j) (/ i j)))
  :hints (("Goal" :use ((:instance nonnegative-integer-quotient-lower-bound-rewrite
        (i (* -1 (numerator (* i (/ j)))))
        (j (denominator (* i (/ j))))) (:instance nonnegative-integer-quotient-upper-bound-rewrite
         (i (* -1 (numerator (* i (/ j)))))
         (j (denominator (* i (/ j)))))
       (:instance nonnegative-integer-quotient-lower-bound-rewrite
         (i (numerator (* i (/ j))))
         (j (denominator (* i (/ j)))))
       (:instance nonnegative-integer-quotient-upper-bound-rewrite
         (i (numerator (* i (/ j))))
         (j (denominator (* i (/ j))))))
     :in-theory (set-difference-theories (enable floor)
       '(nonnegative-integer-quotient-lower-bound-rewrite nonnegative-integer-quotient-upper-bound-rewrite))))
  :rule-classes (:rewrite (:linear :trigger-terms ((floor i j)))))

floor-equal-i-over-j-rewritetheorem

(defthm floor-equal-i-over-j-rewrite
  (implies (and (case-split (not (equal j 0)))
      (case-split (rationalp i))
      (case-split (rationalp j)))
    (equal (equal (* j (floor i j)) i) (integerp (* i (/ j)))))
  :otf-flg t
  :hints (("Goal" :in-theory (set-difference-theories (enable floor)
       '(nonnegative-integer-quotient-lower-bound-rewrite nonnegative-integer-quotient-max-value-rewrite))
     :use ((:instance nonnegative-integer-quotient-max-value-rewrite
        (i (* -1 (numerator (* i (/ j)))))
        (j (denominator (* i (/ j))))) (:instance nonnegative-integer-quotient-lower-bound-rewrite
         (i (* -1 (numerator (* i (/ j)))))
         (j (denominator (* i (/ j)))))))))

dumbtheorem

(defthm dumb (equal (< x x) nil))

floor-with-j-zerotheorem

(defthm floor-with-j-zero
  (equal (floor i 0) 0)
  :hints (("Goal" :in-theory (enable floor))))

floor-upper-bound-2theorem

(defthm floor-upper-bound-2
  (implies (and (<= 0 j)
      (case-split (rationalp i))
      (case-split (rationalp j))
      (case-split (not (equal j 0))))
    (<= (* j (floor i j)) i))
  :hints (("Goal" :in-theory (disable floor-upper-bound)
     :use floor-upper-bound))
  :rule-classes (:rewrite (:linear :trigger-terms ((floor i j)))))

floor-upper-bound-3theorem

(defthm floor-upper-bound-3
  (implies (and (<= j 0)
      (case-split (rationalp i))
      (case-split (rationalp j))
      (case-split (not (equal j 0))))
    (<= i (* j (floor i j))))
  :hints (("Goal" :in-theory (disable floor-upper-bound)
     :use floor-upper-bound))
  :rule-classes (:rewrite (:linear :trigger-terms ((floor i j)))))

floor-lower-boundtheorem

(defthm floor-lower-bound
  (implies (and (case-split (rationalp i)) (case-split (rationalp j)))
    (< (+ -1 (* i (/ j))) (floor i j)))
  :otf-flg t
  :hints (("Goal" :in-theory (set-difference-theories (enable floor)
       '(less-than-multiply-through-by-inverted-factor-from-left-hand-side less-than-multiply-through-by-inverted-factor-from-right-hand-side
         equal-multiply-through-by-inverted-factor-from-right-hand-side))))
  :rule-classes (:rewrite (:linear :trigger-terms ((floor i j)))))

floor-when-arg-quotient-isnt-rationaltheorem

(defthm floor-when-arg-quotient-isnt-rational
  (implies (not (rationalp (* i (/ j))))
    (equal (floor i j) 0))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-non-rational-by-onetheorem

(defthm floor-of-non-rational-by-one
  (implies (not (rationalp i)) (equal (floor i 1) 0))
  :hints (("Goal" :in-theory (enable floor))))

floor-of-rational-and-complextheorem

(defthm floor-of-rational-and-complex
  (implies (and (rationalp i)
      (not (rationalp j))
      (case-split (acl2-numberp j)))
    (and (equal (floor i j) 0) (equal (floor j i) 0)))
  :hints (("Goal" :in-theory (enable floor))))

floor-with-i-not-rationaltheorem

(defthm floor-with-i-not-rational
  (implies (not (rationalp i))
    (equal (floor i j)
      (if (and (complex-rationalp i)
          (complex-rationalp j)
          (rationalp (/ i j)))
        (floor (/ i j) 1)
        0)))
  :hints (("Goal" :in-theory (enable floor))))

floor-with-j-not-rationaltheorem

(defthm floor-with-j-not-rational
  (implies (not (rationalp j))
    (equal (floor i j)
      (if (and (complex-rationalp i)
          (complex-rationalp j)
          (rationalp (/ i j)))
        (floor (/ i j) 1)
        0)))
  :hints (("Goal" :in-theory (enable floor))))

floor-with-j-not-rational-but-i-rationaltheorem

(defthm floor-with-j-not-rational-but-i-rational
  (implies (and (not (rationalp i)) (rationalp j))
    (equal (floor i j) 0)))

floor-of-zerotheorem

(defthm floor-of-zero (equal (floor 0 j) 0))

floor-of-integer-by-1theorem

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