Isabelle 自动证明器在引理上工作,挂在引理的特例上
Isabelle auto prover works on lemma, hangs on special case of the lemma
为什么第二个引理的 "auto" 证明挂起?第二个引理是第一个引理的特例。
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
首先:用HOL通用量词表述目标不方便∀
。无论如何,目标中的自由变量都是隐式普遍量化的,所以你可以简单地省略 ∀
。但是,您将告诉 induction
命令在归纳步骤中使用 arbitrary
:
普遍量化这些变量
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
使用伊莎贝尔的简化器,将此作为重写规则。但是,您会注意到此规则的左侧与此循环的右侧匹配,这导致无限重写序列
ListSumTAux xs a → a + ListSumTAux xs 0 → a + (0 + ListSumTAux xs 0) →
a + (0 + (0 + ListSumTAux xs 0))
发生这些情况时,您可以采取以下措施:
- 你可以做一个结构化的 Isar 证明并手工做事
- 你可以尝试翻转问题方程,即将目标写成
a + ListSumTAux xs 0 = ListSumTAux xs a
。那么左边就不再和右边匹配了。
- 您可以在等式中引入一个额外的前提,例如
a ≠ 0
,以防止简化器循环。
在任何情况下,您都无法通过这种方式证明您的目标,因为它太具体了:如果您将目标表述为 ListSumTAux xs a = a + ListSumTAux xs 0
,那么您将在 0
归纳假设也是如此,但是当然,您的累加器不会总是 0
.
这是归纳证明中的一个常见问题,尤其是当涉及累加器时,您需要概括您的陈述以在证明起作用之前加强归纳假设——就像您在引理的第一个陈述中所做的那样, ListSumTAux_1
。
为什么第二个引理的 "auto" 证明挂起?第二个引理是第一个引理的特例。
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
首先:用HOL通用量词表述目标不方便∀
。无论如何,目标中的自由变量都是隐式普遍量化的,所以你可以简单地省略 ∀
。但是,您将告诉 induction
命令在归纳步骤中使用 arbitrary
:
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
使用伊莎贝尔的简化器,将此作为重写规则。但是,您会注意到此规则的左侧与此循环的右侧匹配,这导致无限重写序列
ListSumTAux xs a → a + ListSumTAux xs 0 → a + (0 + ListSumTAux xs 0) →
a + (0 + (0 + ListSumTAux xs 0))
发生这些情况时,您可以采取以下措施:
- 你可以做一个结构化的 Isar 证明并手工做事
- 你可以尝试翻转问题方程,即将目标写成
a + ListSumTAux xs 0 = ListSumTAux xs a
。那么左边就不再和右边匹配了。 - 您可以在等式中引入一个额外的前提,例如
a ≠ 0
,以防止简化器循环。
在任何情况下,您都无法通过这种方式证明您的目标,因为它太具体了:如果您将目标表述为 ListSumTAux xs a = a + ListSumTAux xs 0
,那么您将在 0
归纳假设也是如此,但是当然,您的累加器不会总是 0
.
这是归纳证明中的一个常见问题,尤其是当涉及累加器时,您需要概括您的陈述以在证明起作用之前加强归纳假设——就像您在引理的第一个陈述中所做的那样, ListSumTAux_1
。