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

Question

在官方 coq 教程中，他们定义了以下小于或等于的归纳定义：

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

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

1. le_n它采用任何自然数并构造 的证明le n n。
2. 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 上使用 elim，在 H 上，尝试使用forall n : nat, 0 <> S n.等）都失败了。

尽管我的“计算机科学”大脑对这种推理完全没问题，但我的“数学家大脑”在接受这一点时遇到了一点麻烦，因为没有假设这是构建le. 这让我觉得也许使用倒置策略是做到这一点的唯一方法。

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

标签： coqcoq-tactic

Answer 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

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

那么这对您的问题有什么帮助呢？有了一个假设n <= 0，这意味着你的目标应该是这样P(n0)的n0 := 0。现在考虑要证明n = 0，应该是什么形状P？您可以尝试采用最简单的解决方案P(n0) := n = 0（如果您直接在代码中调用，这实际上就是 Coq 正在做的事情elim H），但是您无法证明您的两种情况中的任何一种。问题是，选择此选项后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.