tmiyaさんの練習問題をラムダ式で解いてみた

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。
Functional Programming Memo: [Coq] Coq-99 : Part 1
この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。

このようなシンプルな直観主義的な命題論理ならばラムダ式でもシンプルな証明を与えることが出来る。HaskellやMLなどを知っている関数型プログラマやAgda2erならこちらの証明の方がわかりやすいかもしれない。

Section Prop_Logic.

  Definition Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C :=
    fun A B C H1 H2 H3 => (H1 H3 (H2 H3)).

  Definition Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C :=
    fun A B C H =>
      match H with
        | conj H1 (conj H2 H3) => conj (conj H1 H2) H3
      end.

  Definition Coq_03 : forall A B C D:Prop,
    (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D :=
    fun A B C D H =>
      match H with
        | conj H1 (conj H2 (conj Ha Hb)) => conj (H1 Ha) (H2 Hb)
      end.

  Definition Coq_04 : forall A : Prop, ~(A /\ ~A) :=
    fun A H =>
      match H with
        | conj Ha Hna => Hna Ha
      end.

  Definition Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C :=
    fun A B C H =>
      match H with
        | or_introl Ha => or_introl _ (or_introl _ Ha)
        | or_intror (or_introl Hb) => or_introl _ (or_intror _ Hb)
        | or_intror (or_intror Hc) => or_intror _ Hc
      end.

  Definition Coq_06 : forall A, ~~~A -> ~A :=
    fun A H Ha => H (fun Hna => Hna Ha).

  Definition Coq_07 : forall A B:Prop, (A->B)->~B->~A :=
    fun A B H Hnb Ha => Hnb (H Ha).

  Definition Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B :=
    fun A B H => H (fun H1 => H1 (fun Ha => (H (fun _ => Ha)))).

  Definition Coq_09 : forall A:Prop, ~~(A\/~A) :=
    fun A H => H (or_intror _ (fun Ha => H (or_introl _ Ha))).

End Prop_Logic.