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

Definitionコマンドを使って型や、関数を定義することができるが、証明の中で、定義に戻って展開したくなる時がある。例えば次のような２足す関数を定義して、それを二回適用すると4になるような定理を証明したい場合を考える。 Welcome to Coq 8.1 (Feb. 20…

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

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) :…