如何在Coq中证明所有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不会发生。要做到这一点从第一原则，你有两个选择：你可以尝试导入n，或者你可以尝试导入<=。谓词通过归纳定义，通常在这些情况下需要对它进行归纳 - 也就是说，通过对假设的证明进行归纳推理。在这里，尽管如此，你最终需要对n进行推理，以表明n不能成为S n的后继者，并且你可以立即开始在n上进行归纳。

induction n之后，您需要证明基本情况：您有假设1 <= 0，并且您需要证明这是不可能的（目标是False）。通常，要将归纳假设分解为案例，可以使用induction策略或其变体之一。这种策略对假设构建了一个相当复杂的依赖案例分析。看看发生了什么的一种方法是拨打simple inversion，这留给你两个子目标：或者假设1 <= 0的证明使用le_n构造函数，这要求1 = 0，或者证明使用le_S构造函数，这需要S m = 0。在这两种情况下，要求与S的定义明显矛盾，所以策略discriminate证明了子目标。您可以使用inversion H，而不是simple inversion H，在这种特殊情况下，它直接证明了目标（不可能的假设情况非常普遍，并且已经融入了全面的inversion策略）。

现在，我们转到感应情况，我们很快来到我们想要从S (S n) <= S n证明S n <= n的点。我建议你把它作为一个单独的引理（首先要证明），这可以概括为：forall n m, S n <= S m -> n <= m。

Answer 2

Require Import Arith. 
auto with arith.