1

我想将这个证明转换为 Isar 作为 ab 练习（让我自己学习 Isar），只使用命题逻辑中的基本自然演绎规则 (ND)（例如notI, notE, impI, impE... 等）。

我可以很容易地在应用脚本中做到这一点：

lemma very_simple0: "A ⟶ A ∨ B"
  apply (rule impI) (* A ⟹ A ∨ B *)
  thm disjI1 (* ?P ⟹ ?P ∨ ?Q *)
  apply (rule disjI1) (* A ⟹ A *)
  by assumption

但我对 Isar 证明的尝试失败了：

lemma very_simple1: "A ⟶ A ∨ B"
proof (* TODO why/how does this introduce A by itself*)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

我的主要错误是：

Undefined method: "disjI1"⌂

这对我来说似乎很神秘，因为规则在之前的应用脚本中工作得很好。

我究竟做错了什么？

请注意，这也会导致错误：

lemma very_simple2: "A ⟶ A ∨ B"
proof impI
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

与上述相同的错误：

Undefined method: "impI"⌂

为什么？

编辑：

我了解到“方法”仍然需要工作rule impI，或者metis etc脚本仍然失败：

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by (rule disjI1)
  show "A ⟹ A" by assumption
qed

编辑2：

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  have 0: "A ⟹ A ∨ B" by (rule disjI1)
  have 1: "A ⟹ A" by assumption
  from 1 show "True" by assumption
qed

我仍然无法完成证明。

4

1 回答 1

2

你有几个问题。

让我们考虑这个例子：

have "A ⟹ A" by (rule disjI1)

那失败了，那么首先，定理 disjI1 实际上是什么？

thm disjI1
(* ?P ⟹ ?P ∨ ?Q *)

由于规则的工作原理，它尝试将目标“A”与“?P ∨ ?Q”匹配，但失败了。现在，如果您的目标具有正确的形式：

have "A ⟹ A ∨ B" by (rule disjI1)

有用！

第二个问题：

 proof

默认情况下等同于“证明标准”并默认应用一些定理。通常，您将使用“证明-”来应用无定理。

最后，让我们考虑一下您的示例

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)

在状态视图中，您会看到：

proof (state)
goal (1 subgoal):
 1. A ⟹ A ∨ B

这意味着 Isar 必须看起来像

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  show ‹A ∨ B›
    sorry
qed

显示有效的事实表明证明块具有正确的形式。

当心：这是一个重要的步骤，尤其是在开始时。总是从假设和表演开始。不要写其他任何东西。如果显示不起作用，则由 Isar 证明（假设和显示）诱导的结构与预期的证明（可以在状态面板中看到）不匹配。

你可以从那里做任何你想做的事情（包括开始一个新的证明块），但是你不能在不改变应用的规则的情况下改变那个结构。

让我们完成证明。我们想使用假设（所以我们添加 a then）和规则来证明目标。

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  then show ‹A ∨ B›
    by (rule disjI1)
qed

总的来说，我认为你应该阅读具体语义的 Isar 部分。

编辑：最重要的问题是您误解了 Isar 是什么：Isar 不是来帮助您完成不同的证明步骤（例如证明“A ==> A”）。在这里进行前向证明：您从假设（此处为 A）开始并得出结论。所以 Isar 证明看起来像

  assume A
  show "A \/ B"

您永远不必在证明中重复假设 A！

于 2020-05-12T16:06:50.077 回答