案例 vs case_tac/induct vs induct_tac

问题描述

我已经与 Isabelle/HOL 合作了几个月，但我一直无法弄清楚使用 _tac 的确切意图。

具体来说，我在谈论 cases 与 case_tac 和 induct 与 indut_tac（尽管它会是很高兴知道 tac 的一般含义，因为我也在使用其他方法，例如 cut_tac）。

我注意到我不能使用 cases 或 induct 将 apply 与 ⋀-bound 变量一起使用，但如果它是结构化证明，我可以。为什么？

一个例子：

    lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule allI)
  apply (case_tac "P x")
  apply (erule notE)
  apply (erule exI)
  apply assumption
  done

另一方面，我注意到 induct 和 induct_tac 之间的另一个区别是我可以对后者使用双重归纳，但不能对前者使用。再说一次，我不知道为什么。

提前致谢。

解决方法

*_tac 是 apply 脚本中使用的内置策略。特别是，case_tac 和 induct_tac 已基本被 Isabelle/Isar 中的 cases 和 induction 证明方法所取代。正如您提到的，case_tac 和 induct_tac 可以处理 ⋀-bound 变量。但是，这非常脆弱，因为它们的名称通常是自动生成的，并且可能会在 Isabelle 更改时更改（当然，您可以使用 rename_tac 来选择固定名称）。这就是为什么现在结构化证明方法比非结构化策略脚本更受欢迎的原因之一。现在，回到您的示例：为了能够使用 cases，您可以按如下方式引入结构化块：

lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  proof (intro allI)
    fix x
    assume "∄x. P x"
    then show "¬ P x"
      apply (cases "P x")
      apply (erule notE)
      apply (erule exI)
      apply assumption
      done
  qed

如您所见，结构化证明通常比较冗长，但比线性 apply 脚本更具可读性。

如果您仍然对“双重归纳”问题感到好奇，欢迎举个例子。最后，如果您想了解有关使用 Isabelle/Isar 语言环境的结构化证明的更多信息，我强烈建议您阅读 this tutorial on Isabelle/HOL 和 The Isabelle/Isar Reference Manual 以获取更多详细信息。