如何证明 Isabelle 中归纳定义的关系的非自反性？答案

【问题标题】：How can I prove irreflexivity of an inductively defined relation in Isabelle?如何证明 Isabelle 中归纳定义的关系的非自反性？
【发布时间】：2017-12-06 00:03:37
【问题描述】：

以 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。为什么会这样？如何进行不等式证明？

【问题讨论】：

标签： isabelle induction

【解决方案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

【讨论】：

对unequal 的归纳实际上是我想要的。我的实际问题不是关于不平等，而是关于双相似性。在这种情况下，您描述的解决方案并不是真正的选择。而且我不明白为什么对unequal 的归纳在这里不起作用。毕竟，它在 n + m 的示例中有效。
在仔细研究了Isabelle/Isar参考手册中关于induction证明方法的部分后，我找到了解决我问题的方法。我将很快自己回答这个问题。不过，感谢您的努力。
好的。我期待着您的回答。

【解决方案2】：

induction 方法以不同方式处理变量实例化和非变量实例化。非变量实例化 t 是 x ≡ t 的简写，其中 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)。

【讨论】：