ProofCafe行ってきたよ

勉強会

ProofCafeに行ってきました。みんなで楽しく、ペアプル(ペアプルービング; 二人のプログラマが一つの定理の証明を行う証明技法。)してきました。

人がいっぱい

ProofCafe (5)

  • 正直なところ5〜6人集まればいいほうだと思っていたのですが、14人もの人が集ってました。わりと証明に興味を持っている人って多いんですね。
  • せまい机で全員がノートPCを開いてるという、なかなかに禍々しい雰囲気でした。

能力確認

「この中でHaskel,OCamlみたいな関数型言語を使ったことある人ー?」
ノノノノ (全員挙手)

でスタートしました。
みんなすごい。

内容

ここに書いてもしょうがない気がしたので、資料のほうを補強しました。

あと、ProofCafe 第1回 - TogetterにTwitterでの発言をまとめてあります。

補足

Certified Programming with Dependent Types

二次会で話題にあがってたCPDT(Certified Programming with Dependent Types)は、Certified Programming with Dependent Typesから閲覧とダウンロードができます。

ボクのやった証明
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.
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.

Fixpoint rev {A : Type} (xs : list A) :=
  match xs with
    | nil => nil
    | cons y ys =>
      rev ys ++ cons y nil
  end.

Fixpoint rev_iter {A : Type} (xs : list A) (ys : list A) :=
  match ys with
    | nil  => xs
    | cons z zs => rev_iter (cons z xs) zs
  end.

Lemma rev_iter_rev : forall A (xs ys : list A),
   rev_iter ys xs = rev xs ++ ys.
Proof.
induction xs.
 simpl.
 reflexivity.

 intros.
 simpl.
 rewrite IHxs.
 rewrite append_assoc.
 simpl.
 reflexivity.
Qed.

Lemma append_nil : forall A (xs : list A),
  xs ++ nil = xs.
Proof.
induction xs.
 simpl.
 reflexivity.

 simpl.
 rewrite IHxs.
 reflexivity.
Qed.

Theorem rev_eq : forall A (xs : list A),
  rev_iter nil xs = rev xs.
Proof.
intros.
rewrite rev_iter_rev.
apply append_nil.
Qed.

Lemma rev_append {A : Type} (xs : list A) (x : A) :
  rev (xs ++ (cons x nil)) = cons x (rev xs).
Proof.
induction xs.

 reflexivity.

 intros.
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
Qed.

Theorem rev_rev : forall A (xs : list A),
  rev (rev xs) = xs.
Proof.
induction xs.
 simpl.
 reflexivity.

 simpl.
 rewrite rev_append.
 rewrite IHxs.
 reflexivity.
Qed.