2

我如何证明简单的事实

forall x:nat, S x > 0.

?

我的逻辑是

  1. 对于任何 nat n,n > 0 或 n = 0。

  2. S x = 0 导致矛盾。

我的主要问题是我无法记住所有这些关于 nat 的琐碎定理/引理,而且我对搜索命令的了解不够。

我试图“破坏 gt”或“>”构造函数,或者对“gt”进行一些反转。但我无法弄清楚语法或这是否是正确的方向。

任何帮助(除了像欧米茄这样的重物)都非常感谢。

4

3 回答 3

2

这是另一种方法(基于您对自然数的观察)。

首先,我们需要导入一个包含许多关于自然数的事实的模块(没有这个导入Search将找不到我们要查找的内容):

Require Import Coq.Arith.Arith. 

现在,让我们寻找引理,它指出 anynat0或者大于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.


顺便说一句,标准库中有一个引理(从 Coq v8.5 开始),它声明的内容与您的引理完全相同:

Search (S _ > 0).

这导致gt_Sn_O: forall n : nat, S n > 0,您可以只看标准库中这个引理的实现(它又使用了几个引理)。

于 2016-06-17T15:59:17.830 回答
2

这里有一些命令可以帮助你:

  • 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.
于 2016-06-17T15:26:30.223 回答
1

我提出了一种基于算子计算编码的替代解决方案<

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
于 2016-06-17T16:44:46.530 回答