Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_in…

Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。OSのディストリビューションは最近リリースされた Ubuntu 9.10。 非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。 Agdaのインストール Agdaの標準…

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。 Lemma p10_left : (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)). Proof. intros. apply H. intro. elim (H0 H2). apply H1. Qed. …

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。 Proposition p09 : forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C. Proo…

以前Merge Sort を実装して証明した。 http://d.hatena.ne.jp/yoshihiro503/20090923ソースコード全体は以下。 http://bitbucket.org/yoshihiro503/mergesort/

http://d.hatena.ne.jp/yoshihiro503/20090708 で証明した。

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。 Require Import List. Proposition p06 : forall {A} (l1 l2 l3:…

中間値の定理もCoqの標準ライブラリに存在する。Rsqrt_def.vの中にIVTという名前で見つけることができる。 Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }. ただ、中間値が f x …

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている！ Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。 Theorem Bolzano_Weierstrass : forall (un:nat -> R) (X:R -> Pr…

Coqでの実数は9つの項と17の公理で定義されている。項の型と意味はだいたい次の様な感じ。 Parameter R : Set. (* 実数全体 *) Parameter R0 : R. (* 実数の0 *) Parameter R1 : R. (* 実数の1 *) Parameter Rplus : R -> R -> R. (* 実数上での足し算 *) Pa…

この問題はCoqの自然数ライブラリを使った。まずを計算するsum関数を定義した。 Require Import Arith. Fixpoint sum n := match n with | O => O | S n => S n + sum n end. 自然数では割り算が難しいので、全体に2を掛けた次の形をまず証明する。 Lemma p0…

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。まず、自然数全体の型 nat を定義する。 Indu…

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん

Coqが今流行っているらしい。twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。 なんか巷でCoqがはやっているようなので - 菊やんの雑記帳なんかおもしろそうなので一つ簡単な命題を証明してみた。証明したこと Lemma answer_length : forall…

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket…

ocaml-nagoyaのプログラミング合宿に参加してきました。一泊二日で長野の麻績(おみ)に行って、鍋も食べ、焼肉も食べ、酒も飲み、コーディングもして、発表もするというハードなスケジュールでしたが、久しぶりにocaml-nagoyaのメンバーにも会えて非常に充実…

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。Coqでの型クラスは次のように宣言するみたいだ。 Class HMonad (M: T…

OCaml Meeting に行ってきました。 id:camlspotterさんid:osiireさんid:keigoiさんharreさんid:mzpさんid:Gemmaさんそしてid:zyxwvさんおつかれさまでした。OCaml入門者向けから、上級者向けまでさまざまな講演があって非常に楽しめました。OCamlという言語…

オープンソースカンファレンス2009 Nagoya - オープンソースの祭りだぎゃーに行ってきました。 スタッフの皆様おつかれさまでした。ocaml-nagoyaのメンバーは残念ながら今回少なかったですが、セミナーはかなりのお客さんが来てくれました。ブースにも何人か…

プログラムでリストや文字列を扱うことがあるが、これらに関する性質をチェックしたいと思ったらどうしたらよいだろうか？例えばリストを逆順にするrevという関数を定義したときに、rev (rev l) = lという性質が、いかなるリストlでも必ず成り立つということ…

最近仕事でlistの要素を仲間分けしてリストのリストを返す 次のような関数をOCamlで定義した。 let rec classify rel l = match l with | [] -> [] | x::xs -> let (ys,zs) = List.partition (fun y -> rel x y) xs in (x, ys) :: classify rel zs この関数…

Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…

SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。問題はペア構造のチャーチエンコーディングの話。Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。 …

Coqがversion 8.1から8.2にバージョンアップしました。変更点は以下のいろいろ。 Haskellのような type class system が導入されました coqcでコンパイル後のvoファイル を扱うcoqchkというツールが追加されました Setoidのための書き換えタクティック setoi…

でした。

Coqで高精度計算サイト 高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。 それは大きな数を扱うことができないということである。 例えば10^10000000のような大変大きな計算を実行すると答…

CoqではExtractionという機能があるためにOCamlやHaskellなどの関数型言語との連携が容易である。 CoqでOCamlの型や関数を使いたい場合は単に関数の引数として渡せば良いだけだからである。 ただ、沢山の型や関数を一度に渡したい場合、結構面倒である。Coq…