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

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

2007-06-20

なぜか無い補題

雑談 Lemma Require Import Open Scope Proof Qed intros apply rewrite

Coqのライブラリにはなぜか無い補題というものがある。例えばZmult_le_reg_rというレンマはZArithのZorderライブラリにあるが、これの左バージョンは無いのだ。ちなみにZmult_le_reg_rとは次のような内容である。 Zmult_le_reg_r : forall n m p:Z, p > 0…