IEEE-Rounded Square Root
Function:
(defun qsqrt (x n) (declare (xargs :guard (and (real/rationalp x) (posp n)))) (let ((e (1+ (fl (/ (expo x) 2))))) (* (expt 2 e) (rto-sqrt (/ x (expt 2 (* 2 e))) n))))
Theorem:
(defthm qsqrt-expo (implies (and (rationalp x) (> x 0)) (let* ((e (1+ (fl (/ (expo x) 2)))) (xp (/ x (expt 2 (* 2 e))))) (and (<= 1/4 xp) (< xp 1)))) :rule-classes nil)
Theorem:
(defthm qsqrt-rto-sqrt (implies (and (rationalp x) (<= 1/4 x) (< x 1) (integerp n) (> n 1)) (equal (qsqrt x n) (rto-sqrt x n))))
Theorem:
(defthm qsqrt-pos (implies (and (rationalp x) (> x 0)) (> (qsqrt x n) 0)))
Theorem:
(defthm qsqrt-shift (implies (and (rationalp x) (> x 0) (integerp k) (integerp n) (> n 1)) (equal (qsqrt (* (expt 2 (* 2 k)) x) n) (* (expt 2 k) (qsqrt x n)))))
Theorem:
(defthm rnd-qsqrt-equal (implies (and (rationalp x) (> x 0) (not (zp k)) (natp n) (>= n (+ k 2)) (natp m) (>= m n) (common-mode-p mode)) (equal (rnd (qsqrt x m) mode k) (rnd (qsqrt x n) mode k))) :rule-classes nil)
Theorem:
(defthm qsqrt-lower (implies (and (rationalp x) (> x 0) (rationalp l) (<= (* l l) x) (common-mode-p mode) (not (zp k)) (integerp n) (>= n (+ k 2))) (<= (rnd l mode k) (rnd (qsqrt x n) mode k))) :rule-classes nil)
Theorem:
(defthm qsqrt-upper (implies (and (rationalp x) (> x 0) (rationalp h) (>= h 0) (>= (* h h) x) (common-mode-p mode) (not (zp k)) (integerp n) (>= n (+ k 2))) (>= (rnd h mode k) (rnd (qsqrt x n) mode k))) :rule-classes nil)
Theorem:
(defthm exactp-cmp-qsqrt (implies (and (rationalp x) (> x 0) (rationalp q) (> q 0) (integerp n) (> n 1) (exactp q (1- n))) (and (iff (< (* q q) x) (< q (qsqrt x n))) (iff (> (* q q) x) (> q (qsqrt x n))) (iff (= (* q q) x) (= q (qsqrt x n))))) :rule-classes nil)
Theorem:
(defthm qsqrt-sqrt (implies (and (rationalp x) (> x 0) (integerp n) (> n 1) (exactp (qsqrt x n) (1- n))) (equal (* (qsqrt x n) (qsqrt x n)) x)))
Theorem:
(defthm qsqrt-exact-equal (implies (and (rationalp x) (> x 0) (not (zp k)) (natp n) (> n k) (natp m) (> m k) (exactp (qsqrt x n) k)) (equal (qsqrt x n) (qsqrt x m))) :rule-classes nil)