coq - 如何在 Coq 中从头开始证明“S x > 0”？

Question

我如何证明简单的事实

forall x:nat, S x > 0.

?

我的逻辑是

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

2. S x = 0 导致矛盾。

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

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

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

Answer 1

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

首先，我们需要导入一个包含许多关于自然数的事实的模块（没有这个导入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.

---

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

Search (S _ > 0).

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

Answer 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.

Answer 3

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

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