Contents
1.対象プログラムが持つべき性質を洗い出す参考サイトに証明の仕方については記述されているため、このページでは 証明駆動開発 にのみ焦点を当てる。
2.Coqでプログラムを書く
3.書いたプログラムの性質を証明する
4.他の言語のコードに出力する
vimでシェルを見ながら作業出来るようにするためにvimprocを導入する。$ sudo apt-get install coq
次にcoqtop-vimをインストールする。$ mkdir ~/tmp $ cd ~/tmp $ git clone https://github.com/Shougo/vimproc.git $ cd vimproc $ make -f make_unix.mak $ cp -r autoload/* ~/.vim/autoload/ $ cp -r plugin/* ~/.vim/plugin
これでvimでcoqを利用する環境が構築出来た!$ git clone https://github.com/eagletmt/coqtop-vim $ cd coqtop-vim $ cp autoload/coqtop.vim ~/.vim/autoload/ $ cp plugin/coqtop.vim ~/.vim/plugin
このcoqtopを使用して実際に証明を行ってみる。$ coqtop Welcome to Coq 8.3pl4 (April 2012) Coq <
次に前提を全部出す。これにはintrosタクティクを使用する。Coq < Goal forall (A : Prop), A -> A. 1 subgoal ============================ forall A : Prop, A -> A Unnamed_thm <
Aの型Prop、Aが真だという仮定Hが取りだされた。Unnamed_thm < intros. 1 subgoal A : Prop H : A ============================ A
Unnamed_thm < apply H. Proof completed. Unnamed_thm < Qed. intros. apply H. Unnamed_thm is defined Coq < Ctrl+D $
命題定義を入力したらコマンドモードで「:CoqGoto」と入力する。$ vim reflect.v
a. リストAに空のリストBを結合させた結果はリストAに等しい。
b. リストA,B,CについてA::B::Cというように三つのリストを結合する場合、
リストAとBを結合させてからリストCを結合させた場合((A::B)::C)と、
リストBとCを結合させてからリストAを結合させた場合(A::(B::C))は等しい。
Require Import List. Fixpoint myapp (A : Type)(l l' : list A) : list A := match l with | nil => l' | x::xs => x :: (myapp A xs l') end.
Theorem app_nil_r : forall (A : Type)(l : list A), myapp A l nil = l. intros. induction l. reflexivity. simpl. apply (f_equal (cons a)). apply IHl. Qed.
Theorem app_assoc : forall (A : Type)(l1 l2 l3 : list A), myapp A l1 (myapp A l2 l3) = my app A (myapp A l1 l2) l3. intros. induction l1. reflexivity. simpl. f_equal. apply IHl1. Qed.
作成したコードを保存して終了し、coqcコマンドでHaskellコードを生成する。Extraction Language Haskell. Extract Inductive list => "([])" ["[]" "(:)"]. Extraction "myapp" myapp.
作成したコードmyapp.hsを開いてみると、$ coqc myapp.v
module Myapp where import qualified Prelude myapp :: (([]) a1) -> (([]) a1) -> ([]) a1 myapp l l' = case l of { [] -> l'; (:) x xs -> (:) x (myapp xs l')}