ProofCafe01

Thanks

YEAR OF THE CAT

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の証明の解説 &dagger;

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すばらしす。

トップページ

OCaml Tips

ネタ記録庫

関数型言語によるWeb開発

ScalaByExample(訳)

限定継続

お勉強リンク

発表資料

活動記録

最新の20件

Thanks

append_assocの証明の解説 &dagger;