types - COQ の prod 型と sig 型の関係

Question

COQ では、タイプ prod (1 つのコンストラクターのペアを持つ) はデカルト積に対応し、タイプ sig (1 つのコンストラクターが存在する) は従属和に対応しますが、デカルト積が従属和の特定のケースであるという事実はどのように説明されますか? 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

sndメタ理論的な観点から見ると、prod は、コンポーネントがコンポーネントに依存しないsigT の特殊なケースにすぎません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 の で得られるものを説明する 1 つの方法ですsigT。つまり、インデックス付きの s ファミリである型ですx。ここで、インデックスは通常、バリアント型に関連付けられたさまざまなデータ コンストラクターの一般化です。