Floor and Ceiling
Function:
(defun fl (x) (declare (xargs :guard (real/rationalp x))) (floor x 1))
Theorem:
(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:
(defthm fl-unique (implies (and (rationalp x) (integerp n) (<= n x) (< x (1+ n))) (equal (fl x) n)) :rule-classes nil)
Theorem:
(defthm fl-integerp (equal (equal (fl x) x) (integerp x)))
Theorem:
(defthm integerp-fl (implies (integerp x) (equal (fl x) x)))
Theorem:
(defthm quot-bnd (implies (and (<= 0 x) (<= 0 y) (rationalp x) (rationalp y)) (<= (* y (fl (/ x y))) x)) :rule-classes :linear)
Theorem:
(defthm fl-monotone-linear (implies (and (<= x y) (rationalp x) (rationalp y)) (<= (fl x) (fl y))) :rule-classes :linear)
Theorem:
(defthm n<=fl-linear (implies (and (<= n x) (rationalp x) (integerp n)) (<= n (fl x))) :rule-classes :linear)
Theorem:
(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:
(defthm fl/int-rewrite (implies (and (integerp n) (<= 0 n) (rationalp x)) (equal (fl (* (fl x) (/ n))) (fl (/ x n)))))
Theorem:
(defthm fl/int-rewrite-alt (implies (and (integerp n) (<= 0 n) (rationalp x)) (equal (fl (* (/ n) (fl x))) (fl (/ x n)))))
Theorem:
(defthm fl*1/int-rewrite (implies (and (integerp (/ n)) (<= 0 n) (real/rationalp x)) (equal (fl (* (fl x) n)) (fl (* x n)))))
Theorem:
(defthm fl*1/int-rewrite-alt (implies (and (integerp (/ n)) (<= 0 n) (real/rationalp x)) (equal (fl (* n (fl x))) (fl (* x n)))))
Theorem:
(defthm fl-half-int (implies (and (integerp n) (not (= n 0)) (not (= n -1))) (< (abs (fl (/ n 2))) (abs n))) :rule-classes nil)
Theorem:
(defthm minus-fl (implies (rationalp x) (equal (fl (- x)) (if (integerp x) (- x) (1- (- (fl x)))))))
Theorem:
(defthm fl-m-n (implies (and (< 0 n) (integerp m) (integerp n)) (= (fl (- (/ m n))) (1- (- (fl (/ (1- m) n)))))) :rule-classes nil)
Function:
(defun cg (x) (declare (xargs :guard (real/rationalp x))) (- (fl (- x))))
Theorem:
(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:
(defthm cg-unique (implies (and (rationalp x) (integerp n) (>= n x) (> (1+ x) n)) (equal (cg x) n)) :rule-classes nil)
Theorem:
(defthm cg-integerp (implies (rationalp x) (equal (equal (cg x) x) (integerp x))))
Theorem:
(defthm cg-monotone-linear (implies (and (rationalp x) (rationalp y) (<= x y)) (<= (cg x) (cg y))) :rule-classes :linear)
Theorem:
(defthm n>=cg-linear (implies (and (>= n x) (rationalp x) (integerp n)) (>= n (cg x))) :rule-classes :linear)
Theorem:
(defthm cg+int-rewrite (implies (and (integerp n) (rationalp x)) (equal (cg (+ x n)) (+ (cg x) n))))
Theorem:
(defthm cg/int-rewrite (implies (and (integerp n) (> n 0) (rationalp x)) (equal (cg (* (cg x) (/ n))) (cg (/ x n)))))
Theorem:
(defthm cg/int-rewrite-alt (implies (and (integerp n) (> n 0) (rationalp x)) (equal (cg (* (/ n) (cg x))) (cg (/ x n)))))
Theorem:
(defthm fl-cg (implies (rationalp x) (equal (cg x) (if (integerp x) (fl x) (1+ (fl x))))) :rule-classes nil)