Coq メモ

Coq インストール
https://github.com/coq/coq/releases/tag/V8.13.0
ブラウザでお試し
https://x80.org/rhino-coq/
Coq 入門記事
https://hzkr.hatenablog.com/archive/category/Coq
https://www.iij-ii.co.jp/activities/programming-coq/
タクティクの使い方等
https://magicant.github.io/programmingmemo/coq/index.html
Coq公式
https://coq.inria.fr/
標準ライブラリの証明が見れます
https://github.com/coq/coq/tree/master/theories
神戸大学のpdf 命題論理、述語論理、素朴集合論等の形式化
http://herb.h.kobe-u.ac.jp/snap/coq.pdf
「ソフトウェアの基礎」　プログラムの証明等
http://proofcafe.org/sf/
https://qiita.com/41semicolon/items/08b309f60b39256c577e
名古屋大学の講義資料
https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2018_AW/
Coq周辺ツールのリンク集
https://gist.github.com/yamarten/aebed640f962f0e06a7f2ea2f2f08608#coqコードや命題を生成するツール
リンク集
https://qiita.com/kaizen_nagoya/items/13566f0b2083ea8d4998
https://mametter.hatenablog.com/entry/20070813/p2
TopProver 問題集として使える
https://gist.github.com/asi1024/6d318cec8d761668922fb513a7a1441a
問題集
http://web.archive.org/web/20130609191210/http://as305.dyndns.org/aps/problem
Qiita Coq記事
https://qiita.com/tags/coq
ssreflectの使い方
https://qiita.com/suharahiromichi/items/ba3625e3a89ddae45ad3
https://qiita.com/suharahiromichi/items/d16bebbe6f6c98f76d78
https://qiita.com/suharahiromichi/items/02c7f42809f2d20ba11a
http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=9B197A7D5ACE04640405CF1C586E0942 ?
Coqが基づいている論理体系(CIC)とZFC集合論の関係
https://www.researchgate.net/publication/225243273_Sets_in_types_types_in_sets
標準ライブラリにあるCICに追加できる公理
https://qnighy.hatenablog.com/entry/2014/04/22/214515
Coq ブログ
https://lkozima.hatenablog.com/search?q=Coq
ご飯おかわり&進次郎の定理
https://www.mathwills.com/posts/135
https://www.mathwills.com/posts/101
僕はこれくらいしか分かりませんので
https://zenn.dev/sabataro
なんかすごいやつ
https://mathlog.info/articles/1405
Coqのデフォルトは直観主義論理ですよ
https://mathlog.info/articles/1153