我已经困惑了几个小时,我不知道如何证明
forall n:nat, ~n<n
在考克。我真的需要你的帮助。有什么建议么?
这个引理在标准库中:
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
.
Require Import Arith.
auto with arith.