isabelle - 伊莎贝尔的不平等推理

我有以下简单证明：

lemma
    fixes a b n :: nat
    assumes a: "a > n" "b > n"
    shows "a*b > n*n"
proof -
    from assms show "a*b > n*n" by(simp_all add: field_simps)  ERROR
qed

在证明状态下，Isabelle说：


通过导出规则成功解决目标的尝试：
n * n

但是之后：


无法应用初始证明方法⌂：使用此方法：
n n 1. n * n

问题是什么？。实际上，我对执行该proff的实际单个步骤很感兴趣，因此我Hardt Isabelle可以向我展示方法。

最佳答案

field_simps对于重新排列术语很有用，但对于这种推理而言却不太好。当您想证明这样的事情时，通常需要一个好的规则。在这种情况下，关于（严格）不等式和乘法。

如果您有一些看似微不足道的东西，但是您不知道如何准确地证明它和/或您不知道在Isabelle中所称的相关事实，sledgehammer通常会有所帮助：

from assms show "a*b > n*n"
  sledgehammer

  > Sledgehammering...
  > Proof found...
  > "cvc4": Try this:
  >   by (metis (no_types, lifting) dual_order.strict_trans gr_implies_not_zero
  >         linorder_neqE_nat mult.commute nat_0_less_mult_iff
  >         nat_mult_less_cancel1) (796 ms)

如您所见，sledgehammer发现的证明的问题在于，它们通常很长，很慢，而且照亮度不高。从维护的角度来看，它们也有些脆弱。背景理论的变化。尽管如此，这仍然是一个不错的起点，您通常可以从大锤打样（例如此处的nat_mult_less_cancel1）中阅读有关打样的事实。

查找相关事实的另一种方法是find_theorems命令，或者等效地，是Isabelle / jEdit IDE中的“查询”面板。如果你这样做

find_theorems "_ * _ > _ * _"

或者等价地，在“查询”面板中输入_ * _ > _ * _，您将获得大量输出以进行阅读，但某些相关事实隐藏在该输出的末尾，例如mult_strict_mono'：

thm mult_strict_mono'
> ?a < ?b ⟹ ?c < ?d ⟹ 0 ≤ ?a ⟹ 0 ≤ ?c ⟹ ?a * ?c < ?b * ?d

您的证明如下所示：

from assms show "a*b > n*n"
  by (rule mult_strict_mono') simp_all

simp_all仅履行剩余的证明义务n ≥ 0。

哦，顺便说一句：您得到Successful attempt to solve goal但随后出现错误消息的事实是交互式Isabelle的非线性性质的结果：当您编写by时，证明尝试会分叉到背景中，之后，证明文件的处理就好像证明已经成功一样。这是为了允许并行化并允许用户即使在某些证明已损坏的情况下也可以继续处理文档。

Successful attempt消息来自Isabelle的一部分，该部分在show之后被调用，并且该部分看到了成功的（但仍在等待中的）a*b > n*n证明。但是，您随后立即从by (simp_all …)收到一条错误消息，指出证明方法失败。在批处理模式下，诸如此类的故障更加严重（并且更加明显）。

关于isabelle - 伊莎贝尔的不平等推理，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40623339/