3

我正在尝试按照本文档（特别是幻灯片 23）在 Isabelle 中进行基本的自然演绎证明。

我知道我可以做类似的事情

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ B› have ‹B› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ B) ⟶ A ⟶ B› ..
qed

但是也

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ B› and ‹A›
  then obtain ‹B› ..
qed

达到相同的目标。

所以当我尝试写证明时

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ A ⟶ B› have ‹A ⟶ B› ..
      hence ‹B› using ‹A› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B› ..
qed

喜欢

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
qed

伊莎贝尔为什么抱怨

Failed to finish proof:
goal (1 subgoal):
 1. A ⟶ A ⟶ B ⟹ A ⟶ B

我知道这些是 Isabelle 可以一步证明的非常简单的事情：这里的目标是生成一个人类可读的简明证明（在自然演绎的范围内），而无需咨询 Isabelle。

4

1 回答 1

0

对您的证明的这种修改有效：

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then show ‹B› using ‹A› ..
qed

问题是双重的：

  1. 证明块的打开会根据您要证明的目标的形状自动应用“标准”引入规则。在您的情况下，这是暗示介绍，即 theorem impI。问题是你只应用了一次，这给你留下了假设A -> A -> B和剩余的目标A -> B。因此，您还没有假设A您拥有的假设，因为这需要第二次使用impI才能获得。相反，通过使用，proof(intros impI)我告诉 Isabelle 在证明的第一步中不要使用其标准的引入和消除规则集，而是impI尽可能多地应用引入规则（即两次）。或者，proof(rule impI, rule impI)在这里也可以达到相同的效果。
  2. 其次，你的最后一行then obtain，没有完成证明：你show什么都没有！通过使用显式show，您向 Isabelle 发出信号，表明您想要“完善”一个开放目标，并实际得出结论，您在区块开始时要证明的内容是什么。

请注意，如果您obtain的唯一目标是推导出. 问题是你试图从事实出发，在完善开放目标的同时推导出新的事实。例如，这也有效：A -> BAB

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
  then show ‹B› .
qed

其中事实B是在第一行获得的，第二行简单地使用这个事实来细化开放目标B。

于 2018-11-23T08:52:12.577 回答