第 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.
    でもよい。
    ただし,証明しようとする補題・定理が複雑になると, そのような型をもつプログラムを考えるほうが大変になるので, あまり使わない。