δ-reduction δ-reduction は変数をその定義で置き換える。まず何か定義して、 Coq < Definition hoge := fun x:nat => 2+x. hoge is definedcbvを実行してみる。 Coq < Eval cbv delta [hoge] in (hoge 3). = (fun x : nat => 2 + x) 3 : natこの場合は「hog…

change term ゴールとtermが変換可能なときに、ゴールをtermで置き換える tacic。simpl とかを適当に使った結果、やりすぎていらんとこまで置き換えてしまった場合とか、逆に何をどう使えばもっと簡単に置き換えることができるのか分からない場合に使うとよ…

assert form ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。 ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。中間結果 form を指定すると、サブゴールにformが…

Coq in a Hurryの練習問題の一番最後。 とすると であるから、となる正の整数の組のなかで、最小のをとってくる。 すると、であるから。これは矛盾であり２の平方根が有理数でないことの証明になっている。 この証明をCoqを使って書け。 これはとてつもなく…

assumption この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。 intro この tactic はチュートリアルで普通に理解できる以上の機能はない。 結論が「forall x:T, U…

Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。 このtacticの語彙が多いほど証明の記述は楽になる。 しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。 exact ter…

久しぶりに行った神保町で、前原昭二著「数学基礎論入門」なる本を1000円で買ってきた。 不完全性定理の証明にゲーデルの論文をほぼそのまま使っているのがこの本のポイント。 今までまじめに不完全性定理の証明なんて読んだことなかったので、まじめに読ん…

Coqにおける等号は「Leibniz Equality」というもので、 (forall P: Prop, P x -> P y) <-> x = y.つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。等しくないことを示すにはどうすればよいかというと、結果が…

メイドさんに教わったCoqというものをマニュアルと格闘しながら理解したつもり。 Variables A B : PropA と B は命題だよ。 Theorem mp : (A->B)->A->B. auto. Qed.modus ponens ぐらいは自動で証明できるよ。 Variable p : A->B. Variable a : A.なぜか知ら…