はてなブックマーク

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表題の通り。シンプルな問題なので、レガシーCoq (version 8.4pl2) で説明する。 簡単のため、やや人工的な例を紹介する。 まず、正の自然数を引数にとる関数fを仮定し、その関数は引数が偶数のときは、戻り値はその半分になるとする。深い意味は無いので考えてはいけない。 Variable f : forall n : nat, n > 0 -> nat. Hypothesis h : forall (n : nat) (H : 2 * n > 0), f (2 * n) H = n. さて、ここで ある変数x

この記事は OCaml Advent Calendar の5日目の記事です。 OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。 http://github.com/yoshihiro503/coqio このライブラリを使えば、例えば次のようなコードを書くことができる。 Require Import Monad IO. Open Scope string_scope. Definition main : IO unit := do _ <- print "Hello" ; println ", world!". Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1。 このコードを次のコマンドでExtractすればcoq.mlというOCamlのソー

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。 Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。 Coqでの型クラスは次のように宣言するみたいだ。 Class HMonad (M: Type -> Type) := { mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B }. *1 この定義だとHaskellのモナドとあんまり変わらないが、Coqは証明も第一級の値なので、なんらか満たしてほしい性質を型で指定することができる。モナドはモナド則を満たしてほしいので、モナド則をみたしていないといけないクラスにしよう。 モナド則を加えるとちょうどこんな感じになった。

この記事はTheorem Proving Advent Calendarの7日目の記事である。 静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが実装されている。 しかしながら、Twitter社が使っていることなどで最近有名になっている関数型言語のScalaはそのような証明支援器はあまり見受けられない。これはScalaが言語処理系だけでなく一般のアプリケーションでも効果的であることを示している。そうは言ってもScalaで証明支援器を書いてもいいんじゃないかと思ったので書いてみた。 実装に関して、証明支援器のモデルを実装したCoqのライブラリを使用した。coq2scalaを使ってこれをScalaのライブラリと

今日は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 ワォ)

（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 ＊） 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq < Print Z. Inductive Z : Set := Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。 ここでpositiveという型が使われているが、これは１以上の整数全体を表している。 Coqでは、このpositive型に工夫がしてあって、現実のプログラムとの親和性をよくしている。 具体的には次のような再帰的な定義になっている。 Coq < Print positive. Inductive positive : Set := xI : positi

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。 ダウンロード: http://sourceforge.jp/projects/coqbase/ 具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を使った型安全なprintf関数 natからOCamlのint、stringからOCamlのstringへの相互変換関数 Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携

参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。 プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket。 思ったより簡単ではなく、いろいろなテクニックが必要で非常に勉強になった。Coq初心者の人はMergeSortの問題をとりあえずの目標にして証明を頑張ると非常に効率がいいのではないかと思う。 私は、だいたい以下の流れでプログラムした。 Sortedという命題を作り、リストがソート済みであるという状態を定義する mergesort関数があるとして、満たすべき性質(i)を定理として記述する mergesort関数を定義する mergesort関数に必要な補助関数 merge関数を定義し

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。 東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん 自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。 まず、自然数全体の型 nat を定義する。 Inductive nat : Set := | O : nat | S : nat -> nat. 次にこの自然数上での足し算を計算する plus 関数を定義する。 Fixpoint plus x y := match x with | O => y | S x => S

LL Future LL Futureでは、id:sumiiさんがラムダ式や、ユークリッドのアルゴリズムなどの歴史を語っていたのがおもしろかった。数学でのおもしろい概念は何百年後も利用されるのか。 じゃあ今、数学(や計算機科学)でホットな話題が100年後利用されるのかな？学術分野で今ホットなことってなんだろう？ 今回のイベントは未来のプログラミングがテーマなのに、全体的にプログラムの品質などについて言及している人が少なかった気がする。ちょっと不思議だと思った。 ともあれ、控え室などでいろんな人とお話出来たのはなによりの収穫だった。 Haskellのshelarcyさんとラムダな話ができた。未来のHaskellには依存型が入るとか、System Fが入るとか。 Haskellのid:nobsunさんと名刺交換できた。nobsunのソースコードから、厳格な厳しい感じの人を想像していたが、真逆だ

最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。 Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n). このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。 例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値

（＊　注意：今回はCoq 8.1以上を使用。　＊） 今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。 Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。 Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。 しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。 例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。 (* クイックソートの定義 失敗例 *) Fixpoint qsort (l : list A) : list A := mat

Coqで証明をする動画を作って、にこにこ動画に公開した。 http://www.nicovideo.jp/watch/sm1276083

世の中には大阪人に関する間違った認識があふれているように思う。 例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。 今回はそのような間違った俗説を払拭するべくCoqで証明してみた。 Coq < Section なにわ. まず、次のような文を定めて、６つの噂を仮定する。ただし ~（にょろ） は否定を表す記号である。 Coq < Variable 大阪人である : Prop. Coq < Variable たこ焼きを食べたことがある : Prop. Coq < Variable 常に縦縞の服を着る : Prop. Coq < Variable 嫁さんの尻に敷かれてる : Prop. Coq < Variable 阪神の試合には欠かさず行く : Prop. 大阪人である is assumed たこ焼きを食べたことがある is assumed 常に縦縞の

最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。 対象となる OS はWindows Vistaだ! Coqはだいたい次の３ステップで、使うことが出来る。恐れずに挑戦してみよう。 1。CoqのサイトからCoqのもとをダウンロード → 2。それを自分のパソコンにセットアップ → 3。起動 1。Coqのもとをダウンロード まずは Coqのサイト を見てみよう。(インターネットにつながっている必要がある。注意しよう) そこは黄色い雰囲気のサイトで、何やら英語でいろいろ書いてあるだろう。 よくみると[Coq 8.1]という項目の近くに鶏の絵があって、その近くに Download とかいてある部分が見つかる。そこをマウスでクリックしてみよう。 [The current version : Coq 8.1]という項目の中をよくよくさが