7

我只是想知道如何为实数定义“小于”关系。

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

但我想知道 Coq 中是否有一组最小的实数公理，基于这些公理可以推导出其他属性/关系。（例如 Coq.Reals.RIneq有它Rplus_0_r : forall r, r + 0 = r.是一个公理，等等）

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

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

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

4

2 回答 2

3

Coq.Reals.RIneq 有它 Rplus_0_r : forall r, r + 0 = r。是一个公理，等等

Nitpick：Rplus_0_r不是公理，而是公理Rplus_0_l。您可以在模块Coq.Reals.Raxioms中获得它们的列表以及在Coq.Reals.Rdefinitions中使用的参数列表。

如您所见，“大于（或等于）”和“小于或等于”都是根据“小于”定义的，这是假设的，而不是使用您建议的命题引入的。

看起来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.

但是，您仍然需要定义“严格肯定”的s > 0含义以使该位有意义，并且最终您将拥有更少的公理还不清楚（例如，严格肯定的概念应该在加法、乘法等）。

于 2015-12-21T19:50:52.533 回答
2

事实上，Coq.Real 库在它完全被指定为公理的意义上有点弱，而且在过去的某些（简要）点上它甚至是不一致的。

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

值得指出的是 Coq 的 Reals 的一些替代结构：

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

它只使用排中公理（主要用于比较实数），因此对其一致性的置信度非常高。

最有名的实数无公理表征是 C-CORN 项目，http: //corn.cs.ru.nl/，但我们知道建设性分析与通常的分析显着不同。

于 2016-01-28T01:08:20.000 回答