Coq 中的子类型化

Question

我定义的子类型如下

Record Subtype {T:Type}(P : T -> Prop) := {
subtype       :> Type;
subtype_inj   :> subtype -> T;
subtype_isinj : forall (s t:subtype), (subtype_inj s = subtype_inj t) -> s = t;
subtype_h     : forall (x : T), P x -> (exists s:subtype,x = subtype_inj s);
subtype_h0    : forall (s : subtype), P (subtype_inj s)}.

下面的定理能否证明？

Theorem Subtypes_Exist : forall {T}(P : T -> Prop), Subtype P.

如果不是，是否可以从任何众所周知的兼容公理中证明它？或者我可以将其添加为公理吗？它会与任何通常的公理冲突吗？（如外延性、功能选择等）

Answer 1

您的定义与 MathComp 的定义几乎相同；实际上，由于证明相关性，您主要缺少的是单射性。

为此，恐怕您需要假设命题无关：

Require Import ProofIrrelevance.
Theorem Subtypes_Exist : forall {T}(P : T -> Prop), Subtype P.
Proof.
intros T P; set (subtype_inj := @proj1_sig T P).
apply (@Build_Subtype _ _ { x | P x} subtype_inj).
+ intros [s Ps] [t Pt]; simpl; intros ->.
  now rewrite (proof_irrelevance _ Ps Pt).
+ now intros x Px; exists (exist _ x Px).
+ now destruct 0.
Qed.

当然，您始终可以将谓词 P 限制为有效证明无关的类型。

Coq 中的子类型化

Subtyping in Coq

coq

dependent-type