如何阅读Coq中proj1_sig的定义？

Question

7

在 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.

我不确定如何理解这个。是否可以有人提供更直观的理解？

- Dr. John A Zoidberg

这个问题有些相关。还有这个和这个。此外，这个关于 sigma 类型相等性的问题也可能会引起一些兴趣。我添加了这些链接，因为自动链接并不太相关。 - Anton Trunov

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Anton Trunov · Accepted Answer

该类型被定义为，如果P x成立，则类型A的元素x属于类型sig P。

这并不完全正确：我们不能说x:sig A P。类型sig A P中的一个元素e本质上是一个对，由一个元素x:A和一个证明P x成立组成（这称为依赖对）。使用数据构造函数exist将x和P x "包装"在一起。

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

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

prod的居民是一对一对的，比如pair 1 true（或者使用符号表示为(1, true)），其中两个组成部分的类型是相互独立的。

由于在Coq中A -> B仅仅是forall _ : A, B的语法糖（定义在这里），因此prod的定义可以被解释为：

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

上述定义或许可以帮助我们看到，sig A P 的元素是（依赖）对。

从实现中我们可以看到，proj1_sig e 拆开了这个对并返回第一个分量，即 x，抛弃了 P x 的证明。

Coq.Init.Specif 模块包含以下注释：

(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 为我们提供了一种从其子集 {x：A | P x} 恢复超集 A 的元素的方法。

此外，我们可以说，在某种意义上，proj1_sig 类似于 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.