Coq 中的定理 + 归纳 vs Fixpoint + destruct

如何解决Coq 中的定理 + 归纳 vs Fixpoint + destruct

在 Coq 中通过对一个前提的归纳使用 Theorem 证明的每个属性都可以重构为使用 Fixpoint 的证明，其中我们在同一前提下进行析构吗？为 Theorem 和 Fixpoint 设置单独的命令有什么意义？

解决方法

是的。当您调用 induction 策略时，它等效于 applying 归纳原理引理（称为 nat_ind 或 DatatypeName_ind 之类的东西），并且 Coq 自动证明了该归纳原理使用固定点和匹配。因此，如果您“内联”归纳原理的证明，您将得到一个可以由 Fixpoint 和 destruct 构造的证明。

然而，使用 Fixpoint 手动编写证明有点容易出错，因为它总是在与递归调用相对应的上下文中添加一个假设，并且该证明仅当您在参数上使用该假设时才有效来自destruct。该条件仅在最后的 Qed 时检查（您可以使用 Guarded 命令检查这一点，但这需要提前正确地知道递归参数，可能使用 {struct x} 声明） .因此，如果您使用 Fixpoint 编写证明，然后调用 eauto 之类的策略，则该策略可能会“意外地”以没有根据的方式使用递归参数。如果使用 induction，则只能得到直接子项的归纳假设，因此通过策略构造的证明始终有效。