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

今日はCoqを使って大学院試験を解いてみよう。 題材は京都大学 理学研究科 数学専攻の数学の問題だ。 せっかくなので一番 新しい平成１９年度の問題に挑戦してみよう。 （＊＊ 注意！！今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いた…

今日紹介するコマンドはProofコマンドだ。 このコマンドは何もしない。 Proofというからには、自動証明をやってくれるだろう、とか、何かすごいCoqの力で証明が変形するのかな、とか思う人がいるかもしれないが、このコマンドは何もしない。 このコマンドを…

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

Coqでいろいろ作ってみたり、証明をしてみたりできたら、そのとき入力したコマンドやタクティックをファイルに保存してみよう。 ファイル名は〜.v というふうにドットvで終わるようにしよう。これで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 〜;;」…

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

fizzbuzz.vの概要 Inductive FizzBuzzType : Set := | numb : A -> FizzBuzzType | Fizz : FizzBuzzType | Buzz : FizzBuzzType | FizzBuzz : FizzBuzzType. Definition is_fizz (a:A) := ismultiple_dec a A_three A_gt_three_zero. Definition is_buzz (a:…

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などの基本的な型であ…

証明モードのときは今までのCoqコマンドに加えて、タクティックというものを使うことができる。 タクティックは必ず小文字で始まり、ドットで終わる。 s intro. A : Prop ======================================= forall B C:Prop, (A->B->C) -> (A->B) -> …

Coqは証明支援系 (Proof Assistant) と呼ばれるシステムで、定理などの証明を構築することができる。 今回はTheoremというCoqコマンドを使ってみる。 このコマンドを使って定理を記述し、宣言することができる。 文法 [Theorem 定理の名前 : 定理の内容.] 最…

ターミナルでcoqtopと入力すると対話型証明支援系Coqが立ち上がる。 さあ、今日からCoqを使ってみよう！ /yoshihiro$ coqtop Welcome to Coq 8.0pl3 (Jan 2006) Coq CoqではCoqコマンドというものを使って操作をおこなう。 まず最初にCoqを終了するCoqコマン…

よろしくおねがいします。