查找Coq中实数公理化实现方案的相关疑问

Coq实数公理化实现的查找方式 #

你遇到的资料描述和官方文档不一致的问题，本质是Coq标准库实数模块的版本迭代导致的：

• 早期Coq（8.8及更旧版本）的实数库直接把completeness作为顶层公理声明，和你查到的教学资料、旧社区讨论的描述完全一致
• 后续版本对实数库做了分层重构，把原来的单条大公理拆分成了多个更细的基础公理，completeness可以由这些基础公理推导证明，所以在新版本的Coq.Reals.Raxioms文档中它被声明为引理，不是公理

具体查找路径 #

1. 本地安装的Coq标准库源码是最准确的查找渠道，进入Coq安装目录下的theories/Reals文件夹：
   • 基础实数类型R、四则运算、序关系的公理化声明都在Rdefinitions.v文件里，所有用Parameter关键字声明、没有对应构造实现的条目就是公理化的基础定义
   • 所有实数相关的基础公理都在Raxioms.v及其直接依赖的底层源码文件里，用Axiom关键字声明、没有给出证明的条目就是实数库的公理基础
2. 如果你需要匹配旧资料里completeness作为公理的实现，可以查找Coq 8.8及更早版本的标准库源码，对应版本的Raxioms.v中该条目确实是公理声明。

额外说明：当前Coq标准库的实数仍然是完全公理化实现，没有采用柯西序列、戴德金分割这类构造性定义，只是拆分了公理粒度，核心设计逻辑和你查到的资料描述没有本质差异。

内容的提问来源于stack exchange，提问作者Bruno