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

Question

手动或由计算机代数系统执行的符号计算可能有错误或仅在某些假设条件下成立。一个典型的例子是 sqrt(x^2) == x 这在一般情况下是不正确的，但如果 x 是实数且非负，它确实成立。

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

更新:更具体地说，知道是否有微积分和线性代数中的本科作业示例可以正式解决(可能在证明助手的帮助下)，以便解决方案可以由证明检查器自动验证，这将很有趣.精益的一个非常简单的示例分配是 here .

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。