在 Coq 中如何为实数定义 "less than"？

Question

我只是想知道如何为实数定义 "less than" 关系。

我理解对于自然数 (nat)，< 可以递归定义为一个数是另一个数的 (1+) 后继 S数字。我听说关于实数的很多事情在 Coq 中都是公理化的，不计算。

但我想知道在 Coq 中是否存在实数的最小公理集，基于这些公理可以推导出其他 properties/relations。（例如 Coq.Reals.RIneq 认为 Rplus_0_r : forall r, r + 0 = r. 是一个公理，等等）

特别感兴趣的是，是否可以在等式关系之上定义<或<=等关系。例如，我可以想象在传统数学中，给定两个数字 r1 r2:

r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2.

但这在 Coq 的构造逻辑中成立吗？我是否可以使用它至少对不等式进行一些推理（而不是一直重写公理）？

Answer 1

Coq.Reals.RIneq has it that Rplus_0_r : forall r, r + 0 = r. is an axiom, among others

吹毛求疵：Rplus_0_r 不是公理，但 Rplus_0_l 是。您可以在模块 Coq.Reals.Raxioms and a list of the parameters used in Coq.Reals.Rdefinitions.

中获取它们的列表

如您所见，"greater than (or equal)" 和 "less than or equal" 都是根据 "less than" 定义的，这是假设的，而不是使用您建议的命题引入的。

看起来 Rlt 确实可以按照您建议的方式定义：这两个命题可证明等价，如下所示。

Require Import Reals.
Require Import Psatz.
Open Scope R_scope.

Goal forall (r1 r2 : R), r1 < r2 <-> exists s, s > 0 /\ r1 + s = r2.
Proof.
intros r1 r2; split.
 - intros H; exists (r2 - r1); split; [lra | ring].
 - intros [s [s_pos eq]]; lra.
Qed.

然而，您仍然需要定义 "strictly positive" 的含义，以使 s > 0 位有意义，而且您最终会拥有更少的公理一点也不清楚（例如严格正数的概念应该在加法、乘法等下结束。

Answer 2

事实上，Coq.Real 库在完全指定为公理的意义上有点薄弱，并且在过去的某些（简短）点上什至不一致。

所以 le 的定义有点 "ad hoc" 从系统的角度来看，它具有零计算意义，只是一个常数和一些公理。您可以添加公理 "x < x"，而 Coq 无法检测到它。

值得指出 Coq 实数的一些替代构造：

我最喜欢的经典构造是 Georges Gonthier 和 B. Werner 在四色定理中所做的构造：http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

它只使用了排中公理（主要是比较实数）所以一致性可信度很高。

最著名的 axiom-free 实数表征是 C-CORN 项目，http://corn.cs.ru.nl/ 但我们知道建设性分析与通常的分析有很大不同。

在 Coq 中如何为实数定义 "less than"？

How is "less than" defined for real numbers in Coq?

coq

real-number