如何阅读 Coq 对 proj1_sig 的定义？

In Coq, sig定义为

Inductive sig (A:Type) (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

我读为

“sig P 是一种类型，其中 P 是一个接受 A 并返回 Prop 的函数。该类型的定义是，如果 P x 成立，则类型 A 的元素 x 的类型为 sig P。”

proj1_sig定义为

Definition proj1_sig (e:sig P) := match e with
                                    | exist _ a b => a
                                    end.

我不知道该怎么办。有人可以提供更直观的理解吗？

非依赖对 vs 依赖对sig

该类型的定义使得元素x类型的A属于类型sig P if P x holds.

这并不完全正确：我们不能说x : sig A P。居民e类型的sig A P本质上是一个pair一个元素的x : A并证明P x成立（这称为依赖对 https://en.wikipedia.org/wiki/Dependent_type#Dependent_pair_type). x and P x使用数据构造函数“包装”在一起exist.

为了看到这一点，让我们首先考虑非依赖对类型prod，其定义如下：

Inductive prod (A B : Type) : Type :=  pair : A -> B -> A * B

prod的居民是成对的，比如pair 1 true（或者，使用符号，(1, true)），其中types两个组件的独立的彼此的。

Since A -> B在 Coq 中只是语法糖forall _ : A, B（定义here https://coq.inria.fr/library/Coq.Init.Logic.html），定义prod可以脱糖成

Inductive prod (A B : Type) : Type :=  pair : forall _ : A, B -> prod A B

上面的定义或许可以帮助我们了解sig A P是（依赖）对。

我们可以从实施和类型中得出什么proj1_sig

从实现中我们可以看出proj1_sig e打开这对包装并 返回first组件，即。x，扔掉证明P x.

The Coq.Init.Specif https://coq.inria.fr/library/Coq.Init.Specif.html模块包含以下注释：

(sig A P)，或者更具暗示性{x:A | P x}，表示该类型的元素子集A满足谓词P.

如果我们看一下类型proj1_sig

Check proj1_sig.

proj1_sig : forall (A : Type) (P : A -> Prop), {x : A | P x} -> A

我们将会看到proj1_sig为我们提供了一种恢复超集元素的方法A从它的子集{x : A | P x}.

之间的模拟fst and proj1_sig

另外，我们可以说，在某种意义上proj1_sig类似于fst https://coq.inria.fr/library/Coq.Init.Datatypes.html#fst函数，返回一对的第一个组件：

Check @fst.

fst : forall A B : Type, A * B -> A

有一个平凡的性质fst:

Goal forall A B (a : A) (b : B),
  fst (a, b) = a.
Proof. reflexivity. Qed.

我们可以制定类似的声明proj1_sig:

Goal forall A (P : A -> Prop) (x : A) (prf : P x),
  proj1_sig (exist P x prf) = x.
Proof. reflexivity. Qed.