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))))