如何使用 get 使前向消除证明更易于阅读？

Question

我正在按照this document（特别是幻灯片 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。

Answer 1

对你的证明的修改有效：

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. 证明块的打开会根据您要证明的目标的形状自动应用“标准”引入规则。在您的情况下，这是暗示介绍，即定理impI。问题是你只应用了一次，这让你有了假设A -> A -> B，剩下的目标A -> B。因此，您还没有假设A，因为这需要第二次使用impI 才能获得。相反，通过使用proof(intros impI)，我告诉 Isabelle 在证明的第一步不要使用其标准的引入和消除规则集，而是尽可能频繁地应用impI 引入规则（即两次）。或者，proof(rule impI, rule impI) 也可以在这里发挥同样的效果。
2. 第二，从then obtain 开始，你的最后一行没有完成证明：你不是showing 任何东西！通过使用明确的show，您是在向 Isabelle 发出信号，表示您想“完善”一个开放的目标，并实际得出结论，您要在区块开始时证明它是什么。

请注意，如果您的唯一目标是派生B，那么您在此处使用obtain 来从事实A -> B 和A 向前推进是不正确的。问题是你正试图从事实出发，在完善开放目标的同时推导出新的事实。例如，这也有效：

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。