# 7.3  IEEE-Rounded Square Root

The desired function qsqrt is a simple generalization of rto-sqrt to arbitrary positive rationals:

Definition 7.3.1   (qsqrt) Let and with and . Let . then

Notation: is abbreviated as .

PROOF: Since

we have

and

By Lemma 4.1.14, and the lemma follows.

PROOF: Since , and

(qsqrt-shift) Let and with and . For all ,

PROOF: Let and

Then

(rnd-qsqrt-equal) Let , , , and with and and let be a common rounding mode. Then

PROOF: Let . By Definition 7.3.1 and Lemmas 7.2.5 and 6.4.3,

The next two lemmas establish the properties of qsqrt discussed at the beginning of this chapter.

(qsqrt-lower, qsqrt-upper) Let , , , and . Assume that , , , and . Let be a common rounding mode. Then

PROOF: Let Let , , , and . By Lemmas 7.3.1 and 7.2.5,

or

By Lemma 6.4.3,

and by Lemma 6.5.17,

(exactp-cmp-qsqrt) Let , , and . Assume that , , , and q is )-exact. Then

(a) ;

(b) ;

(c) .

PROOF: Let , , and . Then and . By Lemma 7.2.6,

The proof of (b) is similar, and (c) follows.

(qsqrt-sqrt) Let and with and . If is -exact, then .

PROOF: Instantiate Lemma 7.3.6 with

(qsqrt-exact-equal) Let , , , and with , , , and . If is -exact, then .

PROOF: By Corollary 7.3.7, . The corollary again follows from Lemma 7.3.6

Lemma 7.3.6 is also critical in the detection of floating-point precision exceptions. As described more fully in Sections 8.4, 9.5, and 10.3, this exception is signaled when an instruction returns a rounded result that differs from the precise mathematical value of an operation. But in the case of the square root, the ACL2 formalization compares to rather than , where is the target precision. This is justified by (c) above, from which it follows that iff .

David Russinoff 2017-08-01