3

我有以下简单的证明：

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

在证明状态下，伊莎贝尔说：

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

但是之后：

无法应用初始证明方法⌂：使用此方法：n < a n < b 目标（1 个子目标）：1. n * n < a * b

问题是什么？。实际上，我对完成专业的实际单个步骤感兴趣，所以我认为伊莎贝尔可以告诉我方法。

4

1 回答 1

4

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。

哦，顺便说一句：您得到 a 但随后出现错误消息的事实是Successful attempt to solve goal交互式 Isabelle 的非线性性质的结果：当您编写 aby时，证明尝试被分叉到后台和证明文档的处理之后继续进行，就好像证明成功了一样。这是为了允许并行化并允许用户在某些证明被破坏的情况下继续处理文档。

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

于 2016-11-16T07:08:57.230 回答