Isabelle/HOL Isar 中的假假设证明

Question

我试图证明一个引理在某个部分有一个错误的假设。在 Coq 中，我曾经写过“congruence”，它会摆脱目标。但是，我不确定如何在 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 的证明方法都会立即证明任何事情。不，这里的问题是，在证明的那个时候，你不再有你需要的假设，因为你没有把它们链接到归纳中。但首先，请允许我说几句小话，然后给出具体的建议来修正你的证明。

几点说明

1. 在 Isabelle 中写 le a b = True 或 le a b = False 有点不习惯。只需写le a b 或¬le a b。
2. 以方便的形式编写定义对于获得良好的自动化非常重要。当然，您的定义是有效的，但我建议使用以下一个，它可能更自然，并且会免费为您提供方便的归纳规则：

使用函数包：

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

1. 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进行案例分析，然后在@987654335案例中进行分析@你将从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 基本上抛弃了所有固定变量和局部假设。有了我之前提到的更改，您需要在 case Suc 之前添加一个 next，否则 Isabelle 会抱怨。

第四，Isar 中的case 命令可以修复变量。在您的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，然后使用它证明存在性陈述。

Answer 2

Manuel Eberl 做了最难的部分，我只是回答你关于如何尝试和控制simp 等的问题。

在继续之前，我跑题并澄清另一个网站上所说的内容。 “小费”这个词被用来表示对 M.E. 的赞扬，但它应该是“3 个解释提供了 2 个答案”。如果不向列表发送垃圾邮件，就无法更正邮件列表中的电子邮件。

以下是一些简短的答案：

• 无法保证完全控制simp，但属性del 和only，如下所示，将多次控制到您想要的程度。要查看它并没有超出您的预期，需要使用跟踪；下面给出了一个跟踪示例。
• 要完全控制证明步骤，您可以使用“受控”simp、rule、drule 和 erule 以及其他方法。其他人需要提供一份详尽的清单。
• 大多数具有专业知识能够回答“simp、auto、blast 等的详细证据是什么”的人很少愿意投入工作来回答这个问题。调查 simp 正在做什么可能是一项简单而乏味的工作。
• “黑盒证明”总是可选的，据我所知，如果我们希望它们是并且拥有使它们成为可选的专业知识。使它们成为可选的专业知识通常是一个主要的限制因素。有了专业知识，动力就会成为限制因素。

什么是简单的？它不能取悦所有人

如果你看，你会看到。人们抱怨自动化太多，或者他们抱怨 Isabelle 自动化太少。

自动化永远不会过多，但这是因为对于 Isabelle/HOL，自动化大多是可选的。 没有自动化的可能性使证明变得潜在有趣，但只有没有自动化，在宏伟的计划中，证明只不过是纯粹的乏味。

有only和del属性，可以大部分控制simp。仅从实验痕迹说起，即使simp 也会调用其他证明方法，类似于auto 调用simp、blast 等。

我认为你不能阻止simp 调用线性算术方法。但是线性算术在很多时候并不适用。

设置跟踪，甚至是爆炸跟踪

我在这里的回答很笼统，因为它还试图确定auto 在做什么。 auto 采用的最大方法之一是 blast。

如果您不关心blast 何时被auto 使用或直接调用，则不需要attribute_setups。 Makarius Wenzel 删除了爆炸跟踪，但随后很好地展示了如何实现它的代码。

没有爆破部分，只有declare的使用。在证明中，您可以使用using 而不是declare。拿出你不想要的东西。请务必查看 PIDE Simplifier Trace 面板中的新 simp_trace_new 信息。

attribute_setup blast_trace = {*
  Scan.lift
   (Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
    Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
    Scan.succeed true) >>
  (fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
attribute_setup blast_stats = {*
  Scan.lift
   (Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
    Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
    Scan.succeed true) >>
  (fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats b)))
*} 
declare[[simp_trace_new mode=full]]
declare[[linarith_trace,rule_trace,blast_trace,blast_stats]]

通过only 和del 尝试和控制简单，随心所欲

我不想在您的问题中使用公式来努力工作。使用 simp，您在 only 中寻找的结果是没有使用您不期望的规则。

查看simp 跟踪，了解已完成哪些基本的重写将始终完成，例如True 和False 的基本重写。如果您甚至不想这样做，那么您必须求助于rule 之类的方法。

查看是否可以完全关闭simp 的起点是apply(simp only:)。

这里有几个例子。我将不得不更加努力地找到一个示例来显示何时自动使用线性算术：

lemma
  "a = 0 --> a + b = (b::'a::comm_monoid_add)"
  apply(simp only:) (*
    ERROR: simp can't apply any magic whatsoever.
  *)
oops

lemma
  "a = 0 --> a + b = (b::'a::comm_monoid_add)"
  apply(simp only: add_0) (*
    ERROR: Still can't. Rule 'add_0' is used, but it can't be used first.
  *)
oops

lemma
  "a = 0 --> a + b = (b::'a::comm_monoid_add)"
  apply(simp del: add_0) (*
  A LITTLE MAGIC:
    It applied at least one rule. See the simp trace. It tried to finish
    the job automatically, but couldn't. It says "Trying to refute subgoal 1,
    etc.".
      Don't trust me about this, but it looks typical of blast. I was under
    the impressions that simp doesn't call blast.*)
oops

lemma
  "a = 0 --> a + b = (b::'a::comm_monoid_add)"
by(simp) (*
 This is your question. I don't want to step through the rules that simp
 uses to prove it all.
*)