如何阅读 Coq 对 proj1_sig 的定义？
How can I read Coq's definition of proj1_sig?
在 Coq 中，sig 定义为
Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
我读作
"A sig P is a type, where P is a function taking an A and returning a Prop. The type is defined such that an element x of type A is of type sig P if P x holds."
proj1_sig 定义为
Definition proj1_sig (e:sig P) := match e with
| exist _ a b => a
end.
我不知道该怎么做。有人可以提供更直观的理解吗？
非依赖对与 sig
The type is defined such that an element x of type A is of type sig P if P x holds.
这并不完全正确：我们不能说 x : sig A P。 sig A P 类型的居民 e 本质上是元素 x : A 的 对 和 P x 成立的证明（这称为dependent pair）。 x 和 P x 是 "wrapped" 一起使用数据构造函数 exist.
为了理解这一点，让我们首先考虑非依赖对类型 prod，其定义如下：
Inductive prod (A B : Type) : Type := pair : A -> B -> A * B
prod 的居民是成对的，例如 pair 1 true（或者，使用符号 (1, true)），其中两者的 类型 组件彼此独立。
由于 Coq 中的 A -> B 只是 forall _ : A, B 的句法糖（定义为 here），因此 prod 的定义可以脱糖为
Inductive prod (A B : Type) : Type := pair : forall _ : A, B -> prod A B
上述定义或许可以帮助我们看出 sig A P 的元素是（依赖）对。
我们可以从 proj1_sig
的实现和类型中得到什么
从实现中我们可以看到 proj1_sig e 解压了这对
returns 第一个 组件，即。 x，丢掉P x的证明。
Coq.Init.Specif 模块包含以下注释：
(sig A P), or more suggestively {x:A | P x}, denotes the subset of elements of the type A which satisfy the predicate 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 和 proj1_sig
之间的模拟
此外，我们可以说在某种意义上 proj1_sig 类似于 fst 函数，returns 一对中的第一个分量：
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.
在 Coq 中，sig 定义为
Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
我读作
"A sig P is a type, where P is a function taking an A and returning a Prop. The type is defined such that an element x of type A is of type sig P if P x holds."
proj1_sig 定义为
Definition proj1_sig (e:sig P) := match e with
| exist _ a b => a
end.
我不知道该怎么做。有人可以提供更直观的理解吗？
非依赖对与 sig
The type is defined such that an element
xof typeAis of typesig PifP xholds.
这并不完全正确：我们不能说 x : sig A P。 sig A P 类型的居民 e 本质上是元素 x : A 的 对 和 P x 成立的证明（这称为dependent pair）。 x 和 P x 是 "wrapped" 一起使用数据构造函数 exist.
为了理解这一点，让我们首先考虑非依赖对类型 prod，其定义如下：
Inductive prod (A B : Type) : Type := pair : A -> B -> A * B
prod 的居民是成对的，例如 pair 1 true（或者，使用符号 (1, true)），其中两者的 类型 组件彼此独立。
由于 Coq 中的 A -> B 只是 forall _ : A, B 的句法糖（定义为 here），因此 prod 的定义可以脱糖为
Inductive prod (A B : Type) : Type := pair : forall _ : A, B -> prod A B
上述定义或许可以帮助我们看出 sig A P 的元素是（依赖）对。
我们可以从 proj1_sig
的实现和类型中得到什么
从实现中我们可以看到 proj1_sig e 解压了这对
returns 第一个 组件，即。 x，丢掉P x的证明。
Coq.Init.Specif 模块包含以下注释：
(sig A P), or more suggestively{x:A | P x}, denotes the subset of elements of the typeAwhich satisfy the predicateP.
如果我们看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 和 proj1_sig
之间的模拟
此外，我们可以说在某种意义上 proj1_sig 类似于 fst 函数，returns 一对中的第一个分量：
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.