在 Isabelle 中使用“induct”证明时如何使用基本情况假设

Question

假设我要证明一个假设“n ≥ m”（两者都是自然数）的定理，我对n 应用归纳法。在基本情况下，假设是“n = 0”。有了这两个，我们可以得出结论，在基本情况下，“m = 0”。

但是，我在使用语句“n = 0”时遇到了问题：

lemma foo:
  assumes "(n::nat) ≥ (m::nat)"
  shows ...
proof (induct n)
  case 0
  have "m = 0" using <I don't know what to put here> assms by simp
  ...
qed

我试过using "n = 0"，但它似乎是“Undefined fact”。我也尝试将其添加为假设，但无济于事。尽管如此，在分析基本情况时，很明显这是一个隐含的假设。

那么，我如何在我的证明中直接使用基本情况的假设？

Answer 1

当您调用induct 时，您需要参与归纳的任何假设都需要成为证明状态的一部分。特别是，这应该是包含您进行归纳的所有假设（即在您的情况下包含n 的所有假设）。

因此，您应该在proof 之前执行using assms。然后0 ≥ m 将在基本情况下提供给您，名称为"0.prems"（或者只是0 用于所有这些加上归纳假设，在这种情况下不存在）。