coq(ide)を使おう または 初めてのcop(ide) mac編

背景(back ground)

coqって、四色問題も解けちゃうって聞いて俄然やる気になった。

四色問題って、自分が十代の時に、計算機を使って解けたと話題になった課題。

飛び地のない国の地図を四色で塗りつぶせるかという。

かっこよく言えば、自分の人生がここで変わった。

こんなことやってる場合じゃない。計算機をつかわなきゃ。

でも当時は高価で、最初に買った計算機はプログラミング電卓。

導入(install)

Home-brew(brew)が入っていれば、一発。

$ brew cask install coqide

brew が入っていなかったら、qiitaの記事を見ていれてください。

例題(sample)

今、名古屋のProof Cafeでは、"The Software Foundations"を輪講中。

ダウンロードするとplf-tarというファイルがあるのでダブルクリックで解凍する。

起動(start up)

アプリケーションフォルダにcoqideのアイコンが現れている。

これをダブルクリックすると起動する。

ファイルの読み込み

Lemma step_example1a :
  (tapp idBB idB) ==> idB.
Proof.
    apply ST_AppAbs.
    apply v_abs. 
    Qed.

自己参照

「Coqで証明書いてみた」の１行づつの実行を記録してみた。

coq(ide)を使おう　または　初めてのcop(ide) mac編

Godel’s Incompleteness Theorem in coq 壁いくつ、今壁4つ

「Coqの余帰納法でハマってしまった」を記録

MacintoshでCoqide

文書履歴

ver. 0.10 初校 20180317

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.