- 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となる。