にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Fixpoint

Coqで数学的帰納法

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

ポジティブ型とマイポジティブ型

(** Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 *) 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。…

データベースを用いるWebアプリケーション

お客さんがWebブラウザを使って、入力項目をデータベースに登録したり、データベースからデータを取ってきたりする仕組みは、多くの場所に存在するだろう。 このような仕組みは比較的簡単に提供することができ、かつ、利用する人の生活を便利にしてくれる。…

OCamlから学ぶCoq

1 Coqは関数型言語OCamlとよく似ている部分が多いので、OCamlをやったことがある人は、Coqを理解するのが早いだろう。 逆に、Coqに慣れると、OCamlのプログラムが楽々かけるようになるだろう。 今日は、OCamlの視点からCoqの中身を見てみよう。 基本型 OCaml…

関数の定義、型の定義

Coqでは関数や型を定義するための簡単なコマンドが三つある。 Definition, Fixpoint, Inductiveである。 Definitionについて CoqではDefinitionコマンドを使って関数を定義することができる。 Coq Definition f x := x+1. f is defined OCamlの「let 〜;;」…