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って書いてたら通らなくて、しばらく（・３・）アルェー ってなってた。
IH は「Induction Hypothesis (帰納法の仮定)」の略。