The desired function qsqrt is a simple generalization of rto-sqrt to arbitrary positive rationals:
Notation: is abbreviated as .
PROOF: Since , and .
PROOF: Let and
. 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,
By Lemma 7.2.6,
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