Basics_J
プログラミング言語Coqには、ほとんど何も（ブール型や数値型すら）ビルトインされていません。その代わりCoqには、新しい型やそれを処理するための強力なツールが用意されています。 まず最初はとても簡単なサンプルから始めましょう。次の定義は、Coqに対して、新しいデータ型のセット（集合）である'型'を定義しています。その型は日で、要素は月曜日、火曜日...などです。その定義の1行は以下のようにも読めます。"月曜日は日。火曜日は日"といった具合です。 Inductive day : Type := | monday : day | tuesday : day | wednesday : day | thursday : day | friday : day | saturday : day | sunday : day.
Coqの入門記事を書く会 (4) - ひとり勉強会
今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。 英語 言語そのものを浅く/深く眺めていく、という方向のテキスト３つ： Coq in a Hurry 「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。 Coq Proof Assistant： A Tutorial 本家のチュートリアル Interactive Theorem Proving and Program Development (Coq'Art) Amazon 定番の一冊 講義の素材として作られたチュートリアル達。より具体的な題材での演習付きなので面白いかも： 2nd Asian-Pacific Summer School on Formal Methods Using Proof Assistants for Programming Language Research or, H
メモ晒し - rfなブログ
自分の Coq メモを晒してみる。 ■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もしない)) ■tacticについて intro / intros 前提の導入 ゴールの forall や -> で括られた部分を前提へ intros で名前を付けるときは左から 前提に持って行かない場合は、名前を _ にする (intros のみ) apply 前提 A -> B、ゴール B があるとき、ゴールを A にする ゴールに適用できる関数があるとき、apply 関数 でゴールに関数を適用する assert assert (前提の名前 := 式) で、式によって証明させる
証明してみた。 - 菊やんの雑記帳
http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。 とりあえず、問題設定 Axiom A : Set. Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }. Axiom A_mul : A -> A -> A. Axiom A_zero: A. Axiom A_one: A. Infix "*" := A_mul. Notation "0" := A_zero. Notation "1" := A_one. Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c). Axiom A_mul_comm: forall a b, a * b = b * a. Axiom A_mul_1_r: forall a,
Program Verification Through Characteristic Formulae
This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then prove that the program satisfies a given specification by reasoning interactively about the characteristic formula using a proof assistant such as Coq
ヒビルテ(2010-06-17)
λ. Whyでバブルソートの正当性を示す 計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。 BubbleSort.java これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。 定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。 以下が結果の画面。 gwhyのこのインターフェースはテストツー
Whyインストールメモ - kencobaの日記
Whyツールの習得について( http://groups.google.co.jp/group/fm-forum/browse_thread/thread/6fbd1bc05aa8f999) ということで、 私もやってみた。 Whyというのはプログラムの検証用ツールなのだが、 プログラムコードにアサーションのように挿入したWhyのコードを もとに、プログラムを自動的に検証してくれるという、 なんだか素晴らしい仕組みを持っているのだ。 私の環境はUbuntu。 1.インストール Coq(apt-getでインストールできる)以外に必要なものは、 why-2.24.tar.gz(http://why.lri.fr/) いくつか追加でパッケージが必要。 全部sudo apt-get installでインストールしておく。 libocamlgraph-ocaml-dev(これがないとconfigur
OCamlerのためのCoq便利モジュールを公開してみた - にわとり小屋でのプログラミング
このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。 ダウンロード: http://sourceforge.jp/projects/coqbase/ 具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を使った型安全なprintf関数 natからOCamlのint、stringからOCamlのstringへの相互変換関数 Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
Certified Programming with Dependent Types
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
Coq Tips
以下、Parameters A B C P Q R : Prop. を仮定。 目次 前件 (仮定) が……の場合 仮定が False の場合・仮定に矛盾がある場合 仮定が否定の場合 (~A の形) 仮定が含意の場合 (A -> B の形) 仮定が連言の場合 (A /\ B の形) 仮定が選言の場合 (A \/ B の形) 仮定が全称量化子 (forall) の場合 仮定が存在量化子 (exists) の場合 後件 (ゴール) が……の場合 ゴールが True の場合 ゴールが False・否定の場合 ゴールが含意の場合 (A -> B の形) ゴールが連言の場合 (A /\ B の形) ゴールが選言の場合 (A \/ B の形) ゴールが全称量化子 (forall) の場合 ゴールが存在量化子 (exists) の場合 ゴールが恒真命題 (トートロジー)
2009-10-23
Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。 東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん 自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。 まず、自然数全体の型 nat を定義する。 Inductive nat : Set := | O : nat | S : nat -> nat. 次にこの自然数上での足し算を計算する plus 関数を定義する。 Fixpoint plus x y := match x with | O => y | S x => S
ハノイの塔 - 菊やんの雑記帳
久しぶりにCoqで遊ぼうかと思って、いい問題はないかと考えたところ、ハノイの塔あたりが面白いんじゃなかろうかということで証明してみた。 証明したいことはハノイの塔を完成させる最短手数は2^n-1であること… と思って少し書いてみたんだけど、これはかなり大変だということになって、ハノイの塔の解等を計算する関数が正しく解になっていることを証明することを最初の目標としてみた。 問題設定は以下の通り Inductive pos : Set := pos1 | pos2 | pos3. Inductive move : Set := | from_to (from to: pos): move. Definition tower := list pos. Definition moves := list move. Fixpoint single_tower (t: tower) (p: pos)
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://adam.chlipala.net/cpdt/cpdt.pdf