Coqで命題論理の標準形

この記事はTppMark11の問題をCoqでやってみたという内容である。問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Ter…

依存関係のある値のうちの一部をrewriteしようとしたときの問題

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表…

OCamlとCoqを連携してIO処理をモナディックに扱う

この記事は OCaml Advent Calendar の5日目の記事です。OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。 http://github.com/yoshihiro503/coqioこのライブラリを使えば、例えば次のようなコードを書くことができる。 Require I…

証明された証明支援器をScalaで書いてみた

この記事はTheorem Proving Advent Calendarの7日目の記事である。静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが…

VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。

VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初め…

fold_leftとfold_rightが同じになるとき

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。 Definition xs := …

tmiyaさんの練習問題をラムダ式で解いてみた

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。このような…

CPS変換されたフィボナッチ関数の証明をしてみた

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。http://ideone.com/3CQOnしかしfib_cps関数をもっと美しく定義できないものだろうか。[…

Coqプログラマの集会、Coq庵でした

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。スライドは以下から参照できます。 Coq庵 - coqグループ

OCamlでlet recを使わずにfact関数を定義する

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

TDDBC名古屋に行ってきました。

TDD Boot Camp名古屋に参加しました。id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。 当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇…

Alloyセミナーに行ってきました

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記TDDBC名古屋で2日間テスト駆動開発を行った直後で…

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676まずは集合AとA上の掛け算とサクセ…

Coqで多変数多項式の簡約

変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary opera…

第3回 Formal Methods勉強会に行ってきました。

第3回FormalMethods勉強会 : ATND (via fm-forum @ ウィキ - トップページ) 場所は喫茶ルノアールというところの中にある会議室でした。 前半Alloyの話をid:kencobaさんが、後半はCoqの話をtmiyaさんがするという形式でした。13時から19時まで6時間でしたが…

OCamlerのためのCoq便利モジュールを公開してみた

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

迷路の試験問題を解いてみた

Coq

参考:人材獲得作戦・4 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る…

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

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

Getting Started with Agda アグダを始めよう

Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。OSのディストリビューションは最近リリースされた Ubuntu 9.10。 非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。 Agdaのインストール Agdaの標準…

直観主義論理での二重否定除去と排中律の同値性

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。 Lemma p10_left : (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)). Proof. intros. apply H. intro. elim (H0 H2). apply H1. Qed. …

1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。 Proposition p09 : forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C. Proo…

あるソート関数がちゃんとソートする事を証明

以前Merge Sort を実装して証明した。 http://d.hatena.ne.jp/yoshihiro503/20090923ソースコード全体は以下。 http://bitbucket.org/yoshihiro503/mergesort/

reverse (reverse list) == listとなる事を示す

http://d.hatena.ne.jp/yoshihiro503/20090708 で証明した。

リストの結合関数 ++ の結合則 l1 ++ (l2 ++ l3) == (l1 ++ l2) ++ l3

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。 Require Import List. Proposition p06 : forall {A} (l1 l2 l3:…

中間値の定理(The Intermediate Value Theorem)

中間値の定理もCoqの標準ライブラリに存在する。Rsqrt_def.vの中にIVTという名前で見つけることができる。 Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }. ただ、中間値が f x …

Bolzano & Weierstrassの定理(有界な数列は収束する部分列を持つ)

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている! Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。 Theorem Bolzano_Weierstrass : forall (un:nat -> R) (X:R -> Pr…

実数の構成について

Coqでの実数は9つの項と17の公理で定義されている。項の型と意味はだいたい次の様な感じ。 Parameter R : Set. (* 実数全体 *) Parameter R0 : R. (* 実数の0 *) Parameter R1 : R. (* 実数の1 *) Parameter Rplus : R -> R -> R. (* 実数上での足し算 *) Pa…

(1 + 2 + ... + n) = n*(n+1) / 2の証明

この問題はCoqの自然数ライブラリを使った。まずを計算するsum関数を定義した。 Require Import Arith. Fixpoint sum n := match n with | O => O | S n => S n + sum n end. 自然数では割り算が難しいので、全体に2を掛けた次の形をまず証明する。 Lemma p0…

自然数(エンコーディングは問わず)の加算の可換法則、結合法則、分配法則を証明。

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。まず、自然数全体の型 nat を定義する。 Indu…

Proof Party の問題をCoqで挑戦してみた。

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん