Proof Cafe
4/25に、Proof Cafe (栄)に参加してきました。
Coq 初体験。
最初は、id:yoshihiro503 さんから資料に沿って Coq の解説が。
Vernacular が分かれば Coq が分かる? Coq のファイルの拡張子は .v Checkで 型を調べる。 ガリナ(Gallina):ラムダ式 nat : 型を表すラムダ式 (自然数) - Gallina 、この型はSet。 Set : 型を表すラムダ式 (型)、この型はType。 Type : 型を表すラムダ式 (型)、この型はType。 Prop : 命題の型 Eval compute in 〜 で、〜を評価できる。
その後、これをやってみる。
↓書いたやつ。
(* listの定義 *) 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). *) (* append(再帰関数)の定義 *) (* 型を中括弧で指定すると、型推論が効く。 *) (* 型を小括弧で指定すると型推論が効かないけど、あとでImplicitすればできる *) Fixpoint append {A : Type} (xs ys: list A) : list A := match xs with | nil => ys | cons x xs => cons x (append xs ys) end. (* 中置演算子++の定義。append関数に別名を与える。 *) (* at level は結合の強さ*) 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. intros. induction xs. simpl. reflexivity. simpl. rewrite IHxs. reflexivity. Qed. Theorem append_length : forall (A: Type) (xs ys: list A), length (xs ++ ys) = length xs + length ys. Proof. intros. induction xs. simpl. reflexivity. simpl. rewrite IHxs. reflexivity. Qed.
simpl 賢い。すごく賢い。
IHxs が lHxs に見えて、lHxsって書いてたら通らなくて、しばらく(・3・)アルェー ってなってた。
IH は「Induction Hypothesis (帰納法の仮定)」の略。