3

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

forall n:nat, ~n<n

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


Require Import Arith.
auto with arith.
4

2 回答 2

6

这个引理在标准库中:

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.

于 2011-11-12T17:01:19.467 回答
3
Require Import Arith.
auto with arith.
于 2011-11-12T14:15:42.730 回答