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

Question

在COQ中,类型prod(具有一个构造函数对)对应于笛卡尔积和类型sig(存在一个构造函数)对依赖和,但是如何描述笛卡尔积是特定的依赖和的情况？我想知道prod和sig之间有一个联系,例如一些定义相等但我在参考手册中没有明确地找到它.

Answer 1

作为事实上,类型prod更类似于sigT比sig:

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，其中索引是通常与变体类型关联的不同数据构造函数的概括。