使用 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
最佳答案
您可以在文档 Isar-ref 的“第 6 章:证明”中找到答案。理想情况下,您希望通读本章的介绍以及第 6.1 和 6.2 节以完全解决您的疑虑。下面,我介绍最相关的段落:
The logical proof context consists of fixed variables and assumptions.
...
Similarly, introducing some assumption χ has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent proof steps. On the other hand, any result
χ ⊢ φ
exported from the context becomes conditional wrt. the assumption:⊢ χ ==> φ
. Thus, solving an enclosing goal using such a result would basically introduce a new subgoal stemming from the assumption. How this situation is handled depends on the version of assumption command used: while assume insists on solving the subgoal by unification with some premise of the goal, presume leaves the subgoal unchanged in order to be proved later by the user.
让我们看看你的第一个例子:
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
关于isabelle - Isabelle/Isar 的假设语义是什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/62090372/