将“定义”与归纳结合使用

Question

考虑以下应该很容易证明的引理：

lemma
  fixes n m::nat
  defines "m ≡ n - 1"
  shows "m ≤ n"
proof(induction n)
  case 0
  then show ?case unfolding m_def 
      (* Why does «n» appear here? *)
next
  case (Suc n)
  then show ?case sorry
qed

然而在展开 m 之后，目标变为 n - 1 ≤ 0 而不是 0 - 1 ≤ 0 使目标无法证明，因为 n = 2 是一个反例。

这是 Isabelle 中的错误吗？如何正确展开定义？

Answer 1

我认为一个有用的解释如下：回想一下 nat.induct 的定义，即

?P 0 ⟹ (⋀n. ?P n ⟹ ?P (Suc n)) ⟹ ?P ?n

并注意?n表示n隐式全称量化，即前面的定义等价于

⋀n. ?P 0 ⟹ (⋀n. ?P n ⟹ ?P (Suc n)) ⟹ ?P n

现在，当将 nat.induct 应用于您的示例时，显然要证明的第一个子目标是 ?P 0，即 m ≤ 0。但是，在那种情况下，n 仍然是任意但固定的 nat，特别是它 而不是 认为 n = 0，这就是为什么在展开 m 的定义后你会得到 n - 1 ≤ 0 作为新的子目标。关于您的具体问题，问题是您无法通过 n 上的归纳来证明您的结果（但您可以使用 unfolding m_def by simp 轻松证明）。

Answer 2

正如 Javier 所指出的，在引理头中定义的 n 不同于 induction 创建的 n。换句话说，任何来自“外部”的引用 n 的事实都不能直接在 proof (induction n) 环境中使用。

但是，Isabelle 确实提供了一种“注入”此类事实的方法，方法是将它们输送到 induction:

lemma
  fixes n m::nat
  defines "m ≡ n - 1"
  shows "m ≤ n"
  using m_def (* this allows induction to use this fact *)
proof(induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

using assms 在这种情况下同样有效。

请注意，不再需要直接引用 m_def，因为每个 case 都包含一个版本（在 0.hyps 和 Suc.hyps 中；使用 print_cases 在证明中获取更多信息）。

将“定义”与归纳结合使用

Using `defines` with induction

isabelle