我如何证明简单的事实
forall x:nat, S x > 0.
?
我的逻辑是
对于任何 nat n,n > 0 或 n = 0。
S x = 0 导致矛盾。
我的主要问题是我无法记住所有这些关于 nat 的琐碎定理/引理,而且我对搜索命令的了解不够。
我试图“破坏 gt”或“>”构造函数,或者对“gt”进行一些反转。但我无法弄清楚语法或这是否是正确的方向。
任何帮助(除了像欧米茄这样的重物)都非常感谢。
我如何证明简单的事实
forall x:nat, S x > 0.
?
我的逻辑是
对于任何 nat n,n > 0 或 n = 0。
S x = 0 导致矛盾。
我的主要问题是我无法记住所有这些关于 nat 的琐碎定理/引理,而且我对搜索命令的了解不够。
我试图“破坏 gt”或“>”构造函数,或者对“gt”进行一些反转。但我无法弄清楚语法或这是否是正确的方向。
任何帮助(除了像欧米茄这样的重物)都非常感谢。
这是另一种方法(基于您对自然数的观察)。
首先,我们需要导入一个包含许多关于自然数的事实的模块(没有这个导入Search
将找不到我们要查找的内容):
Require Import Coq.Arith.Arith.
现在,让我们寻找引理,它指出 anynat
是0
或者大于0
:
Search ({_ = 0} + {_}).
此搜索结果
zerop: forall n : nat, {n = 0} + {0 < n},
这是 Coq 对先前观察到的事实的说法。
使用这个zerop
引理,我们最终可以证明我们的目标:
Goal forall x:nat, S x > 0.
intros x.
destruct (zerop (S x)).
(* subcase S x = 0 *)
discriminate. (* deals with the contradiction *)
(* subcase S x > 0 *)
assumption.
Qed.
Search (S _ > 0).
这导致gt_Sn_O: forall n : nat, S n > 0
,您可以只看标准库中这个引理的实现(它又使用了几个引理)。
这里有一些命令可以帮助你:
Unset Printing Notations.
为了能够看到对应的符号
Print ID.
查看标识符ID
是什么
unfold ID.
ID
用它的定义代替
SearchAbout (ID (CON ?m) ?n)
查找涉及子项和任何其他子项的ID
应用的结果(如果您重复使用相同的占位符,则搜索将仅返回相应子项匹配的结果)。CON
?m
例如,在您的情况下,这可能会导致此交互式会话:
Unset Printing Notations.
Goal forall x:nat, S x > 0.
intro x.
Print gt.
unfold gt.
Print lt.
unfold lt.
Print le.
SearchAbout (le (S ?m) (S ?n)).
apply le_n_S.
SearchAbout (le 0 ?m).
apply le_0_n.
Qed.
我提出了一种基于算子计算编码的替代解决方案<
:
From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
Lemma test n : 0 < n.+1.
Proof. by []. Qed.
这是如何运作的?事实上,这是可行的,因为我们将<
操作定义为一个函数:
(m < n) = (m.+1 <= n) = (m.+1 - n == 0)
当应用于您的引理时,它变为:
(0 < n.+1) = (0.+1 <= n.+1) = (1 - n.+1 == 0) = (0 - n == 0) = (0 == 0) = true