CoqのソースコードをカッコイイHTMLページにする方法(coqdocを使う) - にわとり小屋でのプログラミング
Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。 そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。 使いかたは以下。 $ coqdoc [Coqファイル.v] ここで、(** コメント *)のように星二つで作ったコメントはドキュメントに青く出力される。特に大きい見出しとして出力したい場合は(** * 見出し *)というコメントにしよう。 コメント内でリンクタグなどのHTMLを書きたい場合は#で囲ったら大丈夫。 さらにスタンダードライブラリなど、どの関数や定理を使ったかリンクがたどれるドキュメントを作ることもできる。それには次のようなオプションつきで、コンパイルしなおしてからcoqdocするとできる。 $ coqc -dump-glob [新たに生成されるglobファイル] [Coqファイル.
OCamlとCoqを連携してIO処理をモナディックに扱う - にわとり小屋でのプログラミング
この記事は 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のソー
OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
今日は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で型クラス(Haskell風 モナドの定義) - にわとり小屋でのプログラミング
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は証明も第一級の値なので、なんらか満たしてほしい性質を型で指定することができる。モナドはモナド則を満たしてほしいので、モナド則をみたしていないといけないクラスにしよう。 モナド則を加えるとちょうどこんな感じになった。
Coqで、クイックソート - にわとり小屋でのプログラミング
（＊ 注意：今回はCoq 8.1以上を使用。 ＊） 今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。 Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。 Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。 しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。 例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。 (* クイックソートの定義 失敗例 *) Fixpoint qsort (l : list A) : list A := mat
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
