Isabelle 自动证明器适用于引理，取决于引理的特殊情况

Question

为什么第二个引理的“自动”证明挂起？第二个引理是第一个引理的特例。

  primrec ListSumTAux :: "nat list ⇒ nat ⇒ nat" where
    "ListSumTAux []     n = n" |
    "ListSumTAux (x#xs) n = ListSumTAux xs (n+x)" 

  lemma ListSumTAux_1 : " ∀a b. ListSumTAux xs (a+b) = a + ListSumTAux xs b"
    apply (induct xs)
    apply (auto)       (* Works fine *)
  done  

  lemma ListSumTAux_2 : "∀ a. ListSumTAux xs a = a + ListSumTAux xs 0 "  
    apply (induct xs)
    apply (auto)       (* Hangs on this *)
  oops

Answer 1

首先:用HOL全称量词∀来表述目标很不方便。无论如何，目标中的自由变量都是隐式普遍量化的，因此您可以简单地省略 ∀。但是，您将告诉归纳命令使用任意在归纳步骤中普遍量化这些变量:

lemma ListSumTAux_1 : "ListSumTAux xs (a+b) = a + ListSumTAux xs b"
  apply (induct xs arbitrary: a b)
  apply (auto)
done  

现在，回答你的问题:auto 陷入困境，因为你的归纳假设具有以下形式

⋀a. ListSumTAux xs a = a + ListSumTAux xs 0

auto 使用 Isabelle 的简化器，它将其作为重写规则。但是，您会注意到该规则的左侧与该循环的右侧匹配，这导致无限重写序列<​​/p>

ListSumTAux xs a → a + ListSumTAux xs 0 → a + (0 + ListSumTAux xs 0) → 
    a + (0 + (0 + ListSumTAux xs 0))

发生这些情况时，您可以采取以下措施:

1. 您可以进行结构化 Isar 证明并手动完成操作
2. 您可以尝试翻转相关方程，即将目标写为 a + ListSumTAux xs 0 = ListSumTAux xs a。那么左侧就不再与右侧匹配了。
3. 您可以在方程中引入一个额外的前提，例如 a ≠ 0，以防止简化器循环。

无论如何，您都无法通过这种方式证明您的目标，因为它太具体了:如果您将您的目标表述为 ListSumTAux xs a = a + ListSumTAux xs 0，那么您归纳假设中也会有 0，但当然，您的累加器不会总是 0。

这是归纳证明中的一个常见问题，特别是当涉及累加器时，您需要概括您的陈述，以便在证明起作用之前加强归纳假设 - 就像您在引理的第一个陈述中所做的那样，ListSumTAux_1。