Isabelle/HOL中的通用量化

我注意到,在与Isabelle/HOL Isar合作时,有几种方法可以处理通用量化问题.我正在尝试以适合本科生理解和复制的风格写出一些证据(这就是我使用Isar的原因!)而且我对如何以一种很好的方式表达普遍量化感到困惑.

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

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

这样可以正常工作,因为x被视为一个原理图变量,就像它被普遍量化一样.但是,它在声明中缺乏普遍的量化,而这种量化并不是很有教育意义.我资助的另一种方式是使用\和\.但是,如果我以这种方式陈述引理,我不能直接应用归纳原理,我必须首先修复普遍量化的变量......从教育的角度来看,这似乎很不方便:

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

什么是表达通用量化的一个很好的证明模式,不需要我在归纳之前明确地修复变量？

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

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

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

这就是为什么Isar样张最近成为首选的原因之一.我强烈建议不要向学生展示你的"坏"伊莎贝尔,以便他们更容易理解.

事实如下:Isabelle定理陈述中的自由变量在逻辑上等同于普遍量化的变量,Isabelle在您证明了它之后自动将它们转换为逻辑示意图变量.这个惯例并不是伊莎贝尔所独有的; 它在数学和逻辑中很常见,它有助于减少混乱.Isar特别试图避免?在目标语句中明确使用运算符(即have/ show;它们仍然出现在assume)中.

或者,简而言之:默认情况下,定理中的自由变量是普遍量化的.我怀疑学生会发现这很难理解; 当我开始与Isabelle作为BSc学生时,我当然没有.事实上,我发现用一个定理来xs @ (ys @ zs) = (xs @ ys) @ zs代替它更自然?xs ys zs. xs @ (ys @ zs) = (xs @ ys) @ zs.