ProofCafe01 のバックアップの現在との差分(No.1)

• バックアップ一覧
• 差分 を表示
• ソース を表示
• バックアップ を表示
• ProofCafe01 へ行く。
  • 1 (2010-04-03 (土) 16:31:04)

• 追加された行はこの色です。
• 削除された行はこの色です。

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