[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.

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

[Joke]Falso : HyperVerifier and HyperProver

　twitterで知ったジョークサイトなんだが、Falso, by Estatis Inc.があります。

　「ある公理を導入すれば」なんでも証明出来てしまう(笑)という話で、それをいかにも画期的新製品みたいな感じに仕上げているのがおかしい。

　追記：togetter: Falso 定理証明系の大革命

[FM] Maude

　今日はFormal Methods Forumの勉強会で、いつものCoq (CPDT)の話の他に、Maudeをちょっと触ってみた、という話をしました。

　Maudeは項書き換え系の言語で形式仕様記述やモデル検査、DSL記述などにも使える言語です。
　Coqと違って証明も出来るけどメインは仕様記述＆それ自体がプロトタイプとして動く、かなぁ。パズルとかにも役に立つかも。

　あわてて作った資料なんで完成度は低いですがこちら。
Slideshare上のプレゼン
PDF資料

　Maudeに興味のある方はコメント頂けると嬉しいです。

[Coq] CoqUn -- Summer Coq Event in Nagoya

　2010/08/29に名古屋でCoq庵 -- 日本の夏、証明の夏というCoqのイベントが開催されます。
　といっても、Coqユーザが集まって話をしようという比較的緩いイベントなんで、Coq初めてという人も参加すると良いのではなかろうか。入門的な話もあります。

[Coq] Puzzle from Hiyama-san's Blog

　檜山さんのblogに掛け算から足し算を作る（パズルとしてやってみよう）という問題が載っています。
　Coqの練習問題としてちょうど良いかと思い解いてみました。
　思ったより時間がかかってしまい、解き終わる前にネタばらしが出ちゃったのだけど、一応、解いた解答です。http://ideone.com/Staa3

　分配則は簡単だったが、交換則を思いつくまでに苦労した。交換測を思いついたらその延長で結合則もなんとか。ただ、証明はちまちまとrewriteしてるだけ。ここは本当は自動化できるんだろうなぁ。
　Coq初心者的には、inv関係の{a'|a*a'=1}みたいな記法の使い方に慣れたのが良かったか。あとAxiom eq_dec_0:forall a:G, {a=0}+{a<>0}みたいなdecide出来る公理の便利さを実感した。