背景(back ground)
coqって、四色問題も解けちゃうって聞いて俄然やる気になった。
四色問題って、自分が十代の時に、計算機を使って解けたと話題になった課題。
飛び地のない国の地図を四色で塗りつぶせるかという。
かっこよく言えば、自分の人生がここで変わった。
こんなことやってる場合じゃない。計算機をつかわなきゃ。
でも当時は高価で、最初に買った計算機はプログラミング電卓。
導入(install)
Home-brew(brew)が入っていれば、一発。
$ brew cask install coqide
brew が入っていなかったら、qiitaの記事を見ていれてください。
例題(sample)
今、名古屋のProof Cafeでは、"The Software Foundations"を輪講中。
https://softwarefoundations.cis.upenn.edu/plf-current/index.html
ダウンロードするとplf-tarというファイルがあるのでダブルクリックで解凍する。
起動(start up)
アプリケーションフォルダにcoqideのアイコンが現れている。
これをダブルクリックすると起動する。
ファイルの読み込み
Lemma step_example1a :
(tapp idBB idB) ==> idB.
Proof.
apply ST_AppAbs.
apply v_abs.
Qed.
自己参照
「Coqで証明書いてみた」の１行づつの実行を記録してみた。
https://qiita.com/kaizen_nagoya/items/6b8398bf6980315945c6
coq(ide)を使おう または 初めてのcop(ide) mac編
https://qiita.com/kaizen_nagoya/items/a236dfbfaa4f946b4f8d
Godel’s Incompleteness Theorem in coq 壁いくつ、今壁4つ
https://qiita.com/kaizen_nagoya/items/181cb3dae504f64d0619
「Coqの余帰納法でハマってしまった」を記録
https://qiita.com/kaizen_nagoya/items/7c9e32a024aeaf7b5658
MacintoshでCoqide
https://qiita.com/kaizen_nagoya/items/0314ca15130bdfa9dce2
物理記事 上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff
数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d
プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945
一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39
小川清最終講義、小川清最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.
文書履歴
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.