このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

Coqで高精度計算サイト 高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。 それは大きな数を扱うことができないということである。 例えば10^10000000のような大変大きな計算を実行すると答…

次の１行を書いて、〜.vというファイルを作ってみよう。 Extraction "plus.ml" plus. これであなたも立派なコカーだ！じゃあ早速コンパイルしてみよう。 /yoshihiro$ coqc 〜.v これで、plusという名前のCoqにもともと用意されている足し算関数がOCamlに変換…

Coqでいろいろ作ってみたり、証明をしてみたりできたら、そのとき入力したコマンドやタクティックをファイルに保存してみよう。 ファイル名は〜.v というふうにドットvで終わるようにしよう。これでCoqのソースファイルは完成だ！ じゃあ、そのソースファイ…

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

Coqの中で定義したり証明の対象にした関数を、ふと日常生活で使いたくなるときがある。 そんなときはExtractionコマンドが大変便利である。 文法 [Extraction 関数名] 例えば次のような恒等関数を作ってExtractionしてみる Coq Definition id (A:Set)(x:A) :…

Coqは非常に疑り深いのでOCamlなどの普通のプログラミング言語の型を全然信頼しない。 このため、CoqからExtractionで引き出した関数を使う場合はCoqの型からOCamlの型への変換をしなければならないことがある。 それはint, nat, stringなどの基本的な型であ…