[[ocaml-nagoya]] Inductive list (A: Type) : Type := | nil : list A | cons : A -> list A -> list A. (* Check (cons nat 3 (nil nat)). *) Implicit Arguments nil [A]. Implicit Arguments cons [A]. (* Check (cons 3 nil). *) Fixpoint append {A : Type} (xs ys: list A) : list A := match xs with | nil => ys | cons x xs => cons x (append xs ys) end. Infix "++" := append (at level 60). Fixpoint length {A : Type} (xs : list A) : nat := match xs with | nil => O | cons x xs => S (length xs) end. Theorem append_assoc : forall (A: Type) (xs ys zs : list A), (xs ++ ys) ++ zs = xs ++ (ys ++ zs). Proof. (* あなたの証明を書いてね *) Qed. Theorem append_length : forall (A: Type) (xs ys: list A), length (xs ++ ys) = length xs + length ys. Proof. (* あなたの証明を書いてね *) Qed. ** append_assocの証明の解説 [#j97ea64b] :intros|~ ゴールがforallで始まっているので、introsによって前提に移動します。 :induction xs|~ induction xs. で xs に関する帰納法が始まる。 xs が nil のときと cons の時の場合分けになる。 :simpl|~ x=nilの場合です。まずは simpl. で式を簡約します。 :reflexivity|~ 簡約すると、 = の両辺は 構文的に等価になります。このとき reflexivity タクティックで証明を完了できます。 :simpl|~ 次はconsの場合です。まずは simpl。 :rewrite IHxs|~ このときのゴールをじっと見つめると。。。どうやら 帰納法の仮定IHxsが使えそうなことがわかる。 (先に書かなかったが、 induction xs. したときに cons の仮定部に 帰納法の仮定が挿入されている。) ~ この IHxs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) は等式の形をしている。この仮定を使ってゴールを書き換えるには rewrite IHxs. とやる。 :reflexivity|~ 両辺が構文的に等価になるので、reflexivityで証明終了。 これで append 関数の 結合則が証明できた。 似たようなやり方で関数型プログラムの証明を書いて行くことができる。Coqすばらしす。