Coq证明过程中如何通过非构造性公理添加选择函数及关联性质假设

现有上下文基础 #

当前Coq证明环境中已有的定义与假设：

(* 基础类型与定义 *)
A B:Type
P : A -> Prop
Q : A -> B -> Prop
(* 已有的存在性假设 *)
H : forall a : A, P a -> exists b : B, Q a b

需要向环境中新增的两个项：

• 函数项 f : A -> B
• 性质假设 H' : forall a : A, P a -> Q a (f a)

纯构造性路径（受限适用） #

Coq核心逻辑内置了严格的Prop与Type层级分离规则，搭配证明无关性设计，禁止从Prop层级的证明中提取可计算的Type层级值。
只有当你手中的存在性假设是**Type层级的强存在（即sig类型）**时，才能在不引入任何公理的情况下完成目标：

• 若现有假设为形式 H_constructive : forall a : A, P a -> {b : B | Q a b}（sig类型属于Type层级，可提取具体值）
• 可直接构造f := fun a pa => proj1_sig (H_constructive a pa)
• 可直接构造H' := fun a pa => proj2_sig (H_constructive a pa)

但你当前持有的H是Prop层级的普通exists，纯构造路径无法满足需求，必须借助非构造公理。

非构造公理路径（通用适配当前场景） #

这是该类场景的标准实现方式，核心是引入经典集合论中的选择类公理，打通Prop层级证明到Type层级可计算值的提取通道。Coq标准库提供了两种等价的常用公理，任选其一即可完成目标：

1. 不定描述公理（Constructive Indefinite Description）
   公理核心：只要“存在x满足某性质”的命题成立，就可以提取出具体的x和对应的性质证明。

   Axiom constructive_indefinite_description :
     forall (T : Type) (pred : T -> Prop),
       (exists x : T, pred x) -> {x : T | pred x}.
   

   操作步骤：
   • 若类型B是可居的（即存在固定默认值b0 : B），对每个输入a分分支处理：
     • 当P a成立时，用不定描述公理从H的证明中提取对应的b值
     • 当P a不成立时，直接返回默认值b0
   • 基于上述分支构造f后，直接从提取的sig结构的第二个投影中拿到Q的证明，组装为要求的H'
2. 经典选择公理（Choice Axiom）
   公理核心：只要对每个输入a都存在对应的b满足关系R，就一定存在一个全局函数f，使得对所有a，R a (f a)成立。

   Axiom choice :
     forall (A B : Type) (R : A -> B -> Prop),
       (forall a : A, exists b : B, R a b) ->
       exists f : A -> B, forall a : A, R a (f a).
   

   操作步骤：
   • 自定义关系R：当P a成立时，令R a b := Q a b；当P a不成立时，令R a b对所有b恒成立
   • 此时原有假设H天然满足forall a, exists b, R a b的前提
   • 直接应用选择公理，就能一步提取出f和对应的全局性质证明，筛选出满足P a的分支即可得到要求的H'
   • 这种方式不需要提前为B类型找默认值——因为P不成立的分支对返回值没有任何约束，不管函数返回什么值都满足关系R的要求

实现注意事项 #

• 引入上述非构造公理后，Coq环境的强归约性质会被打破：构造出的f是纯抽象的函数，没有实际的可计算执行逻辑，仅在证明系统中被保证存在
• Prop层级的普通exists本质是证明无关的命题，你无法在纯构造逻辑下从这类证明中提取出Type层级的可计算值，这正是需要引入公理的根本原因

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