[Coq] Coq-99 : Part 1

Personal memorandum for studying functional languages, theorem proving, and formal verification. But other topics might be included. Written in Japanese (Shift-JIS Encoding). 前にS-99: Ninety-Nine Scala Problemsというのを紹介しましたが、Coqでも入門者が勉強用に解く為の問題集というのを考えてみました。 まずは命題論理の証明の課題。勿論、tautoとかで一発だと思いますが、練習問題なので入門者は自力で解こう。 Admitted.を消して証明を書く事が期待されています。 Section Prop_Logic. Lemma Coq_01 : forall A B C:Prop, (A->B-

[kasumani]

Coq-99 : Part 1 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. Admi

[kururu_goedel]

Coq-99、一応出来た。