我已经困惑了几个小时,我无法弄清楚如何证明
forall n:nat, ~n<n
在Coq.我真的需要你的帮助.有什么建议？
这个引理在标准库中:
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不能是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.