在 Coq 中，证明解决数独或 Takuzu 等难题的函数的正确性的步骤是什么？

Question

证明解决谜题的函数（例如数独或卓祖）的正确性的一般步骤是什么？

Answer 1

我期望典型的“顺序难题”形式化由以下部分组成：

• 首先，定义板配置，无效（即没有/之前约束）和有效（满足所有约束）。

• 两个“求解器”函数，在给定有效的板配置的情况下：

  • 步进求解器：如果可能的话，进行一次移动（例如返回一个

    option

    ）；
  • 求解器：如果可能的话，通过多次移动找到解决方案。

• 以及相应的两个“检查器”功能：

  • 步骤检查器：检查棋盘配置（例如单步移动的结果）是否有效；
  • 解决方案检查器：作为步骤检查器加上检查板是否已满，即它是最终配置。

• 最后，为了证明正确性：

  • 步骤求解器正确：证明，给定任何有效的非结束配置，如果可能的话，步骤求解器会生成有效的新配置（即生成满足步骤检查的配置）；
  • 求解器正确：证明，给定任何有效的非结束配置，求解器会生成一个解决方案（如果有）。

通过考虑返回整套可能解决方案的求解器，或者更好的是，考虑使用一些回溯或其他类型的延续方案逐个“流”解决方案的求解器，该方案可能会变得更加复杂。

另一方面，一些简化是可能的：特别是，在像 Coq 这样的依赖类型的完整语言中，检查器可能会被省略（尽管在实践中这些检查器无论如何都是有用的，以验证数据），因为该语言让我们严格定义板配置（无效和有效），并且求解器（任何函数）保证返回符合声明的返回类型（是其实例）的结果。

对于具体示例，您可以查看以下实现进行比较/参考，请特别参阅“正确性定理”的自述文件：GitHub 上的 coq-community / sudoku