floor

other

(in-package "ACL2")

local

(local (include-book "floor-proofs"))

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

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

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

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

floor-non-negativetheorem

(defthm floor-non-negative
  (implies (and (<= 0 i)
      (<= 0 j)
      (case-split (not (complex-rationalp i))))
    (<= 0 (floor i j))))

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

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

floor-upper-boundtheorem

(defthm floor-upper-bound
  (implies (and (case-split (rationalp i)) (case-split (rationalp j)))
    (<= (floor i j) (/ i j)))
  :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))))))

dumbtheorem

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

floor-with-j-zerotheorem

(defthm floor-with-j-zero (equal (floor i 0) 0))

floor-with-i-zerotheorem

(defthm floor-with-i-zero (equal (floor 0 j) 0))

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

floor-of-non-rational-by-onetheorem

(defthm floor-of-non-rational-by-one
  (implies (not (rationalp i)) (equal (floor i 1) 0)))

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

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

Included Books