是否可以在不使用反转的情况下在 Coq 中证明 `forall n: nat, le n 0 -> n = 0.`？答案

【问题标题】：Is it possible to prove `forall n: nat, le n 0 -> n = 0.` in Coq without using inversion?是否可以在不使用反转的情况下在 Coq 中证明 `forall n: nat, le n 0 -> n = 0.`？
【发布时间】：2021-05-10 04:55:25
【问题描述】：

在official coq tutorial 中，他们定义了以下小于或等于的归纳定义：

Inductive le (n : nat) : nat -> Prop :=
          | le_n : le n n
          | le_S : forall m : nat, le n m -> le n (S m).

我对此的理解是，它定义了两个类型构造函数：

le_n 接受任何自然数并构造 le n n 的证明。
le_S 接受任何自然数m，le n m 的证明并构造le n (S m) 的证明

到目前为止一切顺利。然而，他们随后继续引入以下引理和证明

Lemma tricky : forall n:nat, le n 0 -> n = 0.
Proof.
  intros n0 H.
  inversion H.
  trivial.
Qed.

“反转”步骤是我感到困惑的地方。我知道除非 n 等于 0，否则无法构造 le n 0，因为 0 没有后继，但我不确定倒置策略是如何解决这个问题的。

为了尝试了解它在哪些方面做得更好，我尝试在不使用倒置策略的情况下证明这个引理。但是，到目前为止，我的所有尝试（即在 n0 和 H 上使用 elim，尝试使用 forall n : nat, 0 <> S n. 等事实）都失败了。

虽然我的“计算机科学”大脑完全可以接受这种推理，但我的“数学家大脑”在接受这一点时遇到了一点麻烦，因为没有假设这是唯一的方法构造le的居民。这让我想到，也许使用倒置策略是做到这一点的唯一方法。

没有倒置策略是否可以证明这个引理？如果可以，怎么做？

【问题讨论】：

标签： coq coq-tactic

【解决方案1】：

可以不用倒置来证明这个引理：重点是对适当的目标进行归纳（消除）。

首先请注意，当您将elim 应用于le n 0 类型的假设时，Coq 将应用与le 相关的消除原则。这里那个消除原理叫做le_ind，可以查询它的类型：

forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

这可能有点吓人，但重要的一点是，为了从假设 n <= n0 中证明目标 P n0，您需要考虑两种情况，一种用于 le 的每个构造函数。

那么这对您的问题有何帮助？假设n <= 0，这意味着你的目标应该是P(n0) 和n0 := 0。现在考虑要证明n = 0，P 的形状应该是什么？您可以尝试采用最简单的解决方案 P(n0) := n = 0（如果您在代码中直接调用 elim H，这实际上就是 Coq 正在做的事情）但是您无法证明您的两种情况中的任何一种。问题是，选择P(n0) := n = 0，您忘记了n0 的值，因此您不能使用它等于0。解决这个问题的方法就是记住n0就是0，也就是设置P(n0) := n0 = 0 -> n = 0。

我们如何在实践中做到这一点？这是一种解决方案：

Goal forall n, le n 0 -> n = 0.
Proof.
  intros n H.
  remember 0 as q eqn: Hq. (* change all the 0s to a new variable q and add the equation Hq : q = 0 *)
  revert Hq. (* now the goal is of the shape q = 0 -> n = 0 and H : le n q *)
  elim H.
  - intros; reflexivity. (* proves n = n *)
  - intros; discriminate. (* discriminates S m = 0 *)
Qed.

所有这些泛化0 的工作实际上是inversion 试图为你做的。

请注意，我提出的谓词P 并不是唯一可能的解决方案。另一个有趣的解决方案是基于match（关键字是小规模反转）和P(n0) := match n0 with 0 => n = 0 | S _ => True end。此外，战术最终总是会产生赤裸裸的加利纳术语，因此您总是可以（至少在理论上）写一个与任何战术证明相同的术语。下面是一个使用 Coq 强大但冗长的模式匹配的示例：

Definition pf : forall n, le n 0 -> n = 0 :=
  fun n H =>
    match H
          in le _ q
          return match q return Prop with
                 | 0 => n = q
                 | S _ => True
                 end
    with
    | le_n _ => match n with 0 => eq_refl | S _ => I end
    | le_S _ _ _ => I
    end.

编辑：使用remember 策略简化策略脚本。最初的提议是手动重新实现remember：

set (q := 0). (* change all the 0s in the goal into q and add it as hypothesis *)
  intro H.
  generalize (eq_refl : q = 0). (* introduce q = 0 *)
  revert H.
  generalize q ; clear q.  (* generalizes q *)
  (* Now the goal is of the shape
     forall q : nat, n <= q -> q = 0 -> n = q
     and we can apply elim *)
  intros q H ; elim H.

【讨论】：

【解决方案2】：

问题在于induction 或elim 策略忘记了 在le n 0 中，第二个参数是0。可能有两种情况，le n 0 的证明是le_n 或证明是le_S。事实上，第二种情况是不可能的，因为0 <> S n 但战术不会知道这一点。

inversion 更接近于destruct 和induction，因为它不会给你任何归纳假设。它将查看您给出的命题的所有构造函数，并查看哪些构造函数可以导致它。而这一次，它很聪明，发现 le_S 仅适用于你有 0 <> S n 并丢弃它。

手动完成的一种方法是简单地强制 Coq 记住第二个参数是 0。

Lemma tricky : forall n, le n 0 -> n = 0.
Proof.
  assert (h : forall n m, m = 0 -> le n m -> n = 0).
  { intros n m e h.
    induction h.
    - assumption.
    - discriminate.
  }
  intros n hyp.
  eapply h.
  - reflexivity.
  - assumption.
Qed.

如您所见，我通过添加等式来概括引理。 discriminate 策略允许您从诸如 0 = S n 之类的荒谬假设中得出目标。

【讨论】：

【解决方案3】：

可以按照 Théo 的方法设计一个使用 SSReflect 的简短证明，同时交换 h 的两个假设：

Lemma tricky n (len0 : le n 0) : n = 0.
Proof.
  have h m : le n m -> m = 0 -> n = 0 by elim. 
  exact: (h 0).
Qed.

【讨论】：

【解决方案4】：

当你 destruct 假设 n <= 0 时，Coq 忘记了右手边的值是 0 并要求你证明第二步的任意值 m。

因此，您必须 remember 表明该值实际上是 0。那么你将有足够的信息来得到第二种情况下矛盾的假设“S m = 0”。

Goal forall n, n <= 0 -> n = 0.
  remember 0 as m. 
  destruct 1. 
  - reflexivity.
  - pose proof (I : match S m with S _ => True | 0 => False end) as HF.
    rewrite Heqm in HF.
    apply False_ind, HF.
Qed.

【讨论】：