Formalizing Calculus without Limit Theory in Coq
Formal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to foun...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-06-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/9/12/1377 |
| _version_ | 1797530208225460224 |
|---|---|
| author | Yaoshun Fu Wensheng Yu |
| author_facet | Yaoshun Fu Wensheng Yu |
| author_sort | Yaoshun Fu |
| collection | DOAJ |
| description | Formal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to found a new form of calculus more easily but rigorously. This theory as an innovation differs from traditional calculus but is equivalent and more comprehensible. First, the definition of the difference-quotient control function is given intuitively from the physical facts. Further, conditions are added to it to get the derivative, and define the integral by the axiomatization. Then some important conclusions in calculus such as the Newton–Leibniz formula and the Taylor formula can be formally verified. This shows that this theory can be independent of limit theory, and any proof does not involve real number completeness. This work can help learners to study calculus and lay the foundation for many applications. |
| first_indexed | 2024-03-10T10:25:44Z |
| format | Article |
| id | doaj.art-c637f255ed3a41139e1b1b8ea01bb359 |
| institution | Directory Open Access Journal |
| issn | 2227-7390 |
| language | English |
| last_indexed | 2024-03-10T10:25:44Z |
| publishDate | 2021-06-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj.art-c637f255ed3a41139e1b1b8ea01bb3592023-11-22T00:02:05ZengMDPI AGMathematics2227-73902021-06-01912137710.3390/math9121377Formalizing Calculus without Limit Theory in CoqYaoshun Fu0Wensheng Yu1Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, ChinaBeijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, ChinaFormal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to found a new form of calculus more easily but rigorously. This theory as an innovation differs from traditional calculus but is equivalent and more comprehensible. First, the definition of the difference-quotient control function is given intuitively from the physical facts. Further, conditions are added to it to get the derivative, and define the integral by the axiomatization. Then some important conclusions in calculus such as the Newton–Leibniz formula and the Taylor formula can be formally verified. This shows that this theory can be independent of limit theory, and any proof does not involve real number completeness. This work can help learners to study calculus and lay the foundation for many applications.https://www.mdpi.com/2227-7390/9/12/1377calculusdifference-quotient control functionCoqformalizationlimit theory |
| spellingShingle | Yaoshun Fu Wensheng Yu Formalizing Calculus without Limit Theory in Coq Mathematics calculus difference-quotient control function Coq formalization limit theory |
| title | Formalizing Calculus without Limit Theory in Coq |
| title_full | Formalizing Calculus without Limit Theory in Coq |
| title_fullStr | Formalizing Calculus without Limit Theory in Coq |
| title_full_unstemmed | Formalizing Calculus without Limit Theory in Coq |
| title_short | Formalizing Calculus without Limit Theory in Coq |
| title_sort | formalizing calculus without limit theory in coq |
| topic | calculus difference-quotient control function Coq formalization limit theory |
| url | https://www.mdpi.com/2227-7390/9/12/1377 |
| work_keys_str_mv | AT yaoshunfu formalizingcalculuswithoutlimittheoryincoq AT wenshengyu formalizingcalculuswithoutlimittheoryincoq |