coq - 证明助手中的认证计算

Question

手动或通过计算机代数系统执行的符号计算可能是错误的，或者仅在某些假设下才成立。一个经典的例子是sqrt(x^2) == x一般不正确，但如果x是真实的且非负的，它确实成立。

是否有使用 Coq、Isabelle、HOL、Metamath 或其他证明助手/检查器来证明符号计算正确性的示例？特别是，我对微积分和线性代数示例感兴趣，例如求解定积分或不定积分、微分方程和矩阵方程。

更新： 更具体地说，有兴趣知道是否存在可以正式解决（可能在证明助手的帮助下）的微积分和线性代数本科作业的示例，以便解决方案可以通过自动验证证明检查器。一个非常简单的精益作业示例在这里。

标签： coqisabelletheorem-provingproof-of-correctnesshol

Answer 1

对于 Coq 证明助手，有几个库可以提供帮助。Coquelicot（ https://gitlab.inria.fr/coquelicot/coquelicot ）非常符合您的要求。Coquelicot 团队进行了一项练习，并参加了法国中学文凭考试——我想说这更像是一所大学而不是高中数学考试——并完成了大部分练习的证明。可以在此处的示例中找到证明（https://gitlab.inria.fr/coquelicot/coquelicot/-/tree/master/examples）。我想把练习和解决方案翻译成英文。

但这是几年前的事了，同时针对特定应用程序有非常强大的工具。例如，有一个 coq-interval ( https://gitlab.inria.fr/coqinterval/interval )，它完全自动地对相当复杂的不等式进行 Coq 证明，比如高阶多项式在某个区间内与某个最大值匹配一个正弦函数偏差。它通过泰勒分解和计算残差的上限来做到这一点。它还可以对各种数值积分进行错误证明。最近添加的一项新功能是能够进行经过验证的正确绘图。

在 Coq 中证明无限精度实数和浮点计算之间的误差的工具是 Gappa ( https://gitlab.inria.fr/gappa/gappa )。

另一个非常有趣的 Coq 开发是 CoRN ( https://github.com/coq-community/corn )，它是 Coq 中构造实数的形式化。建设性实数是可以计算的真实实数。本质上，建设性实数是一种算法，可以将数字计算到任何所需的精度，并证明该算法具有收敛性。可以证明这样的数字满足实数的所有通常性质。构造实数的一个有趣的副作用是它们只需要 LPO 作为公理，而在经典实数中，实数的存在本身就是一个公理。您在 CoRN 中进行的任何计算，例如 pi>3，都会自动被证明是正确的。

所有这些工具都包含在 Coq 平台中，这是 Coq 证明助手的通用发行版。

还有更多，而且还在稳步增加。我想说，在不久的将来，我们有一个可用的、经过验证的正确 CAS。