• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
        • Register-Transfer Logic
          • Bit Vectors
          • Logical Operations
          • Basic Arithmetic Functions
            • Modulus
            • Floor and Ceiling
            • Chop
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Basic Arithmetic Functions

Floor and Ceiling

Floor and Ceiling

Definitions and Theorems

Function: fl

(defun fl (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

Theorem: fl-def

(defthm fl-def
  (and (integerp (fl x))
       (implies (case-split (rationalp x))
                (and (<= (fl x) x) (< x (1+ (fl x))))))
  :rule-classes
  ((:linear
        :corollary (implies (case-split (rationalp x))
                            (and (<= (fl x) x) (< x (1+ (fl x))))))
   (:type-prescription :corollary (integerp (fl x)))))

Theorem: fl-unique

(defthm fl-unique
  (implies (and (rationalp x)
                (integerp n)
                (<= n x)
                (< x (1+ n)))
           (equal (fl x) n))
  :rule-classes nil)

Theorem: fl-integerp

(defthm fl-integerp
  (equal (equal (fl x) x) (integerp x)))

Theorem: integerp-fl

(defthm integerp-fl
  (implies (integerp x) (equal (fl x) x)))

Theorem: quot-bnd

(defthm quot-bnd
  (implies (and (<= 0 x)
                (<= 0 y)
                (rationalp x)
                (rationalp y))
           (<= (* y (fl (/ x y))) x))
  :rule-classes :linear)

Theorem: fl-monotone-linear

(defthm fl-monotone-linear
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (fl x) (fl y)))
  :rule-classes :linear)

Theorem: n<=fl-linear

(defthm n<=fl-linear
  (implies (and (<= n x)
                (rationalp x)
                (integerp n))
           (<= n (fl x)))
  :rule-classes :linear)

Theorem: fl+int-rewrite

(defthm fl+int-rewrite
  (implies (and (integerp n) (real/rationalp x))
           (and (equal (fl (+ x n)) (+ (fl x) n))
                (equal (fl (+ n x)) (+ n (fl x))))))

Theorem: fl/int-rewrite

(defthm fl/int-rewrite
  (implies (and (integerp n)
                (<= 0 n)
                (rationalp x))
           (equal (fl (* (fl x) (/ n)))
                  (fl (/ x n)))))

Theorem: fl/int-rewrite-alt

(defthm fl/int-rewrite-alt
  (implies (and (integerp n)
                (<= 0 n)
                (rationalp x))
           (equal (fl (* (/ n) (fl x)))
                  (fl (/ x n)))))

Theorem: fl*1/int-rewrite

(defthm fl*1/int-rewrite
  (implies (and (integerp (/ n))
                (<= 0 n)
                (real/rationalp x))
           (equal (fl (* (fl x) n)) (fl (* x n)))))

Theorem: fl*1/int-rewrite-alt

(defthm fl*1/int-rewrite-alt
  (implies (and (integerp (/ n))
                (<= 0 n)
                (real/rationalp x))
           (equal (fl (* n (fl x))) (fl (* x n)))))

Theorem: fl-half-int

(defthm fl-half-int
  (implies (and (integerp n)
                (not (= n 0))
                (not (= n -1)))
           (< (abs (fl (/ n 2))) (abs n)))
  :rule-classes nil)

Theorem: minus-fl

(defthm minus-fl
  (implies (rationalp x)
           (equal (fl (- x))
                  (if (integerp x)
                      (- x)
                    (1- (- (fl x)))))))

Theorem: fl-m-n

(defthm fl-m-n
  (implies (and (< 0 n) (integerp m) (integerp n))
           (= (fl (- (/ m n)))
              (1- (- (fl (/ (1- m) n))))))
  :rule-classes nil)

Function: cg

(defun cg (x)
  (declare (xargs :guard (real/rationalp x)))
  (- (fl (- x))))

Theorem: cg-def

(defthm cg-def
  (and (integerp (cg x))
       (implies (case-split (rationalp x))
                (and (>= (cg x) x) (> (1+ x) (cg x)))))
  :rule-classes
  ((:linear
        :corollary (implies (case-split (rationalp x))
                            (and (>= (cg x) x) (> (1+ x) (cg x)))))
   (:type-prescription :corollary (integerp (cg x)))))

Theorem: cg-unique

(defthm cg-unique
  (implies (and (rationalp x)
                (integerp n)
                (>= n x)
                (> (1+ x) n))
           (equal (cg x) n))
  :rule-classes nil)

Theorem: cg-integerp

(defthm cg-integerp
  (implies (rationalp x)
           (equal (equal (cg x) x) (integerp x))))

Theorem: cg-monotone-linear

(defthm cg-monotone-linear
  (implies (and (rationalp x)
                (rationalp y)
                (<= x y))
           (<= (cg x) (cg y)))
  :rule-classes :linear)

Theorem: n>=cg-linear

(defthm n>=cg-linear
  (implies (and (>= n x)
                (rationalp x)
                (integerp n))
           (>= n (cg x)))
  :rule-classes :linear)

Theorem: cg+int-rewrite

(defthm cg+int-rewrite
  (implies (and (integerp n) (rationalp x))
           (equal (cg (+ x n)) (+ (cg x) n))))

Theorem: cg/int-rewrite

(defthm cg/int-rewrite
  (implies (and (integerp n) (> n 0) (rationalp x))
           (equal (cg (* (cg x) (/ n)))
                  (cg (/ x n)))))

Theorem: cg/int-rewrite-alt

(defthm cg/int-rewrite-alt
  (implies (and (integerp n) (> n 0) (rationalp x))
           (equal (cg (* (/ n) (cg x)))
                  (cg (/ x n)))))

Theorem: fl-cg

(defthm fl-cg
  (implies (rationalp x)
           (equal (cg x)
                  (if (integerp x) (fl x) (1+ (fl x)))))
  :rule-classes nil)