読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

LLFutureというイベントに行ってきます。

Gallinaについて軽く話します。

Coqで依存型

最近Agdaがはやっているみたいなので、Coqでも依存型(dependent type)を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…

CoqのソースコードをカッコイイHTMLページにする方法(coqdocを使う)

Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。 そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。 使いかたは以下。 $ coqdoc [Coqファイル.v] ここで、(** コメント *)…

CoqでProject Euler (problem 44)

Problem44が解けた? - みずぴー日記に触発されて、Project EulerのProblem 44に挑戦してみた。 問題44: 五角数は Pk = k(3k-1)/2で生成される. 五角数のペア PmとPnについて, 差と和が五角数になるものを考える. 差を D = |Pm - Pn| と書く. 差 D の最小値を…

CSNagoyaでHaskell勉強会

名古屋でHaskellの勉強会をやるという噂を聞いたので、行ってきた。CSNagoyaという勉強会で、教科書は「ふつうのHaskellプログラミング」。みんなで音読していくという方式で、ノートPCを持ってきていない人と持ってきている人でペアプロミングしながら、理…

PPL2008に行ってきた。

Coqでπ計算などで有名なReynald Affeldtさんから、貴重な意見がいただけたり、楽しい話がたくさんあったりで、非常に素晴らしい経験だった。 驚いたこと プログラミング in OCamlでも有名な五十嵐先生のところの研究室では、CALと呼ばれる、小さい証明器を使…

Coqで、クイックソート

(* 注意:今回はCoq 8.1以上を使用。 *)今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では…

Coqで”無限オブ無限”(証明部分)

ヒビルテで、さかいさんが興味深いCoqのコードを紹介していた。 ⇒ λ. Coqで“無限オブ無限” どうやら元ネタはここ(derive your dreams)らしい。おもしろそうなので、さかいさんのコードを証明してみた。証明した定理は以下。 Theorem main : forall m n:nat, …

セマンティクス

(*****************************************) (** SEMANTICS *) (*****************************************) Require Import List. Section ListAssoc. Variable A B:Set. Variable A_beq : A -> A -> bool. Fixpoint List_assoc (l:list (A*B))(a:A){str…

シンタクス

(*****************************************) (** SYNTAX *) (*****************************************) (** 基本データ構造を二分木構造で定める *) Inductive DATA:Type := | DNIL : DATA | DCONS : DATA -> DATA -> DATA. Inductive VAR : Type := | …

Coqでつくる手続き型プログラミング言語

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

Coqでニコニコ :-]

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

PeanoZArith.v

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

PeanoPositive.v

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

二進表現じゃない整数型

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

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

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

大阪人に関するうわさ

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

定義と、その展開

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

Coqのインストール

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

Coqのインストール

Coqのサイトが見れない

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

データベースを用いるWebアプリケーション

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

Coqで大学院試験

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

さあ!証明しよう!

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

1行でできるCoqプログラム

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

Coqのソースコードをコンパイル

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

OCamlから学ぶCoq

1 Coqは関数型言語OCamlとよく似ている部分が多いので、OCamlをやったことがある人は、Coqを理解するのが早いだろう。 逆に、Coqに慣れると、OCamlのプログラムが楽々かけるようになるだろう。 今日は、OCamlの視点からCoqの中身を見てみよう。 基本型 OCaml…

Variableコマンドと抽象化

この記事は途中です。

関数の定義、型の定義

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…

CoqでFizzBuzz

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でFizzBuzz

CoqでHello, world!(改)

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

Coqの世界から現実世界へ

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

Coqで作った関数を実生活で使用する

Coqの型とOCamlの型

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

Coqの型とOCamlの型

Coqで書いた定理を証明してみる

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

Coqで定理を書いてみる

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

Coqの起動のしかた

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

Coqでの証明

はてな日記を始めました!

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