Require Import

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

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

なぜか無い補題

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

CoqでHello, world!(改)

Coqで "Hello, world!" を標準出力させるのはちょっと難しい。 なぜならCoqはプログラミング言語ではなく、システム開発の支援をするツールであり、扱う言語は純粋関数型言語だからだ。純粋でない部分(外部に標準出力する部分)のために、今回は16行ほどのO…