第 2 回
命題論理

• プリント

•    式      :     型   :  ソート
      |             |         |
   program : specification : Set
      |             |         |
  proof term : proposition : Prop
      |             |         |
    証明     :    命題   :  ソート

  この対応がカリー・ハワードの同型 (Curry-Howard isomorphism)。
  と調べていたら こんなページがありました :-)
  つまり，証明はプログラムを書くことに相当する。
例えば，
    Definition f : nat -> nat := fun n : nat => n.
と，
    Lemma f : P -> P.
を考えると，上の nat -> nat との部分と，下の P -> P の部分が 対応している。
下の補題は，まだ証明されていないので，本体が定義されていない状態 である。
これを証明すると，そういう型 (ここでは P -> P) があることが 示される。
→ 関数定義をしていることに相当する。
上の例で，証明をした後に，
    Print f.
とすると，
    f = fun H : P => H
          : P -> P
と表示される。→ 恒等関数が出来ている。
• 7 exact コマンド
  例えば，練習問題の id_p の証明ならば，
      Proof.
        exact (fun H :P => H).
      Qed.
  でもよい。
  ただし，証明しようとする補題・定理が複雑になると， そのような型をもつプログラムを考えるほうが大変になるので， あまり使わない。