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

Notation: is abbreviated as .

PROOF: Since

PROOF: Since , and .

PROOF: Let and

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.

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

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

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

PROOF: Instantiate Lemma 7.3.6 with .

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