1

我有

theory Even
imports Main

begin

inductive
  structural_even :: "nat ⇒ bool"
where
  "structural_even 0"
| "structural_even n ⟹ structural_even (Suc(Suc n))"

fun
  computational_even :: "nat ⇒ bool"
where
  "computational_even 0 = True"
| "computational_even (Suc 0) = False"
| "computational_even (Suc(Suc n)) = computational_even n"


lemma "computational_even n ⟹ structural_even n"
proof (induct n rule: computational_even.induct)
 show "computational_even 0 ⟹ structural_even 0"
 by (metis structural_even.intros(1))
next

证明后我得到

goal (3 subgoals):
 1. computational_even 0 ⟹ structural_even 0
 2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
 3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))

我从大锤那里接到了梅蒂斯的电话

结构性偶数.intros(1) =结构性偶数0

我明白了

show computational_even 0 ⟹ structural_even 0 
Successful attempt to solve goal by exported rule:
 computational_even 0 ⟹ structural_even 0 
proof (state): depth 0

然后。但是，在接下来我得到

goal (3 subgoals):
 1. computational_even 0 ⟹ computational_even 0
 2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
 3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))

因此，尽管系统说“成功尝试通过导出规则解决目标”，但在 1 处仍有一个微不足道的剩余子目标。

为什么会发生这种情况，我该如何解决？

4

1 回答 1

2

Sledgehammer 找到了正确的证明（尽管您可能想要使用它simp）。事实上，你可以继续第二个和第三个子目标（在你证明它们之后，它们将减少为与 #1 类似的新子目标）并最终用qed.

问题是伊莎贝尔如何处理假设。如果像您的情况一样，它们没有明确列出，则留给用户来证明它们。如果

show "computational_even 0 ⟹ structural_even 0"

被等效替换

presume "computational_even 0"
show "structural_even 0"

您的证明表明，structural_even 0只要computational_even 0是真的，它就是真的，但伊莎贝尔“不知道”为什么后者是真的。因此，它为您留下了新的子目标，即证明中陈述的假设可以从子目标中陈述的假设推导出来。这个子目标将qed通过考虑假设来完成证明。

顺便说一句，根本不需要这种情况的假设，因为structural_even 0根据其定义是正确的。所以假设可以安全地移除，只留下

show "structural_even 0"

此外，您可以使用 指定任意假设presume，但您必须稍后证明它们。例如，您可以证明目标

presume "computational_even (Suc 0)"
show "structural_even 0"

但是你必须证明（错误的）目标computational_even 0 ⟹ computational_even (Suc 0)。

为了将假设与目标的前提统一起来，assume改为使用：

assume "computational_even 0"
show "structural_even 0"

在这种情况下，不需要证明子目标的假设（这已经通过与 的统一步骤完成assume）。结果在完成子目标的证明后，如你所料，只剩下 2 个子目标。

作为一个免费的奖励，当assume与错误的假设一起使用时（例如，在前面的错误情况下，computational_even (Suc 0)），Isabelle 将抱怨相应的show语句未能改进任何未决目标，您将无法继续。

于 2016-02-02T17:08:58.783 回答