Coquelicot: A User-Friendly Library of Real Analysis for Coq
Coquelicot: A User-Friendly Library of Real Analysis for Coq
复制标题
DOI：
10.1007/s11786-014-0181-1
复制
发表时间：
2015-03-01
影响因子：
0.8
通讯作者：
Melquiond, Guillaume
中科院分区：
文献类型：
--
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
实际分析对许多应用程序普遍存在，仅仅是因为它是对物理或社会经济系统进行建模的合适工具。因此，在证明助手中保证其支持，因此用户可以正式验证关键系统的数学定理和正确性。 COQ系统带有标准实数的公理化和实际分析定理库。不幸的是，这个标准库缺乏一些广泛使用的结果。例如，功率系列的开发并不比其定义更进一步。此外，积分和衍生物的定义基于依赖类型，这使得它们在实践中特别繁琐。为了削弱这些不足之处，我们设计了一个用户友好的库：Coquelicot。通过依靠总功能代替限制类型，衍生品，积分，功率序列等，可以实现一种更简单的编写公式和定理语句的方法。为了帮助进行证明过程，该库带有一组全面的定理，不仅涵盖了这些概念，还涵盖了一些扩展，例如参数积分，二维可不同性，渐近行为。它还提供了一些自动化来执行可怜性证明。此外，Coquelicot是COQ标准库的保守扩展，我们在两个库之间提供对应定理。我们已经在几种用例上行使了图书馆：在大学入门级的考试中，贝塞尔功能的定义和属性以及解决一维波方程的解决方案。
Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, power series are not developed further than their definition. Moreover, the definitions of integrals and derivatives are based on dependent types, which make them especially cumbersome to use in practice. To palliate these inadequacies, we have designed a user-friendly library: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals, two-dimensional differentiability, asymptotic behaviors. It also offers some automation for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and we provide correspondence theorems between the two libraries. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation.