归纳证明中的自由类型变量

Question

在尝试通过归纳法证明有关函数的引理时，我遇到了自由类型变量的问题。在我的归纳假设中，延续是一个 schematic 变量，但它的类型涉及一个 free 类型变量。因此，当我尝试应用 i.h 时，Isabelle 无法将类型变量与具体类型统一。我编造了这个最小的例子：

fun add_k :: "nat ⇒ nat ⇒ (nat ⇒ 'a) ⇒ 'a" where
"add_k 0 m k = k m" |
"add_k (Suc n) m k = add_k n m (λn'. k (Suc n'))"

lemma add_k_cps: "∀k. add_k n m k = k (add_k n m id)"
proof(rule, induction n)
  case 0  show ?case by simp
next
  case (Suc n)
  have "add_k (Suc n) m k = add_k n m (λn'. k (Suc n'))" by simp
  also have "… = k (Suc (add_k n m id))" 
      using Suc[where k="(λn'. k (Suc n'))"] by metis
  also have "… = k (add_k n m (λn'. Suc n'))"
      using Suc[where k="(λn'. Suc n')"] sorry (* Type unification failed *)
  also have "… = k (add_k (Suc n) m id)" by simp
  finally show ?case .
qed

在"sorry step"中，原理图变量?k的显式实例化失败

Type unification failed

Failed to meet type constraint:

Term:  Suc :: nat ⇒ nat
Type:  nat ⇒ 'a

因为 'a 是免费的，不是原理图。如果没有实例化，简化器无论如何都会失败，我找不到其他可行的方法。

由于我无法量化类型，我看不出如何在证明中制作 'a 原理图。当一个术语变量在证明中局部成为示意图时，为什么它的类型中的变量不是这种情况？在引理被证明之后，它们无论如何都成为理论层面的示意图。这似乎非常有限。将来是否可以选择执行此操作，或者是否存在某些固有限制？或者，是否有一种方法可以避免这个问题并仍然在已证明的引理中保持连续的示意性多态性？

Answer 1

这是归纳法在 HOL 中的固有限制。归纳是HOL中的一个规则，所以归纳假设中的任何类型都不可能泛化。

针对您的问题的专门解决方案是首先证明

lemma add_k_cps_nat: "add_k n m k = k (n + m)"
  by (induction n arbitrary: m k) auto

然后证明add_k_cps.

一般方法是：首先证明固定类型的实例，归纳法适用于这些实例。在示例中，是 nat 的归纳。然后推导出在类型本身中推广的证明。

Answer 2

当从类型变量已固定的块中导出定理时，自由类型变量将成为定理中的示意图。特别是，您无法量化块中的类型变量，然后在块中实例化类型变量，就像您在归纳中尝试做的那样。对类型的任意量化导致 HOL 中的不一致，因此改变这一点的希望很小。

幸运的是，有一种方法可以在不进行类型量化的情况下以 CPS 方式证明你的引理。问题是你的语句不够笼统，因为它包含id。如果你概括它，那么证明有效：

lemma add_k_cps: "add_k n m (k ∘ f) = k (add_k n m f)"
proof(induction n arbitrary: f)
  case 0  show ?case by simp
next
  case (Suc n)
  have "add_k (Suc n) m (k ∘ f) = add_k n m (k ∘ (λn'. f (Suc n')))" by(simp add: o_def)
  also have "… = k (add_k n m (λn'. f (Suc n')))" 
    using Suc.IH[where f="(λn'. f (Suc n'))"] by metis
  also have "… = k (add_k (Suc n) m f)" by simp
  finally show ?case .
qed

如果您选择 f = id，您会得到原来的定理。

归纳证明中的自由类型变量

Free type variables in proof by induction

isabelle