Coqで多重再帰のデータ構造を証明する

Coq Inductive induction

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

2009-07-08

Coqで数学的帰納法

Fixpoint induction

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

2007-08-26

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

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

2007-06-28

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

Fixpoint Lemma Theorem Proof Qed intro intros case unfold fold induction reflexivity rewrite elim inversion apply assumption

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