在Isabelle/HOL中的全称量化

Question

我注意到在使用Isabelle/HOL Isar时有几种处理全称量化的方法。我正在尝试以适合本科生理解和复制的方式编写一些证明（这就是我使用Isar的原因！），但我不确定如何以一种好的方式表示全称量化。

例如，在Coq中，我可以写forall x, P(x)，然后我可以说“induction 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)

有没有一种漂亮的证明模式可以表达普遍量化，而不需要我在归纳之前明确固定变量？

- Martin Copes

Answer 1

你可以使用 induct_tac，case_tac 等方法。这些是在正式的 Isar 中使用的 induct/induction 和 cases 方法的旧版变体。它们可以处理目标状态中绑定的元宇量化变量，例如你第二个示例中的 x：

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

induct_tac与induction相比的一个劣势是它不提供case，所以你不能只写 case (Suc x) 然后 from Suc.IH 和 show ?case 在你的证明中。另一个劣势是处理绑定变量通常非常脆弱，因为它们的名称通常是由Isabelle自动生成的，并且在Isabelle更改时可能会更改（当然不是在上面展示的情况下）。

这就是为什么现在偏爱Isar证明的原因之一。我强烈建议不要向你的学生展示“糟糕”的Isabelle，以便让他们更容易理解。

事实是：在Isabelle中的定理语句中的自由变量在逻辑上等同于全称量化变量，并且在你证明它之后，Isabelle将自动将它们转换为概要变量。这种约定不是Isabelle特有的；它在数学和逻辑中很常见，并且有助于减少杂乱的因素。特别是Isar试图避免在目标语句中显式使用⋀ 运算符（即have/show；它们仍然出现在assume中）。

或者，简而言之：定理中的自由变量默认情况下是全称量化的。我怀疑学生们会发现这很难理解；当我作为BSc学生开始使用Isabelle时，我肯定没有。事实上，我发现将定理陈述为xs @ (ys @ zs) = (xs @ ys) @ zs比∀xs ys zs. xs @ (ys @ zs) = (xs @ ys) @ zs更加自然。

- Manuel Eberl