とってもシンプルな言語をCoq内で定義してみた。次のような感じでプログラムは表現される。 (* プログラムの例 入力された２数を足し算するプログラム *) Definition plus_program := MAIN ( X O 詳細は以下

Coqで証明をする動画を作って、にこにこ動画に公開した。 http://www.nicovideo.jp/watch/sm1276083

次に、このPeanoPositiveを使って、PeanoZという整数型を作った。

まずこの前のコードに引き算のレンマを加えて、PeanoPositive.vとしてまとめた。

この前作ったマイポジティブ型は、ペアノの公理を元にした形式化だったので、それを使って、ペアノゼットという整数型を作ってみた。 既存のポジティブ型とマイポジティブ型との間の同型対応は、前回示してあるので、それをもとにしている既存のZ型とペアノ…

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

世の中には大阪人に関する間違った認識があふれているように思う。 例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。今回はそのような間違った俗説を払拭するべくCoqで証明してみた。 Coq Section なにわ. …

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

最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。 対象となる OS はWindows Vistaだ!Coqはだいたい次の３ステップで、使うことが出来る。恐れずに挑戦してみよう。 1。CoqのサイトからC…

なぜかCoqのサイトやOCamlのサイトなどが見れない。 困った。同じようなページが↓にあるようだ。とりあえず、ここを参考にしよう。 http://pauillac.inria.fr/coq/coq-eng.html

お客さんが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コマン…