isabelle - Isabelle/Isar 的假设语义是什么?
问题描述
在使用 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 节,以完全解决您的疑虑。下面,我介绍最相关的段落:
逻辑证明上下文由固定变量和假设组成。
...
类似地,引入一些假设 χ 有两个影响。一方面,创建了一个局部定理,可以在随后的证明步骤中用作事实。另一方面,
χ ⊢ φ
从上下文中导出的任何结果都变成有条件的。假设:⊢ χ ==> φ
。因此,使用这样的结果解决封闭目标基本上会引入源自假设的新子目标。这种情况如何处理取决于使用的假设命令的版本:虽然假设坚持通过与目标的某个前提统一来解决子目标,但假设保持子目标不变,以便用户稍后证明。
让我们看一下您的第一个示例:
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
推荐阅读
- sql-server - SQL 报表生成器:无法让数据集值出现在报表上
- popover - iOS 13 呈现 iOS 的模态半屏,iPadOS 的弹出框
- linux - 如果第一个字母不是字母,则使用 awk 将一个列值替换为另一个列值
- php - Laravel 从 5.6 升级到 Laravel 6
- laravel - 带有标头令牌的 volley Post 请求的问题
- jolt - Jolt:Json 字符串文字到 json 对象
- c# - 将 Google 工作表导出为 PDF 时如何访问参数
- javascript - JS Uncaught SyntaxError: Unexpected token :
- javascript - 使用 Promise 时重复 Mongoose 日志条目
- python - 我不明白我必须将什么“版本”v 作为日期格式