「The Little Prover」のCoqでの実現---「定理証明手習い」の「公理」をCoqで証明してみた
https://qiita.com/suharahiromichi/items/723896ebfbc332f9d3dd
を見て、何をどうすればいいか分からない人のための
「「The Little Prover」のCoqでの実現」入門
道具の準備
Macintosh
$ brew cask install coqide
The Little Prover
コピペして保存する。
ここではcoqというフォルダに保存。
名前はlittle prover.v
vという拡張子はVerilog HDLと重複する。
拡張子が重複するのはシステム全体では好ましくない。
ひとまずこのまま進む。
Cannot find a physical path bound to logical path matching
suffix <> and prefix mathcomp.
SSrefrelct等の入手
From mathcomp Require Import all_ssreflect.
「CoqのMathcomp/SSReflect拡張を使用しているので、それについては[3]を参照してください。」
[3] Mathematical Components resources
http://ssr.msr-inria.inria.fr/
参考資料
「coq入門」の入門
https://qiita.com/kaizen_nagoya/items/13566f0b2083ea8d4998
「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
文書履歴(document history)
ver. 0.01 初稿 20190217
ver. 0.04 URL追記 20230226
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.