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