(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。 そんなときは、Show Scriptコマンドで整形すると…

こんな感じの画像を生成してくれます。リファクタリングのお供にどうぞ。 何をやるの? coqdepの出力をdotファイルに変換する dotファイルをGraphvizで画像に変換する 使い方 $ coqdep -I . *.v | ruby depends.rb > depend.dot $ dot -Tpng -o depend.png de…

Coqでラムダ計算を証明してみた - みずぴー日記の続けて、単純型付きラムダ計算の型推論(Type reconstruction)に関する定理の証明をしてました。そして、とうとう健全性と完全性の証明ができました! やったね! GitHub - mzp/lambda at c0123fd0ca42d545f9e45…

Coqを使っていたら、coqcを落すコードに出会ってしまいました。 コード Require Import Sets.Ensembles. Variable (P: Prop). Variable (A: Type). Hypothesis the_hypo : forall x, exists xs, In A xs x -> P. Theorem some_theorem : P -> P. Proof. intr…

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式 型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT …

定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。 要約 Inductiveに定義したPropのほうが使いやすいらしい Inductiveに定義したPropの各名前は、applyできる Inductive Xを定義するとX_indが自動で定…

今日もTypes and Programming Languages (The MIT Press)に載っている定理の証明です。 type_dec 補題を定義する際に、以下のような定義が必要になりました。 Definition type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}. で、これを証明するために…

前回までで作った型付け規則を元に、Types and Programming Languages (The MIT Press)に載っている「Inversion of the typing relation補題」の証明にチャレンジしました。Inversion of the typing relation補題は Lemma LambdaRel : forall (x : string) (…

とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediat…

前回作ったラムダ式の上に、evalを定義しました。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰関数の定義は、かなり厳しい制約があるっぽい よく分からないこと 最初、termを与えると値になるまで評価するevalを書い…

バリアントでラムダ式を作って、その上でsubstituteを定義してみました。目指してるのは単純型付きラムダ計算です。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰のあるバリアントはInductiveで定義する 相互再帰のあ…

最近Coqが流行してるので、ボクも流れに乗ってみました。今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。 Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. そののために、appendを定義したり…