- Coqにおける Set, Prop は(型の型(=種類)的な意味で) sort という。ともにbuilt-in
- Setはプログラムやデータ型のためにある
- Propは証明や命題のためにある
| # | Set | Prop |
|---|---|---|
| アトミックな項 | Program, データ | Proof 証明 |
| 型 | Specification, データ型 | Proposition 命題 |
| グローバルな宣言 | Parameter |
Axiom |
| ローカルな宣言 | Variable |
Hypothesis |
| 項の定義 | Definition Let |
Theorem Lemma |
※ 実際には、Setの項定義のためにTheoremは使えるし、Propの項定義のためにDefinitionを使うことができる
TransparentとOpaque
- 定義された項と型
t : Tが、その後参照可能であるとき、 transparent という - 定義された項と型
t : Tが、その後Tは参照可能であるが、tは存在の確認のみ可能であるとき、 opaque という
プログラムの場合、項がどのように定義されるかによって、結果の項は当然変わるし、計算量も変わる。つまりtransparentが向いている。 証明の場合、2つの異なる証明項は同じ役割を果たすので、その存在しか興味がない。よって、opaqueが向いている。
実際、Definition t : T := ..で定義されれば、 transparent となり、 Theorem, Lemma ~ Qed で定義される場合はopaqueとなる。
