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. 

现在，让我们寻找引理，它规定任何 nat 要么是 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，您可以在标准库中查看此引理的实现(该引理又使用了几个引理) )。