4

在使用 Isar 时，我发现了一个令人惊讶的行为（对我来说）。我尝试使用假设，有时 Isar 抱怨它无法解决未决目标，例如我最典型的示例是有一个假设但无法假设它：

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

尽管以下确实有效：

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

这并不奇怪。

但是下一个令我惊讶的是，鉴于我的第一个示例失败了，它可以工作：

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

为什么第一个和第二个不一样？

错误信息：

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (A) ⟹ A
4

1 回答 1

4

您可以在文档 Isar-ref 的“第 6 章：证明”中找到答案。理想情况下，您希望通读本章介绍以及第 6.1 和 6.2 节，以完全解决您的疑虑。下面，我介绍最相关的段落：

逻辑证明上下文由固定变量和假设组成。

...

类似地，引入一些假设 χ 有两个影响。一方面，创建了一个局部定理，可以在随后的证明步骤中用作事实。另一方面，χ ⊢ φ从上下文中导出的任何结果都变成有条件的。假设：⊢ χ ==> φ。因此，使用这样的结果解决封闭目标基本上会引入源自假设的新子目标。这种情况如何处理取决于使用的假设命令的版本：虽然假设坚持通过与目标的某个前提统一来解决子目标，但假设保持子目标不变，以便用户稍后证明。

让我们看一下您的第一个示例：

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

只有一个没有前提的子目标：A. 鉴于没有前提，“与前提的统一”是不适用的。

在第二个例子中，

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

子目标是A⟹A有前提的A。因此，您可以使用assume: 进行统一。

最后，

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

与前面的案例不同，因为你没有引入任何假设。因此，您可以使用show释放子目标。应该注意的from this show "A" by (simp)是，它等同于，from assms show "A" by simp或者更好的是from this show "A".：

lemma 
  assumes "A"
  shows "A"
proof -
  from assms show "A".
qed
于 2020-05-29T17:56:17.427 回答