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

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

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

Coqで多重再帰のデータ構造を証明する

Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_in…

しりとりの圏をCoqで実装してみた

Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…

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

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

OCamlから学ぶ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で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でHello, world!(改)

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