Formalizing Calculus without Limit Theory in Coq

Yaoshun Fu and Wensheng Yu
Additional contact information
Yaoshun Fu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China
Wensheng Yu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China

Mathematics, 2021, vol. 9, issue 12, 1-24

Abstract: 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.

Keywords: calculus; difference-quotient control function; Coq; formalization; limit theory (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2021
References: View complete reference list from CitEc
Citations: View citations in EconPapers (2)

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/12/1377/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/12/1377/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:9:y:2021:i:12:p:1377-:d:574636

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().