Truncated Square Root
Function:
(defun rtz-sqrt (x n) (declare (xargs :guard (and (real/rationalp x) (natp n)))) (if (zp n) 0 (let* ((lower (rtz-sqrt x (1- n))) (upper (+ lower (expt 2 (- n))))) (if (<= (* upper upper) x) upper lower))))
Theorem:
(defthm rtz-sqrt-bounds (implies (and (rationalp x) (<= 1/4 x) (not (zp n))) (and (<= 1/2 (rtz-sqrt x n)) (<= (rtz-sqrt x n) (- 1 (expt 2 (- n)))))) :rule-classes nil)
Theorem:
(defthm expo-rtz-sqrt (implies (and (rationalp x) (<= 1/4 x) (not (zp n))) (equal (expo (rtz-sqrt x n)) -1)))
Theorem:
(defthm exactp-rtz-sqrt (implies (and (rationalp x) (<= 1/4 x) (not (zp n))) (exactp (rtz-sqrt x n) n)) :rule-classes nil)
Theorem:
(defthm rtz-sqrt-square-bounds (implies (and (not (zp n)) (rationalp x) (<= 1/4 x) (< x 1)) (and (<= (* (rtz-sqrt x n) (rtz-sqrt x n)) x) (< x (* (+ (rtz-sqrt x n) (expt 2 (- n))) (+ (rtz-sqrt x n) (expt 2 (- n))))))) :rule-classes nil)
Theorem:
(defthm rtz-sqrt-unique (implies (and (not (zp n)) (rationalp x) (<= 1/4 x) (< x 1) (rationalp a) (exactp a n) (>= a 1/2) (<= (* a a) x) (< x (* (+ a (expt 2 (- n))) (+ a (expt 2 (- n)))))) (= a (rtz-sqrt x n))) :rule-classes nil)
Theorem:
(defthm rtz-rtz-sqrt (implies (and (rationalp x) (<= 1/4 x) (not (zp m)) (natp n) (>= n m)) (equal (rtz (rtz-sqrt x n) m) (rtz-sqrt x m))))