Trung tâm cá nhân
sách gpt4 ai đã đi

proof - Isabelle/HOL 中的通用量化

In lại 作者：行者123 更新时间：2023-12-04 19:02:27 27 4
mua khóa gpt4 Nike

我注意到，在使用 Isabelle/HOL Isar 时，有几种方法可以处理通用量化。我正在尝试以适合本科生理解和重现的风格编写一些证明(这就是我使用 Isar 的原因!)，我对如何以一种好的方式表达全称量化感到困惑。

例如，在 Coq 中，我可以写 forall x, P(x)然后我可以说“归纳 x”，它会根据相应的归纳原理自动生成目标。然而，在 Isabelle/HOL Isar 中，如果我想直接应用归纳原理，我必须在没有任何量化的情况下陈述定理，如下所示:

lemma foo: P(x)
proof (induct x)

这很好用，因为 x 被视为示意图变量，就好像它被普遍量化了一样。然而，它在陈述中缺乏普遍的量化，这不是很有教育意义。我获得资金的另一种方式是使用 \Và \ .但是，如果我以这种方式陈述引理，我不能直接应用归纳原理，我必须首先修复普遍量化的变量......从教育的角度来看，这似乎也不方便: 
lemma foo: \x. P(x)
proof -
fix x
show "P(x)"
proof (induct x)

什么是表达普遍量化的好证明模式，不需要我在归纳之前明确地修复变量？

1 Câu trả lời

Bạn có thể sử dụng induct_tac , case_tac等。这些是 induct 的旧变体/inductionVà cases在适当的 Isar 中使用的方法。它们可以在目标状态下对绑定(bind)的元通用量化变量进行操作，例如 x在你的第二个例子中:

lemma foo: "⋀x. P(x :: nat)"
proof (induct_tac x)
induct_tac 的一个缺点超过 induction是它不提供案例，所以你不能只写 case (Suc x)Sau đó from Suc.IHVà show ?case在你的证明中。另一个缺点是寻址绑定(bind)变量通常相当脆弱，因为它们的名称通常由 Isabelle 自动生成，并且可能在 Isabelle 更改时更改。 (当然不是你上面显示的情况)

这就是如今 Isar 证明受到青睐的原因之一。我强烈建议不要向学生展示“坏”伊莎贝尔，目的是让他们更容易理解。

事实是这样的:Isabelle 中定理语句中的自由变量在逻辑上等同于全称量化变量，并且 Isabelle 在您证明之后自动将它们转换为示意图变量。这个约定并不是 Isabelle 独有的；它在数学和逻辑中很常见，它有助于减少困惑。 Isar 特别试图避免显式使用 ⋀目标语句中的运算符(即 have/ trình diễn ；它们仍然出现在 assume 中)。

或者，简而言之:定理中的自由变量在默认情况下是普遍量化的。我怀疑学生会觉得这很难理解；当我开始与 Isabelle 作为 BSc 学生一起学习时，我当然没有。事实上，我发现将定理表述为 xs @ (ys @ zs) = (xs @ ys) @ zs 更为自然。而不是 ∀xs ys zs. xs @ (ys @ zs) = (xs @ ys) @ zs .

关于proof - Isabelle/HOL 中的通用量化，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/34486551/

27 4 0
Bài viết được đề xuất: laravel - 如何更改最大文件大小的 Laravel 验证消息(以 MB 而不是 KB 为单位)？
Bài viết được đề xuất: shell - 防止 POSIX xargs 尝试运行空命令
Bài viết được đề xuất: javascript - 并行触发异步请求，但使用 rxjs 按顺序获取结果
Bài viết được đề xuất: R，knitr，pander - 如何很好地格式化日期的摘要()
行者123
Hồ sơ cá nhân

Tôi là một lập trình viên xuất sắc, rất giỏi!

Nhận phiếu giảm giá Didi Taxi miễn phí
Mã giảm giá Didi Taxi
Các bài viết nóng hổi trên toàn bộ trang web
Giấy chứng nhận ICP Bắc Kinh số 000000
Hợp tác quảng cáo: 1813099741@qq.com 6ren.com