ひとり正月Coq勉強会

以前も若干勝手にCoqを勉強したことはありましたが,その時は直感主義論理の簡単な証明を書いたくらいで時間がなくなってしまいました.今回は非常に簡単ながら証明駆動っぽい開発をやってみました.なお,Coqはほぼ書いたことがないので証明とかアレかもしれない.

やってみたかったこと

非常に簡単な証明駆動開発

題材

cons

• sortとかマジな証明だとちゃんと小1時間で終わらなくなってしまうので,本当に簡単なものをやってみた

consしたら

• head $ cons x xs = x になる
• tail $ cons x xs = xs になる

の２つの性質が満たされる.ということで命題を書いてみた

Definition is_head_x (A : Type)( x :option A) ( xs : list A) : Prop := (head xs) = x.
Definition is_tail_ys (A : Type)( ys :list A) ( xs : list A) : Prop := (tail xs) = ys.

そして consを定義

Definition cons ( A : Type) ( x : A) ( xs : list A) : list A := cons x xs.

証明はdefinitionより明らかなのでunfoldするだけで,わざわざ書く価値もないが,とりあえず.適当に証明して.

Extraction Language Haskell.
Extraction cons.

でHaskellのconsを適用するだけの関数が出てきた.

非常に簡単すぎてこれでいいのかよくわからないが,多分証明駆動開発の最も短い実例になったと思う.