coq - Isabelle/HOL Isar 中错误假设的证明

Question

我试图证明一个引理在某个部分有一个错误的假设。在 Coq 中，我曾经写过“一致”，它会摆脱目标。但是，我不确定如何在 Isabelle Isar 中进行。我试图证明关于我的 le 的引理功能:

primrec le::"nat ⇒ nat ⇒ bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ⇒ False | Suc j ⇒ le k j)"

lemma def_le: "le a b = True ⟷ (∃k. a + k = b)"
proof
  assume H:"le a b = True"
  show "∃k. a + k = b"
  proof (induct a)
    case 0
    show "∃k. 0 + k = b"
    proof -
      have "0 + b = b" by simp
      thus ?thesis by (rule exI)
    qed

    case Suc
    fix n::nat
    assume HI:"∃k. n + k = b"
    show "∃k. (Suc n) + k = b"
    proof (induct b)
      case 0
      show "∃k. (Suc n) + k = 0"
      proof -
        have "le (Suc n) 0 = False" by simp
        oops

请注意我的 le功能是“小于或等于”。在证明的这一点上，我发现我有假设 H其中指出 le a b = True ，或者在这种情况下是 le (Suc n) 0 = True这是错误的。我该如何解决这个引理？

还有一个小问题:我想写 have "le (Suc n) 0 = False" by (simp only:le.simps)但这不起作用。看来我需要添加一些规则来减少 case 表达式。我错过了什么？

非常感谢您的帮助。

Answer 1

问题不在于很难摆脱 False伊莎贝尔的假设。事实上，如果存在 False，几乎所有 Isabelle 的证明方法都会立即证明任何事情。在假设中。不，这里的问题是，在证明的那个点上，您不再有您需要的假设，因为您没有将它们链接到归纳中。但首先，请允许我说几句小话，然后给出具体的建议来修正你的证明。

几点说明

写le a b = True有点单调或 le a b = False在伊莎贝尔。只需写信 le a b或 ¬le a b .

以方便的形式编写定义对于获得良好的自动化非常重要。当然，您的定义有效，但我建议使用以下定义，它可能更自然，并且免费为您提供方便的归纳规则:

使用函数包:

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

Existentials 有时会隐藏重要的信息，并且它们往往会与自动化混淆，因为自动化永远不知道如何实例化它们。

如果您证明以下引理，则证明是全自动的:

lemma def_le': "le a b ⟷ a + (b - a) = b"
  by (induction a arbitrary: b) (simp_all split: nat.split)

使用我的函数定义，它是:

lemma def_le': "le a b ⟷ (a + (b - a) = b)"
  by (induction a b rule: le.induct) simp_all

然后你的引理很简单:

lemma def_le: "le a b ⟷ (∃k. a + k = b)"
  using def_le' by auto

这是因为存在使搜索空间爆炸。给自动化一些具体的遵循有很大帮助。

实际答案

有很多问题。首先，您可能需要做 induct a arbitrary: b , 自 b在你的归纳过程中会发生变化(对于 le (Suc a) b ，你必须对 b 进行案例分析，然后在案例 b = Suc b' 中，你将从 le (Suc a) (Suc b') 到 le a b' )。

其次，在最顶部，您有 assume "le a b = True" ，但你没有将这个事实链接到归纳中。如果在 Isabelle 中进行归纳，则必须将包含归纳变量的所有必需假设链接到归纳命令中，否则它们在归纳证明中将不可用。所讨论的假设涉及 a和 b ，但如果你对 a 进行归纳，你将不得不推理一些任意变量 a'与 a无关.这样做，例如:

assume H:"le a b = True"
thus "∃k. a + k = b"

(对于 b 上的第二次归纳也是如此)

第三，当您在 Isar 中有多个案例时(例如在归纳或案例分析期间)，您必须用 next 将它们分开。如果他们有不同的假设。 next本质上抛弃了所有固定变量和局部假设。通过我之前提到的更改，您将需要一个 next之前 case Suc ，否则伊莎贝尔会提示。

四、 case Isar 中的命令可以修复变量。在您的 Suc情况下，归纳变量 a是固定的；更改为 arbitrary: b , a和一个 b是固定的。您应该为这些变量指定明确的名称；否则，Isabelle 会发明它们，您将不得不希望它提出的那些与您使用的相同。那不是很好的作风。所以写例如 case (Suc a b) .请注意，在使用 case 时，您不必修复变量或假设某些事情。 . case命令会为您处理这些并将本地假设存储在与案例同名的定理集合中，例如 Suc这里。它们被归类为 Suc.prems , Suc.IH , Suc.hyps .此外，当前案件的证明义务存储在 ?case中。 (不是 ?thesis !)。

结论

有了这个(和一点点清理)，你的证明看起来像这样:

lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
  assume "le a b"
  thus "∃k. a + k = b"
  proof (induct a arbitrary: b)
    case 0
    show "∃k. 0 + k = b" by simp
  next
    case (Suc a b)
    thus ?case
    proof (induct b)
      case 0
      thus ?case by simp
    next
      case (Suc b)
      thus ?case by simp
    qed
  qed
next

可以浓缩为

lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
  assume "le a b"
  thus "∃k. a + k = b"
  proof (induct a arbitrary: b)
    case (Suc a b)
    thus ?case by (induct b) simp_all
  qed simp
next

但实际上，我建议您简单地证明一个具体的结果，例如 le a b ⟷ a + (b - a) = b首先，然后使用它证明存在陈述。