logic - 如何证明 forall n:nat, ~n 我已经困惑了几个小时，我不知道如何证明 forall n:nat, ~n<n 在考克。我真的需要你的帮助。有什么建议么？

Question

我已经困惑了几个小时，我不知道如何证明

forall n:nat, ~n<n

在考克。我真的需要你的帮助。有什么建议么？

Answer 1

这个引理在标准库中：

Require Import Arith.
Lemma not_lt_refl : forall n:nat, ~n<n.
Print Hint.

其中的结果是lt_irrefl。一种更直接的实现方式是

info auto with arith.

这证明了目标并展示了如何：

intro n; simple apply lt_irrefl.

既然您知道在哪里可以找到证明，我将仅从基本原理（我想这是您作业的重点）给出如何做的提示。

首先，你需要证明一个否定。这几乎意味着您将n<n推论作为假设并证明您可以推断出矛盾。然后，为了推理n<n，将其扩展到它的定义。

intros h H.
red in H.   (* or `unfold lt in H` *)

现在你需要证明这S n <= n不可能发生。要从第一原则做到这一点，此时您有两个选择：您可以尝试诱导 on n，或者您可以尝试诱导 on <=。<=谓词由归纳定义，在这些情况下，您通常需要对其进行归纳——也就是说，通过对假设的证明进行归纳来推理。但是，在这里，您最终需要推理n，以表明它n不能成为 的第 m^个继任者S n，并且您可以立即开始归纳n。

之后induction n，您需要证明基本情况：您有假设1 <= 0，并且您需要证明这是不可能的（目标是False）。通常，要将归纳假设分解为案例，您可以使用该induction策略或其变体之一。这种策略在假设上构建了一个相当复杂的相关案例分析。查看正在发生的事情的一种方法是调用simple inversion，这给您留下了两个子目标：假设的证明1 <= 0使用le_n需要 的构造函数1 = 0，或者证明使用le_S需要 的构造函数S m = 0。在这两种情况下，需求显然与 的定义相矛盾S，因此该策略discriminate证明了子目标。而不是simple inversion H，您可以使用inversion H，在这种特殊情况下直接证明了目标（不可能的假设情况非常常见，并且已融入成熟的inversion策略）。

现在，我们转向归纳案例，在这里我们很快就来到了我们想要证明S n <= n的地方S (S n) <= S n。我建议您将其声明为一个单独的引理（首先要证明），可以概括为：forall n m, S n <= S m -> n <= m.

Answer 2

Require Import Arith.
auto with arith.