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

Question

在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).

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

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 和 H 上使用 elim，尝试使用 forall n : nat, 0 <> S n. 等事实)都失败了。

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

是否可以在没有反转策略的情况下证明这个引理？如果可以，如何实现？

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 (如果您在代码中直接调用 elim H，这实际上就是 Coq 正在做的事情)但是您无法证明这两种情况中的任何一种。问题是选择 P(n0) := n = 0你忘记了 n0 的值(value)所以你不能使用它等于 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 .此外，战术最终总是会产生裸露的 gallina 术语，因此您总是可以(至少在理论上)写出一个术语来证明与任何战术相同的东西。下面是一个使用 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.