key: cord-0047239-resa6iqv authors: Fu, Yaoshun; Yu, Wensheng title: A Formalization of Properties of Continuous Functions on Closed Intervals date: 2020-06-06 journal: Mathematical Software - ICMS 2020 DOI: 10.1007/978-3-030-52200-1_27 sha: a4d63f60e041a17162bf22ea443690db51830716 doc_id: 47239 cord_uid: resa6iqv Formal mathematics is getting increasing attention in mathematics and computer science. In particular, the formalization of calculus has important applications in engineering design and analysis. In this paper, we present a formal proof of some fundamental theorems of continuous functions on closed intervals based on the Coq proof assistant. In this formalization, we build a real number system referring to Landau’s Foundations of Analysis. Then we complete the formalization of the basic definitions of interval, function, and limit and formally prove the theorems including completeness theorem, intermediate value theorem, uniform continuity theorem and others in Coq. The proof process is normalized, rigorous and reliable. Analysis is one of the greatest achievements in the history of mathematics. The achievement opens a new era of mathematical progress and plays an important role in development of physics, astronomy, signal processing and other disciplines. Analysis which evolved from calculus is a branch of mathematics that studies limits and related theories [12] . At the end of the 19th century, mathematicians deduced many properties of continuous functions on closed intervals, which undoubtedly promoted the development of analytical theory. There are some important properties of continuous functions on closed intervals including Weierstrass second theorem: Boundedness theorem, Weierstrass first theorem: Extreme value theorem, Bolzano-Cauchy second theorem: Intermediate value theorem, Cantor theorem: Uniform continuity theorem. Bolzano's Function Theory gives the earliest proofs of the Boundedness theorem and the Extreme value theorem (but published some 100 years later) [15] , and Weierstrass proved the Extreme value theorem in Berlin lecture. The Intermediate value theorem was first proved in 1817 by Bolzano, and then Cauchy [7] gave a proof in 1821. The definition of uniform continuity is proposed by Heine, and he published a proof of the Uniform continuity theorem. With the further research of limits by mathematicians, the establishment of a rigorous and complete system of real numbers theory has become a key issue. In 1872, three major real numbers theories appeared in Germany: Dedekind cut theory, Cantor-Henie-Meray "basic sequence" theory, and Weierstrass "bounded monotone sequence" theory. Among them, the Dedekind cut is particularly recognized, and it is called the creation of human intelligence that does not rely on the intuitiveness of space and time. Then Peano established a natural number theory through a set of axioms, thereby solving the core problems of rational number theory and also the basic problems of real number theory. In recent years, with the rapid development of computer science, especially the emergence of proof assistant Coq, Isabelle and HOL Light and so on [2, 4, 8, 10, 14, 17] , formal proof of mathematical theorems has made great progress. In 2005, the international computer experts Gonthier and Werner provided the formal proof in Coq of the famous "four-color theorem" successfully [5] . After years of hard work, Gonthier again achieved the machine proof in Coq of the "odd order theorem" in 2012 [6] . Those progress make Coq more and more popular in academia. Wiedijk pointed out that relevant research teams around the world have completed or plan to formalize the proof of theorems such as Gödel's first incompleteness theorem, Jordan curve theorem, Prime theorem and Fermat last theorem of a hundred well-known mathematical theorems [17] . Based on "Real number theory" formal system, we formalize the properties of continuous functions on closed intervals. Moreover, we give formal proofs of these theorems, which include the Boundedness theorem, the Extreme value theorem, the Intermediate value theorem, the Uniform continuity theorem. It should be noted that the properties of continuous functions on closed intervals is an important theorem in analysis. The structure of this article is as follows: In Sect. 2, we introduce the "real number theory" machine proof system. In Sect. 3, we present the formal definition of the function limit and related properties. In Sect. 4, we discuss the machine proof of the properties of continuous functions on closed intervals in detail, which are derived by supremum theorem. In Sect. 5, we draw conclusions and discuss some potential further work. Before formally proving the properties of continuous functions on closed intervals, we first need to build a formal system of real number theory. van Benthem Jutting [1] completed the formalization in Automath of Landau's "Foundations of Analysis", which was a significant early progress in formal mathematics. Harrison [9] presents formalized real numbers and differential calculus on his HOL Light system. The definition of real numbers in Coq standard library uses the axiomatic way, and based on this, excellent real analysis library Coquelicot [3] has been established. This library accomplishes many achievements, but its definition of real number is non-constructive. Hornung [11] completed the first four chapters of the "Foundations of Analysis" in Coq, which is closed related to our work, however our system is closer to the expression of Landau and more readable. We also completed the complex number part and proved equivalence between eight completeness theorems of real number. There are several ways to define natural numbers in Coq. Based on Morse-Kelley axiomatic set theory, it is designed to give quickly and naturally a foundation for mathematics, and meanwhile deduce the Peano axioms as theorems [16, 18] . If we start from the more higher type rather than set theory, we can formalize straight Peano axioms as follows: Parameter Nat :Type. Axiom One :Nat. Notation "1" := One. Axiom Successor :Nat -> Nat. Notation " x ' " := (Successor x)(at level 0). Based on this, we can use "Parameter" and "Axiom" to define natural number related functions such as addition and multiplication. This way is intuitive but not elegant. The natural numbers defined by "Inductive" can recursively define natural number related functions. Landau's "Foundations of Analysis" [13] is based on naive set theory and some basic logic. Starting from the Peano axioms, natural numbers (positive integers), fractions (positive), rational numbers/integer (positive) are defined in order. The real number, defined by Dedekind cut, defines complex numbers through real numbers for constructing systematically the whole number system theory. We have completed the Coq formalization of the system, and the complete source is available online: https://github.com/coderfys/analysis/ In this system, we can prove Dedekind fundamental theorem, and derive Supremum theorem. The proof details are not described, and the formalization is as follows. Divide all real numbers into two classes, so that the first class and second class are not empty, and each number in the first class is less than each number in the second class. Then there is a unique real number E, so that any number less than E belongs to the first class, and any number greater than E belongs to the second class. Section Dedekind. Variables Fst Snd :Ensemble Real. Definition R_Divide := ∀ r, r ∈ Fst \/ r ∈ Snd. Definition ILT_Class := ∀ e f, e ∈ Fst -> f ∈ Snd -> e < f. Theorem DedekindCut : ∀ Fst Snd, R_Divide Fst Snd -> No_Empty Fst -> No_Empty Snd -> ILT_Class Fst Snd -> ∃ E, Split Fst Snd E. If a non-empty real number set has a upper bound, then there must be a least bound (the Supremum as an example). Definition bound_up y A := ∀ z, z ∈ A -> z ≤ y. Definition supremum y A := bound_up y A /\ ∀ z, bound_up z -> y ≤ z. Theorem SupremumT : ∀ R, No_Empty R -> ∃ x, bound_up x R -> ∃ y, supremum_s y R. The formal definition of functions in this system is as follows: Definition Fun := Real -> Real. Definition FunDot_con (f : Corollary Pr_FunDot : The function f (x) is continuous (left, right) at a point, then the function f (x) is locally bounded at this point (take right continuous for example): In this real number system, division function requires three parameters, and the third of which is the proof that the second is not 0. Therefore, the "NoO N" above means "2 = 0". and is not everywhere 0, then 1 f (x) is continuous on (take f (x) > 0 as an example). Continuous functions have four fundamental properties on closed intervals: Boundedness theorem (Weierstrass second theorem), Extreme value theorem (Weierstrass first theorem), Intermediate value theorem (Bolzano-Cauchy second theorem), Uniform continuity theorem (Cantor theorem). These theorems are the basis of mathematical analysis and the direct expression of real number theory in functions. Our formalizations rely on a logical axiom law of excluded middle. Definition z ∈ (a, b) . The notation "[x0| − δ]" below represents U x0 (δ) in mathematics. Lemma L1 : ∀ f a b, FunClose_con f a b -> ∀ x0, x0 ∈ (a,b) Upper bound: Construct a real number set {t : f (x) has an upper bound on [a, t]}. The formal definition is as follows: is right continuous at the point a, there exists δ > 0, and f (x) has an upper bound on (a, a+δ), when b ≤ a+δ proves the proposition. When a+δ < b, R is not empty. On the other hand, b is an upper bound of R obviously, so R has supremum ξ, and ξ ≤ b. Case 1(ξ < b): According to Lemma L1, there exists δ 1 > 0, and f (x) has an upper bound on (a, ξ + δ 1 ). The proposition is proved when b < ξ + δ 1 . When ξ + δ 1 ≤ b, there is ξ + δ 1 ∈ R, which contradicts ξ is the supremum of R. Lower bound: According to the lemma Pr fun1, it can be deduced that −f (x) is continuous on [a, b] . From Theorem T1, we know that −f (x) has the upper bound "up", then "-up" is the lower bound of f (x) on [a, b]. Theorem T2 : ∀ f a b, FunClose_con f a Maximum value: Construct a real number set {f (x) : x ∈ [a, b]}. The formal definition is as follows: First, we prove a lemma L3: if f (x) is left continuous at point b, a < b and f (b) > C, then there is z between a, b, satisfies f (z) > C. The formal definition is as follows: In summary, R is not empty and b is an upper bound of R, so R has a supremum ξ, and ξ ≤ b. When ξ = b, it can deduce contradiction according to Pr supremum and L3. Therefore ξ ∈ (a, b) . for any x ∈ [ξ − δ, ξ + δ], which can be deduced f (x) < C. Further, we can conclude that (ξ + δ) ∈ R which contradicts ξ is the supremum of R. Case 2(f (ξ) > C): f (x) is continuous at point ξ, hence f (x) is left continuous at point ξ. By L3 there must exist z ∈ (a, ξ) and f (z) > C, so z is the upper bound of R, which contradicts ξ is the supremum of R. f (a) > f(b): Refer to T1', T2' proof. Definition Un_Con f a b : Let f (x) be continuous on [a, b], fix any > 0. we construct a real number set {t : ∃δ > 0 and |f (x 1 ) − f (x 2 )| < when x 1 , x 2 ∈ [a, t] and |x 1 − x 2 | ≤ δ}. The formal definition is as follows: Because f (x) is right continuous at point a, there must exists δ 1 > 0, and |f (x) − f (a)| < 2 for any x ∈ [a, a + δ 1 ). Let δ 2 = min(a + δ1 2 )(b − a), we prove that a+δ 2 ∈ R. Obviously, b is an upper bound of R, So R has a supremum ξ and ξ ≤ b. As f (x) is continuous at point ξ, there exists δ > 0, and |f (x) − f (ξ)| < 2 for any x ∈ [ξ − δ, ξ + δ]. Further, we can deduce |f (x 1 ) − f (x 2 )| < for any x 1 , x 2 ∈ [ξ − δ, ξ + δ]. Therefore, |f (x 1 ) − f (x 2 )| < for any x 1 , x 2 ∈ [a, ξ + δ] and |x 1 − x 2 | ≤ δ. Case 1(ξ < b): When b < ξ + δ, the proposition is proved due to the arbitrariness of . When ξ + δ ≤ b, we further prove ξ + δ ∈ R, which contradicts ξ is the supremum of R. Case 2(ξ = b): b < ξ + δ, the proposition is proved by the arbitrariness of . This paper formalizes limits, continuous functions and related theorems. These theorems include Boundedness theorem, Extreme value theorem, Intermediate value theorem, and Uniform continuity theorem. We have completed their formal proofs based on the real number theory system developed by ourselves. In the future, we will formalize more theorems of continuous functions and make meaningful attempts for formal work in the fields of real analysis and complex analysis. We are grateful to the anonymous reviewers, whose comments much helped to improve the presentation of the research in this article. Checking Landau's "Grundlagen" in the AUTOMATH System Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions Coquelicot: a user-friendly library of real analysis for Coq Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant Formal proof-the four-color theorem A machine-checked proof of the odd order theorem Who gave you the epsilon? Cauchy and the origins of rigorous calculus Formal proof Theorem Proving with the Real Numbers Formal proof-theory and practice A History of Mathematics Foundations of Analysis: The Arithmetic of Whole, Rational, Irrational, and Complex Numbers Isabelle/HOL Bolzano and uniform continuity A formal system of axiomatic set theory in Coq Formal proof-getting started Machine Proof System of Axiomatic Set Theory