Chop
Function:
(defun chop (x k) (declare (xargs :guard (and (real/rationalp x) (integerp k)))) (/ (fl (* (expt 2 k) x)) (expt 2 k)))
Theorem:
(defthm chop-mod (implies (and (rationalp x) (integerp k)) (equal (chop x k) (- x (mod x (expt 2 (- k)))))))
Theorem:
(defthm chop-down (implies (and (rationalp x) (integerp n)) (<= (chop x n) x)) :rule-classes nil)
Theorem:
(defthm chop-monotone (implies (and (rationalp x) (rationalp y) (integerp n) (<= x y)) (<= (chop x n) (chop y n))) :rule-classes nil)
Theorem:
(defthm chop-chop (implies (and (rationalp x) (integerp k) (integerp m) (<= k m)) (and (equal (chop (chop x m) k) (chop x k)) (equal (chop (chop x k) m) (chop x k)) (<= (chop x k) (chop x m)))))
Theorem:
(defthm chop-plus (implies (and (rationalp x) (rationalp y) (integerp k)) (and (equal (chop (+ x (chop y k)) k) (+ (chop x k) (chop y k))) (equal (chop (+ (chop x k) (chop y k)) k) (+ (chop x k) (chop y k))) (equal (chop (- x (chop y k)) k) (- (chop x k) (chop y k))) (equal (chop (- (chop x k) (chop y k)) k) (- (chop x k) (chop y k))))))
Theorem:
(defthm chop-shift (implies (and (rationalp x) (integerp k) (integerp m)) (equal (chop (* (expt 2 k) x) m) (* (expt 2 k) (chop x (+ k m))))))
Theorem:
(defthm chop-bound (implies (and (rationalp x) (integerp n) (natp m)) (iff (<= n x) (<= n (chop x m)))) :rule-classes nil)
Theorem:
(defthm chop-small (implies (and (rationalp x) (integerp m) (< x (expt 2 (- m))) (<= (- (expt 2 (- m))) x)) (equal (chop x m) (if (>= x 0) 0 (- (expt 2 (- m)))))))
Theorem:
(defthm chop-0 (implies (and (rationalp x) (integerp m) (< (abs (chop x m)) (expt 2 (- m)))) (equal (chop x m) 0)))
Theorem:
(defthm chop-int-bounds (implies (and (natp k) (natp n) (rationalp x)) (and (<= (chop (fl (/ x (expt 2 n))) (- k)) (/ (chop x (- k)) (expt 2 n))) (<= (/ (+ (chop x (- k)) (expt 2 k)) (expt 2 n)) (+ (chop (fl (/ x (expt 2 n))) (- k)) (expt 2 k))))) :rule-classes nil)
Theorem:
(defthm chop-int-neg (implies (and (natp k) (natp n) (rationalp x) (rationalp y) (= (fl (/ x (expt 2 k))) (fl (/ y (expt 2 k)))) (not (integerp (/ x (expt 2 k))))) (equal (chop (1- (- (fl (/ y (expt 2 n))))) (- k)) (chop (- (/ x (expt 2 n))) (- k)))))