ProofCafe #01 - keigoiの日記

名古屋・栄のお洒落レストラン「どえりゃあ」で、第一回 ProofCafe が開催されました。
ProofCafe は、コンピュータプログラムの安全性に関する定理証明に興味を持つ方々の集いです。
記念すべき第一回目は Coqという定理証明支援系について id:yoshihiro503 が講師を務めました。
詳細は http://coq.g.hatena.ne.jp/yoshihiro503/20100331/p1 。
参加者はほぼ全員社会人で、この分野に対する興味の深さが伺えました。

例題とか

よしひろさんによる一通りのチュートリアルが終わった後、周囲の人は reverse . reverse = id (.は関数合成) の証明や append を使った reverse と iterative な reverse が同じであることの証明などをしていた。
私は map f . reverse = reverse . map f の証明でお茶をにごした。list や append は資料中のものを使っている。 map と append に関する補題の後、その補題を使った定理を証明している。

Fixpoint map {A B:Set} (f:A->B) (xs:list A) : list B :=
  match xs with
  | nil => nil
  | cons y ys => cons (f y) (map f ys)
  end.

Lemma map_append (A B:Set)(f:A->B)(xs ys:list A) : map f (append xs ys) = append (map f xs) (map f ys).
intros.
induction xs.
 simpl in |- *.
 reflexivity.
 
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
Qed.

Theorem map_reverse (A B:Set)(f:A->B)(xs:list A) : map f (reverse xs) = reverse (map f xs).
induction xs.
 simpl in |- *.
 reflexivity.
 
 simpl in |- *.
 rewrite (map_append A B f (reverse xs)) in |- *.
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
Qed.

関連リンク

例題とか