[Coq] Coq-99 : Part 1

　前にS-99: Ninety-Nine Scala Problemsというのを紹介しましたが、Coqでも入門者が勉強用に解く為の問題集というのを考えてみました。

　まずは命題論理の証明の課題。勿論、tautoとかで一発だと思いますが、練習問題なので入門者は自力で解こう。
　Admitted.を消して証明を書く事が期待されています。

Section Prop_Logic.
  Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
  Admitted.
  Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
  Admitted.
  Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D.
  Admitted.
  Lemma Coq_04 : forall A : Prop, ~(A /\ ~A).
  Admitted.
  Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
  Admitted.
  Lemma Coq_06 : forall A, ~~~A -> ~A.
  Admitted.
  Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A.
  Admitted.
  Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B.
  Admitted.
  Lemma Coq_09 : forall A:Prop, ~~(A\/~A).
  Admitted.
End Prop_Logic.

解答例は例えばこれとか。