proof - Isabelle/HOL 中的通用量化

Question

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

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

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

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

lemma foo: \<And>x. P(x)
proof -
fix x
show "P(x)"
proof (induct x)

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

Answer 1

您可以使用 induct_tac , case_tac等。这些是 induct 的旧变体/induction和 cases在适当的 Isar 中使用的方法。它们可以在目标状态下对绑定(bind)的元通用量化变量进行操作，例如 x在你的第二个例子中:

lemma foo: "⋀x. P(x :: nat)"
proof (induct_tac x)

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

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

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

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