Sledgehammer 给出了不充分的证明策略

Question

我有

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))

我接到 sledgehammer 打来的 metis 电话

structural_even.intros(1) = structural_even 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 处有一个微不足道的剩余子目标，尽管系统说 "Successful attempt to solve goal by exported rule"。

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

Answer 1

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 为真时就为真，但 Isabelle "has no idea" 为什么后者为真。因此，它为您留下了新的子目标，即证明中陈述的假设可以从子目标中陈述的假设中推导出来。此子目标将由 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)），伊莎贝尔会抱怨相应的 show声明未能细化任何未决目标，您将无法继续。

Sledgehammer 给出了不充分的证明策略

Sledgehammer gives insufficient proof tactic

isabelle

isar