2010-09-26

tmiyaさんの練習問題をラムダ式で解いてみた

Coq 練習問題

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。
Functional Programming Memo: [Coq] Coq-99 : Part 1
この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。

このようなシンプルな直観主義的な命題論理ならばラムダ式でもシンプルな証明を与えることが出来る。HaskellやMLなどを知っている関数型プログラマやAgda2erならこちらの証明の方がわかりやすいかもしれない。

Section Prop_Logic.

  Definition Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C :=
    fun A B C H1 H2 H3 => (H1 H3 (H2 H3)).

  Definition Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C :=
    fun A B C H =>
      match H with
        | conj H1 (conj H2 H3) => conj (conj H1 H2) H3
      end.

  Definition Coq_03 : forall A B C D:Prop,
    (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D :=
    fun A B C D H =>
      match H with
        | conj H1 (conj H2 (conj Ha Hb)) => conj (H1 Ha) (H2 Hb)
      end.

  Definition Coq_04 : forall A : Prop, ~(A /\ ~A) :=
    fun A H =>
      match H with
        | conj Ha Hna => Hna Ha
      end.

  Definition Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C :=
    fun A B C H =>
      match H with
        | or_introl Ha => or_introl _ (or_introl _ Ha)
        | or_intror (or_introl Hb) => or_introl _ (or_intror _ Hb)
        | or_intror (or_intror Hc) => or_intror _ Hc
      end.

  Definition Coq_06 : forall A, ~~~A -> ~A :=
    fun A H Ha => H (fun Hna => Hna Ha).

  Definition Coq_07 : forall A B:Prop, (A->B)->~B->~A :=
    fun A B H Hnb Ha => Hnb (H Ha).

  Definition Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B :=
    fun A B H => H (fun H1 => H1 (fun Ha => (H (fun _ => Ha)))).

  Definition Coq_09 : forall A:Prop, ~~(A\/~A) :=
    fun A H => H (or_intror _ (fun Ha => H (or_introl _ Ha))).

End Prop_Logic.

2010-08-30

CPS変換されたフィボナッチ関数の証明をしてみた

Coq CPS変換フィボナッチ

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。

http://ideone.com/3CQOn

しかしfib_cps関数をもっと美しく定義できないものだろうか。

[追記 2010 09/07]
asパターンを使えばパターンマッチを入れ子にしなくても良いことがわかったので、少し実装をシンプルにして書いてみた。証明部分はほぼ同じ。
http://ideone.com/ZFPeQ

2010-08-30

Coqプログラマの集会、Coq庵でした

Coq Coq庵

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。

スライドは以下から参照できます。
Coq庵 - coqグループ

2010-07-24

OCamlでlet recを使わずにfact関数を定義する

OCaml 再帰関数不動点演算 ProofCafe CPDT

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。

Inductive t (A: Set) : Set :=
  | T : (t A -> A) -> t A.

一見なんの問題も無さそうなこの型定義は失敗し、次のようなコンパイルエラーが出力される。

Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".

もしこの型が定義できたとすると次のような関数が定義できてしまう。

Definition ワォ (T f) := f (T f).

ここで (ワォ (T ワォ)) はいくら評価しても同じ項になり、無限ループしてしまう。無限ループはCoqでは御法度なので以上のようなt型は定義できないということなのだ。

以下からが、本日の本題だ。この現象を逆手に取って OCamlで使えばlet recを使わずにループが表現できるんじゃないかと考えてみた。
OCamlでは上のような再帰型は問題なく定義できる。

type 'a t = T of ('a t -> 'a)
let wow (T f) = f (T f)

let _ = wow (T wow)

このコードはlet recを使っていないが、コンパイルすると無限ループで止まらないプログラムが得られる。もう少し工夫して次のように定義すると、関数fixpが定義出来る。fixpは(fixp f ≡ f (fixp f))を満たす不動点演算子だ。

type ('a,'b) t = F of (('a,'b) t -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b)
let fixp_aux (F fld) = fld (F fld)
let v = F (fun self f x -> f (fixp_aux self f) x)
let fixp f x = fixp_aux v f x

このfixpを使って階上を計算するfact関数は次のように記述できる。

let fact =
  fixp (fun fact x -> if x = 0 then 1 else x * fact (x-1))
let _ = print_int (fact 10)

このコードは型定義とlet定義しか使っていないが、ちゃんと(fact 10)が正しい値3628800を返す。OCamlが今偶然手元にない人もIDEONEの結果をみて確かめる事ができる: http://ideone.com/W2yJB。

[追記 2010-07/25]
id:KeisukeNakanoさんのより詳しい記事がありました。多相バリアントを使ったより高度な定義を見る事ができます。#009 賢人鳥をまねる - λx.x K S K ＠はてな

2010-07-18

TDDBC名古屋に行ってきました。

TDD Boot Camp名古屋に参加しました。

id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。
当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇させていただきました - t-wadaの日記

テストをするとき、対象とする関数に副作用が含まれる場合に困難が伴います。私は関数型言語チームとしてOCamlやScalaで参加しましたが、関数型言語は副作用を推奨しないということが言語設計の根底にあるため、テストがしやすいといった特徴があるように感じました。

講師のid:t-wadaさん、id:bleis-tiftさんやスタッフの皆さん、ありがとうございました。

2010-07-13

Alloyセミナーに行ってきました

形式手法 Alloy セミナー

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記

TDDBC名古屋で2日間テスト駆動開発を行った直後でしたが、テスト駆動は開発者向けの手法、Alloyはどちらかというと設計者向けのテストツールのように感じました。

プログラミングの手法や品質管理に比べ、設計書をチェックする手法はあまりないように思います。しかし設計段階での記述漏れやあいまいさがありそれに実装段階で気づいた場合、大きな出戻りが発生することがあります。このような設計段階の誤りを減らすためにAlloyのような軽量な検証ツールは非常に効果的なのではないでしょうか。

システム開発において設計者はAlloyを使い、開発者はテスト駆動開発を行えば、極めて効率よく高品質のものができあがるんじゃないかと考えています。

2010-07-04

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676

まずは集合AとA上の掛け算とサクセッサSを仮定。この部分はid:kikxさんのコードのコピー。

Axiom A : Set.
Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }.

Axiom A_mul : A -> A -> A.
Axiom A_zero: A.
Axiom A_one: A.

Infix "*" := A_mul.
Notation "0" := A_zero.
Notation "1" := A_one.

Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c).
Axiom A_mul_comm: forall a b, a * b = b * a.
Axiom A_mul_1_r: forall a, a * 1 = a.
Axiom A_mul_inv_ex: forall a, a <> 0 -> { a': A | a * a' = 1 }.
Axiom A_mul_0_r: forall a, a * 0 = 0.

Lemma A_mul_1_l: forall a, 1 * a = a.
Proof.
  intros.
  rewrite (A_mul_comm 1 a).
  exact (A_mul_1_r a).
Qed.

Definition A_inv a (H: a <> 0) :=
  let (a', H) := A_mul_inv_ex a H in a'.

Axiom S: A -> A.
Axiom S_inv: A -> A.

Axiom S_inv_l: forall a, S_inv (S a) = a.
Axiom S_inv_r: forall a, S (S_inv a) = a.
Axiom S_0:  S 0 = 1.
Axiom  S_mul: forall a b (H: a <> 0),
  S (a * S (b * A_inv a H)) = a * S (S b * A_inv a H).

Lemma inv_is_inv: forall a (H: a <> 0), a * A_inv a H = 1.
Proof.
  intros.
  unfold A_inv.
  case (A_mul_inv_ex a H).
  trivial.
Qed.

ここからA上の足し算も仮定。同時に足し算が満たすべき公理も仮定。

Parameter A_add : A -> A -> A.
Infix "+" := A_add.
Hypothesis A_add_1_r_S: forall a, a + 1 = S a.
Hypothesis A_add_dist: forall a b c,  a * (b + c) = a * b + a * c.
Hypothesis A_add_0_r: forall a, a + 0 = a.
Hypothesis A_add_comm: forall a b, a+ b = b + a.
Hypothesis A_add_assoc: forall a b c, (a + b) + c = a + (b + c).
Hypothesis A_neg_ex: forall a, { a': A | a + a' = 0 }.

id:kikxさんの定義した足し算をA_kikxs_addという名前で用意し、上で仮定した抽象的な足し算A_addがA_kikxs_addと必ず等価になることを証明した。このことからA_addは一意であることが示せた。

Definition A_kikxs_add a b :=
  match A_eq_dec a 0 with
  | left _ => b
  | right H => a * S (b* A_inv a H)
  end.

Theorem uniqueness : forall a b, A_add a b = A_kikxs_add a b.
Proof.
 intros a b.
 unfold A_kikxs_add.
 case (A_eq_dec a 0).

  intro eq; rewrite eq.
  rewrite A_add_comm.
  rewrite A_add_0_r.
  reflexivity.

  intro neq.
  pattern a at 1; rewrite <- (A_mul_1_r a).
  pattern b at 1; rewrite <- (A_mul_1_l b).
  pattern 1 at 2; rewrite <- (inv_is_inv a neq).
  rewrite (A_mul_assoc).
  rewrite <- A_add_dist.
  rewrite (A_add_comm 1 _).
  rewrite A_add_1_r_S.
  rewrite (A_mul_comm _ b).
  reflexivity.
Qed.