技術と魚

技術屋ですが経営もやってます

Coq再入門 - SetとProp

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