2

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

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

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

4

3 回答 3

5

对于 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。

于 2021-11-16T08:34:07.523 回答
3

我唯一想到的是 Isabelle/HOL 可以重放 SMT 证明（例如由 Z3 或 CVC4 生成），例如涉及整数和实数算术。对于计算机代数系统，我不知道任何可比的例子。

问题在于，计算机代数系统的设置方式往往不能为其简化输出详细的证书——如果他们能够做到这一点，人们可以尝试在定理证明器中重放它。但它必须超越纯粹的等式推理，因为许多规则（例如您的示例）需要证明不等式作为先决条件。

如果计算机代数系统能够将其计算的轨迹输出为使用的重写规则列表，包括如何证明它们的每个先决条件，原则上可以在定理证明器中重放这样的轨迹——但这当然会要求 CAS 使用的每条规则在定理证明器中都有对应的规则（这大致就是在 Isabelle 中重放 SMT 证明的工作方式）。但是，我不知道有这样的项目。

另一方面，有各种示例使用 CAS 来计算一些易于验证（但难以计算）的结果，例如分解多项式、分离实数多项式的根、Wilf-Zeilberger 见证，然后验证这在定理证明器中确实是一个有效的结果。但是，这并不涉及验证 CAS 的计算过程，只涉及结果。

于 2021-11-15T17:54:23.440 回答
2

出于演示目的，我准备了一个小型“假练习”，既说明验证计算的含义，也说明 Coq 中可用的最图形化的方法（这显示了你可以在 2021 年 11 月做的一些事情）。

它可以在github.com:ybertot/osxp_demos_coq的 github 上看到，尤其是文件sin_properties.v。

演示遵循以下路径：

  • 证明我们可以自动陈述和证明给出 PI 的“安全近似”的陈述（这是 Coq 库中数学常数的名称）。

  • 证明 Coq 可用于绘制一个已知的数学函数，在本例中是sin介于 0 和 PI 之间的函数。这依赖于gnuplot图形显示的连接。恐怕gnuplot不会包含在 M. Soegtrop 在另一个答案中提到的 Coq 平台中。

  • 显示我们也可以sin(1/x)使用 Coq 绘制函数函数 sin(1/x) 在 0.01 和 0.2 之间的正确图 （绘图实际上保存为github 存储库中的pdf 文件）

  • 证明通用函数绘图仪在这种情况下实际上返回了一个误导性的结果（通用函数绘图仪是gnuplot）。 函数 sin(1/x) 的不正确图，该线未达到应在 0.03 和 0.04 之间的值 1 误导性情节也在 github 存储库中作为 pdf 文件给出。

  • 下一步是证明我们可以证明某些计算的间隔保证，有时会自动使用该interval策略，有时该interval策略无法得出结论。这里的重点是该命令无法得出结论，而不是给出无法信任的答案。发生这种情况时，用户可以依靠知识和数学推理来获得所需的结果。该演示展示了如何证明对于x一定范围内的任意一个，该sin函数保证具有正值。

  • 下一步是证明sin x < x对于每个正数x，它表明数学推理可以依赖于各种数学技术：

    • 将区间分解为两部分，
    • 使用中值定理，
    • 计算的导数x - sin x（这可以在 Coq 中自动完成），
    • cos依赖于已知在 0 和 PI 之间严格递减的事实。

这只是一个简短的演示，它还旨在解释如何必须以不同于袖珍计算器的方式使用定理证明器，因为仅返回一个没有限定数学公式值的近似值是一个无法真正信任的过程。

原始问题还包括有关计算积分的问题。该interval软件包还包含此功能。

于 2021-11-16T10:09:41.923 回答