types - COQ 中 prod 和 sig 类型之间的关系

Question

在 COQ 中，类型 prod（具有一个构造函数对）对应于笛卡尔积，类型 sig（具有一个构造函数）对应于依赖求和，但是如何描述笛卡尔乘积是依赖求和的特例这一事实？我想知道 prod 和 sig 之间是否存在联系，例如一些定义相等，但我在参考手册中没有明确找到它。

Answer 1

事实上，该类型更prod类似于：sigTsig

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

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

Inductive sigT (A : Type) (P : A -> Type) : Type :=
  existT : forall x : A, P x -> sigT P

从元理论的角度来看，prod 只是 sigT 的一个特例，您的snd组件不依赖于您的fst组件。也就是说，您可以定义：

Definition prod' A B := @sigT A (fun _ => B).

Definition pair' {A B : Type} : A -> B -> prod' A B := @existT A (fun _ => B).

Definition onetwo := pair' 1 2.

---

但是，它们不能在定义上相等，因为它们是不同的类型。你可以显示一个双射：

Definition from {A B : Type} (x : @sigT A (fun _ => B)) : prod A B.
Proof. destruct x as [a b]. auto. Defined.

Definition to {A B : Type} (x : prod A B) : @sigT A (fun _ => B).
Proof. destruct x as [a b]. econstructor; eauto. Defined.

Theorem fromto : forall {A B : Type} (x : prod A B), from (to x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

Theorem tofrom : forall {A B : Type} (x : @sigT A (fun _ => B)), to (from x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

但这不是很有趣...... :)

Answer 2

乘积是从属总和的特殊情况，恰好当从属总和与常见产品类型同构时。

考虑一个系列的传统求和，其项不依赖于索引：一系列n项的总和，所有这些项都是x. 由于x不依赖于索引，通常表示为i，我们将其简化为n*x。否则，我们会有x_1 + x_2 + x_3 + ... + x_n，其中每个x_i都可以不同。这是描述 Coq 所拥有的一种方式sigT：一种类型，它是 s 的索引族x，其中索引是通常与变体类型相关联的不同数据构造函数的概括。