我如何证明 Isabelle 中归纳定义的关系的反身性？

Question

以 Isabelle 中自然数不等式的以下定义为例：

inductive unequal :: "nat ⇒ nat ⇒ bool" where
  zero_suc: "unequal 0 (Suc _)" |
  suc_zero: "unequal (Suc _) 0" |
  suc_suc:  "unequal n m ⟹ unequal (Suc n) (Suc m)"

我想证明unequal的反反性，即¬ unequal n n。出于说明目的，让我首先证明人为引理 ¬ unequal (n + m) (n + m):

lemma "¬ unequal (n + m) (n + m)"
proof
  assume "unequal (n + m) (n + m)"
  then show False
  proof (induction "n + m" "n + m" arbitrary: n m)
    case zero_suc
    then show False by simp
  next
    case suc_zero
    then show False by simp
  next
    case suc_suc
    then show False by presburger
  qed
qed

在前两种情况下，False必须从假设0 = n + m和Suc _ = n + m推导出来，这是微不足道的。

我希望 ¬ unequal n n 的证明可以用类似的方式完成，即根据以下模式：

lemma "¬ unequal n n"
proof
  assume "unequal n n"
  then show False
  proof (induction n n arbitrary: n)
    case zero_suc
    then show False sorry
  next
    case suc_zero
    then show False sorry
  next
    case suc_suc
    then show False sorry
  qed
qed

特别是，我希望在前两种情况下，我得到假设 0 = n 和 Suc _ = n。但是，我根本没有任何假设，这意味着我被要求从无到有地证明 False。为什么会这样，如何证明不等式？

Answer 1

您正在上岗unequal。相反，你应该归纳超过 n，像这样：

lemma "¬ (unequal n n)"
proof (induct n)
  case 0
  then show ?case sorry
next
  case (Suc n)
  then show ?case sorry
qed

然后我们可以在每个标有 sorry 的子目标上使用 Sledgehammer。 Sledgehammer (with CVC4) 推荐我们完成证明如下：

lemma "¬ (unequal n n)"
proof (induct n)
  case 0
  then show ?case using unequal.cases by blast
next
  case (Suc n)
  then show ?case using unequal.cases by blast
qed

Answer 2

induction 方法以不同方式处理变量实例化和非变量实例化。非变量实例化 t 是 x ≡ t 的 shorthand，其中 x 是新变量。因此，归纳是在 x 上完成的，上下文还包含定义 x ≡ t.

因此，第一个证明中的(induction "n + m" "n + m" arbitrary: n m)等价于(induction k ≡ "n + m" l ≡ "n + m" arbitrary: n m)，具有上述效果。要在第二个证明中获得这种效果，您必须将 (induction n n arbitrary: n) 替换为 (induction k ≡ n l ≡ n arbitrary: n)。这些假设实际上会变得如此简单，以至于induction方法运行的预简化器可以从中推导出False。结果，将没有任何案例需要证明，您可以将整个内部 proof–qed 块替换为 by (induction k ≡ n l ≡ n arbitrary: n).

我如何证明 Isabelle 中归纳定义的关系的反身性？

How can I prove irreflexivity of an inductively defined relation in Isabelle?

induction

isabelle