如何在Coq中为实数定义"小于"？

Question

我只是想知道如何为实数定义"小于"关系.

我理解,对于自然数(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的建设性逻辑？我是否可以用它来至少对不平等做一些推理(而不是一直重写公理)？

Answer 1

Coq.Reals.RIneq 得出 Rplus_0_r ：对于所有 r，r + 0 = r。是一个公理，等等

吹毛求疵：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有意义，并且根本不清楚您最终会有更少的公理（例如，严格正的概念应该在以下情况下封闭）加法、乘法等）。