読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

SICPのEx 2.4 をCoqで解いてみた

Coq SICP Extraction Language Scheme

SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。

問題はペア構造のチャーチエンコーディングの話。

Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。
CoqのコードからSchemeのコードを出力してみたら、問題で与えられているコードとだいたい一緒だったから大丈夫だろう。

Section SICP_EX_2_4.

(* このセクションで使う二つの型 A, B を仮定する *)
Variable A B : Type.

Definition pair (X:Type) : Type := (A->B->X) -> X.

Definition  cons (X:Type) (x:A) (y:B) : pair X  := 
  (fun m => m x y).

Implicit Arguments cons [X].

Definition  car (z: pair A) : A  :=
   z (fun p q => p).

(* Exercise 2.4 その1  任意の引数 x y に対して car (cons x y) が x となる事を検証する *)
Theorem exercise_2_4_car : forall x y, car (cons x y) = x.
Proof.
 auto.
Qed.


Definition  cdr (z: pair B) : B  :=
   z (fun p q => q).

(* Exercise 2.4 その2  任意の引数 x y に対して cdr (cons x y) が y となる事を検証する *)
Theorem exercise_2_4_cdr : forall x y, cdr (cons x y) = y.
Proof.
 auto.
Qed.

End SICP_EX_2_4.

Extraction Language Scheme.
Extraction cons.
Extraction car.
Extraction cdr.

コンパイル結果 (Coq 8.1 pl2)

(define cons (lambdas (x y m) (@ m x y)))

(define car0 (lambda (z) (z (lambdas (p q) p))))

(define cdr0 (lambda (z) (z (lambdas (p q) q))))