Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> NASA PVS Library <s> This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> NASA PVS Library <s> This paper reports on a construction of the real numbers in the ProofPower implementation of the HOL logic. Since the original construction was implemented, some major improvements to the ideas have been discovered. The improvements involve some entertaining mathematics: it turns out that the Dedekind cuts provide many routes one can travel to get from the ring of integers, Z, to the field of real numbers, R. The traditional stop-over on the way is the field of rational numbers, Q. This paper shows that going via certain rings of algebraic numbers can provide a pleasant alternative to the more well-trodden track. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> NASA PVS Library <s> When handling proofs of properties in the real world we often need to assert that one numeric quantity is greater than another. When these numeric quantities are real-valued, it is often tempting to get out the calculator to calculate the values of the expressions and then enter the results directly into the theorem prover as "facts" or axioms, since formally proving the desired properties can often be very tiresome. Obviously, such a procedure poses a few risks. ::: ::: An alternative approach, presented in this paper, is to prove the correctness of an arbitrarily accurate calculator for the reals. If this calculator is expressed in terms of the underlying integer arithmetic operations of the theorem-prover's implementation language, then there is a reasonable expectation that a practical evaluator of real-valued expressions may have been constructed. ::: ::: Obviously, there are some constraints imposed by computability theory. It is well known, for example, that it is not possible to determine the sign of a computable real in finite time. We show that for all practical purposes, we need not worry about such fussy details. After all, mathematicians have --- throughout the centuries --- been prepared to make such calculations without being overly punctilious about the computability of the operations they were performing! ::: ::: We report on the experience of validating and using a real number calculator in PVS. <s> BIB003
In addition to its axiomatization of R, PVS also comes with a development of constructive reals by BIB003 . They are based on a stream of digits that gives Cauchy sequences. Then each operation is defined: addition, subtraction, multiplication, inverse, division, and power series. All the correctness lemmas relate the Cauchy implementation with the main implementation. Their statements look as follows. x , y : VAR real cx , cy : VAR cauchy_real mul_lemma : LEMMA cauchy_prop (x , cx ) AND cauchy_prop (y , cy ) = > cauchy_prop ( x *y , cauchy_mul ( cx , cy )) 3.2.5. Mizar While originally an axiomatization, the formalization of real numbers in Mizar was later changed to a construction based on Dedekind cuts  ). Since Mizar is based on set theory, Dedekind cuts easily fit in this system. The hierarchy starts by defining the natural numbers and the nonnegative rational numbers RAT+ on top of them. Then Dedekind cuts are formalized with their traditional definition: which translates to saying that A is a Dedekind cut if it is a strict subset of Q + ∪ {0} such that Although the empty set is usually excluded from Dedekind cuts, this is not the case in Mizar. The reason is that the empty set happens to represent 0 in Mizar, so it will not cause any issue in the following. The nonnegative real numbers then follow by taking the union of nonnegative rational numbers and Dedekind cuts. As a consequence, the injection from nonnegative rational numbers to real numbers is just the identity function. Note that Dedekind cuts represent both rational and irrational numbers, so one would end up with every rational number being represented by two sets. Therefore, to obtain a unique representation for rational numbers, the definition of nonnegative real numbers removes rational Dedekind cuts from this union: Since negative integers and negative rational numbers were built the same way (a pair with a first element equal to zero / the empty set), integers and rational numbers are actual subsets of real numbers. Arithmetic operations and their properties are first proved on Dedekind cuts, then extended to nonnegative reals, and finally extended to reals. For instance, the function below defines the addition on Dedekind cuts. Finally, the library proves the completeness property under various forms. Below is the one for the least upper bound expressed as a function. Given a nonempty upper-bounded set, it returns the least upper bound (noted by the keyword it in the definition). l e t X be real -membered set ; assume A1 : ( not X i s empty & X i s bounded_above ); func upper_bound X -> real number means ( ( f o r r being real number s t r in X holds r <= i t ) & ( f o r s being real number s t 0 < s holds ex r being real number s t ( r in X & i t -s < r ) ) ); 3.2.6. HOL4 As in Mizar's library, HOL4 defines real numbers BIB001 ) using Dedekind cuts: with hrat_lt the strict ordering on positive rational numbers. In this definition, a cut C is a subset of Q + ≡ {(x + 1, y + 1) | x, y ∈ N}. To define operations and prove theorems, there are two functions hreal, from subsets of Q + toward R + , and cut from R + toward Dedekind cuts, characterized by val hreal_tybij = d e f i n e _ n e w _ t y p e _ b i j e c t i o n s { name =" hreal_tybij " , ABS =" hreal " , REP =" cut " , tyax = hreal_tydef }; where define new type bijections generates the functions hreal and cut such that Except for the multiplicative inverse, operations on positive real numbers are then defined in a way similar to Mizar: Finally, as in HOL Light, real numbers are defined as the quotient of the set of pairs of positive real numbers by the following equivalence relation: 3.2.7. ProofPower-HOL As Mizar and HOL4, ProofPower-HOL defines real numbers using Dedekind cuts. The definition below uses ProofPower's syntax: • is the separator between quantifiers and formulas, $ is an arbitrary relation (over which the formula is universally-quantified), and is the infix notation for $ . Unlike those systems, here Dedekind cuts are subsets of dyadic numbers D = {(2m + 1)/2 n | m ∈ N and n ∈ Z}. The reference manual (ProofPower development team 2006) only describes multiplications and natural exponentiation for this set in theory DYADIC. Unfortunately, the construction of negative real numbers and real operations is not described. Moreover, another formalization of real numbers, based on Dedekind cuts of Z √ 2 , is described by BIB002 , but is not available.