a. リストAに空のリストBを結合させた結果はリストAに等しい。 b. リストA,B,CについてA::B::Cというように三つのリストを結合する場合、 リストAとBを結合させてからリストCを結合させた場合((A::B)::C)と、 リストBとCを結合させてからリストAを結合させた場合(A::(B::C))は等しい。
2.Coqでプログラムを書く
リストの結合をするプログラムをCoqで書いてみる。
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.
リストを使用するときはRequire Import Listでインポートする。
3.書いたプログラムの性質を証明する
a.空リストを結合しても変わらない
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.
b.結合結果はリストの結合順番に依存しない
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.
Extraction Language Haskell.
Extract Inductive list => "([])" ["[]" "(:)"].
Extraction "myapp" myapp.
作成したコードを保存して終了し、coqcコマンドでHaskellコードを生成する。
$ coqc myapp.v
作成したコードmyapp.hsを開いてみると、
module Myapp where
import qualified Prelude
myapp :: (([]) a1) -> (([]) a1) -> ([]) a1
myapp l l' =
case l of {
[] -> l';
(:) x xs -> (:) x (myapp xs l')}
