Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> The definitions of the mode Function and the graph of a function are introduced. The graph of a function is defined to be identical with the function. The following concepts are also defined: the domain of a function, the range of a function, the identity function, the composition of functions, the 1-1 function, the inverse function, the restriction of a function, the image and the inverse image. Certain basic facts about functions and the notions defined in the article are proved. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> Summary. We define the proper and the improper limit of a real function at a point. The main properties of the operations on the limit of a function are proved. The connection between the one-side limits and the limit of a function at a point are exposed. Equivalent Cauchy and Heine characterizations of the limit of a real function at a point are proved. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical Ɛ and δ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real analysis, and a relatively high degree of proof automation in many cases. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> Preface. 1. Introduction. I: Preliminaries. 2. Overview. 3. Summaries of the Case Studies. 4. ACL2 Essentials. II: Case Studies. 5. An Exercise in Graph Theory J.S. Moore. 6. Modular Proof: The Fundamental Theorem of Calculus M. Kaufmann. 7. Mu-Calculus Model-Checking P. Manolios. 8. High-Speed, Analyzable Simulators D. Greve, et al. 9. Verification of a Simple Pipelined Machine Model J. Sawada. 10. The DE Language. 11. Using Macros to Mimic VHDL D. Borrione, et al. 12. Symbolic Trajectory Evaluation D.A. Jamsek. 13. RTL Verification: A Floating-Point Multiplier D.M. Russinoff, A. Flatau. 14. Design Verification of a Safety-Critical Embedded Verifier P. Bertoli, P. Traverso. 15. Compiler Verification Revisited W. Goerigk. 16. Ivy: A Preprocessor and Proof Checker for First-Order Logic W. McCune, O. Shumsky. 17. Knuth's Generalization of McCarthy's 91 Function J. Cowles. 18. Continuity and Differentiability R. Gamboa. Bibliography. Index. <s> BIB005 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> Summary. The continuity of real functions is discussed. There is a function defined on some domain in real numbers which is continuous in a single point and on a subset of domain of the function. Main properties of real continuous functions are proved. Among them there is the Weierstras Theorem. Algebraic features for real continuous functions are shown. Lipschitzian functions are introduced. The Lipschitz condition entails continuity. <s> BIB006 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> We describe a method for introducing “partial functions” into ACL2, that is, functions not defined everywhere. The function “definitions” are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions, and we discuss how such functions can be used to prove theorems about state machine models without reasoning about “clocks” or counting the number of steps until termination. Our macro for introducing “partial functions” also permits a variety of other recursive schemes, and we briefly illustrate some of them. <s> BIB007 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is R N with the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimension N in a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitrary N-dimensional Euclidean space, e.g. Brouwer's fixpoint theorem and the differentiability of inverse functions. <s> BIB008 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert's epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq's standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library's in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation. <s> BIB009 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Partial functions <s> We describe the library of theorems about N-dimensional Euclidean space that has been formalized in the HOL Light prover. This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. The library includes various `big name' theorems (Brouwer's fixed point theorem, the Stone-Weierstrass theorem, the Tietze extension theorem), numerous non-trivial results that are useful in applications (second mean value theorem for integrals, power series for real and complex transcendental functions) and a host of supporting definitions and lemmas. It also includes some specialized automated proof tools. The library has as planned been applied to the Flyspeck project and has become the basis of a significant development of results in complex analysis, among others. <s> BIB010
Mathematical functions are usually defined as functions from a subset of real numbers to real numbers. There are two ways for proof systems to define partial functions. They either specify the definition domain in the type of the function, or they use total functions and specify the domain in theorem hypotheses. For instance, the square root function can be defined, either as a partial function defined on nonnegative reals, or as a total function defined for all real numbers. In the latter case, a theorem such as √ x 2 = x will have x ≥ 0 as an explicit hypothesis. The way of defining functions is highly dependent on the underlying logic. Mizar identifies functions with their graphs: sets X such that ∀x, y 1 , y 2 , x, y 1 ∈ X ∧ x, y 2 ∈ X ⇒ y 1 = y 2 . Thanks to this approach, the domain is defined as {x | ∃y, x, y ∈ X} and f (x) is the only value such that x, f (x) ∈ X if x is in the domain BIB001 ). Due to the set-theoretical approach of Mizar, having functions defined on partial domains is natural. PVS also uses partial domains: a real function is a function defined on a sub-type of real numbers. Using type correctness conditions (TCC), side conditions are automatically generated, and often proved for simple functions. This definition allows one to formalize theorems without making a distinction between total and partial functions. Again, this choice is natural for PVS, due to the pervasiveness of sub-types in its logic framework. In C-CoRN, functions have to be compatible with the equivalence relation, so that a function applied to two different Cauchy sequences representing the same real numbers gives the same result. So each function has to come with this property of being welldefined. For partial functions, the only difference is that this property is only required for values in the domain, which also has to be well-defined. HOL-based systems, including ProofPower-HOL, use the second approach: functions are total and theorems work only on restricted domains. Indeed, sub-typing is hardly supported in these systems. So it is simpler to ensure that all real functions have the same type, that is, their preimage is R. This is also the case for some functions of the Coq standard library such as the multiplicative inverse and the square root. In ACL2, the way to define partial functions is on a case-by-case basis. The different approaches are described by BIB007 . The situation is sensibly different from other systems because the issue of function sub-typing is nonexistent: manipulating functions is outside the scope of a first-order system. 4.2.2. Limits The notion of limit is defined in PVS and ProofPower  ) using the usual ε-δ definition. In a domain D, a function f : R → R converges toward a limit ∈ R at point x ∈ D when In Coq's standard library, the convergence is given for arbitrary metric spaces. For a function f : This definition leaves out the condition "x is a limit point of D". This makes the definition easier to use, but uniqueness of the limit is no longer guaranteed. In Isabelle/HOL and HOL Light, convergence for functions between two topological spaces is defined using the topological definition (2) with the filter F = {P | ∃S ∈ {opens}, x ∈ S ∧ S\{x} ⊆ P }. The formalization proves that this definition is equivalent to (7) in a metric space. HOL4 uses its topological definition (3) of convergence with the same topology as for convergence of sequences, but with the partial order defined by ∀y, y ∈ R, y y ⇔ |y − x| ≤ |y − x|. Unlike sequences and series, there is no notation for limits of functions. The notion of convergence for real functions in Mizar BIB002 ) is defined using sequences as follows: The equivalence with (6) is proved in the particular case D = dom f \{x}. Mizar also formalizes notions of limit at infinity  ) and one-side limits  ). C-CoRN formalizes Definitions (6) and (8) for total functions and proves their equivalence. Limits for partial functions are not defined. Finally, in ACL2(r) and in the non-standard analysis library for Isabelle/HOL, limits are defined using non-standard real numbers: 4.2.3. Continuity The notion of continuity of function f at point x can be defined using the limit: lim y→x f (y) = f (x). This is the case for HOL4 and HOL Light. Continuity of f at x can also be defined using an ad-hoc predicate: PVS adapts this definition to partial functions and proves the preservation of continuity by basic operations BIB003 . In the Coq standard library, both variants are formalized and the equivalence is proved. Since the generic limit (7) is only defined for metric spaces and not vector spaces, continuity theorems (e.g. continuity of linear combination) have been proved only for the ad-hoc definition though. Definition (10) is the main one: it is used in most theorems that need some continuity hypothesis. As for limits, Mizar uses sequences to define continuity BIB006 : This definition is proved equivalent with (10) and with the topological version (2). ProofPower  goes the other way around: it uses Definition (10) and proves the equivalence with the sequence-based version of continuity (11). The case of C-CoRN is peculiar, since it formalizes constructive mathematics. As such, any function is naturally continuous. (Otherwise, given a discontinuous function, one could devise a way to decide equality between real numbers.) Therefore, having a predicate for continuity is useless; it is replaced by uniform continuity, which is formalized for partial functions on a closed interval [a; b] ⊆ dom f . 4.2.4. Differentiability For differentiability, Coq's standard library, PVS, and ProofPower  , use an ε-δ formula based on Newton's difference quotient: directly or through the limit definition. Note that, in Coq, there is no simple way to express the value = f (x) above. Indeed, the term derive pt f x is not a real number but a function that takes a proof that f is derivable at x and returns a real number. As a consequence, whenever one wants to write f (x) in a formula, one has to explicitly build a proof of differentiability beforehand and pass it BIB009 . In HOL4 and HOL Light, Newton's difference quotient is used too, but through their respective topological limit definitions ( (2) and (3)). Another approach is implemented in additional libraries of HOL Light: the Frechet derivative in a real normed vector space BIB008 BIB010 . In C-CoRN, as with continuity, the previous definition is modified to get a uniform differentiability on a closed interval  . In the non-standard analysis libraries of Isabelle/HOL BIB004 and ACL2(r) BIB005 , differentiability is defined by applying Definition (9) of limit to Newton's difference quotient. In all these formalizations, usual theorems such as the Mean Value Theorem and the Intermediate Value Theorem are proved.