COQ中类型prod和sig之间的关系(Relation between types prod and sig in COQ)

COQ中类型prod和sig之间的关系(Relation between types prod and sig in COQ)

在COQ中，类型prod（带有一个构造函数对）对应于笛卡尔乘积并且类型sig（带有一个构造函数）与相关的总和相对应，但是如何描述笛卡尔乘积是相关和的特定情况？ 我想知道prod和sig之间是否存在关联，例如某些定义相同，但我在参考手册中没有明确地找到它。

In COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that the cartesian product is a particular case of dependent sum? I wonder there is a link between prod and sig, for instance some definitional equality but I don't find it explicitely in the reference manual.

最满意答案

事实上，类型prod比sig更类似于sigT ：

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.

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

As a matter of fact, the type prod is more akin to sigT than 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

From a meta-theoretic point of view, prod is just a special case of sigT where your snd component does not depend on your fst component. That is, you could define:

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.

---

They can not be definitionally equal though, since they are different types. You could show a bijection:

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.

But that's not very interesting... :)