Coq
ssreflect
coqide
名古屋のIoTは名古屋のOSで

導入

MacintoshでCoqide
https://qiita.com/kaizen_nagoya/items/0314ca15130bdfa9dce2

なぜCoqが重要か
https://qiita.com/yoshihiro503/items/7e6a9994eb37ed7c3bf9

Emacs & ProofGeneral で Coq 使い分け
https://qiita.com/mathink/items/0f3f5e8620ba54266161

確認・説明

「OCaml入門」入門
https://qiita.com/kaizen_nagoya/items/456bedf9f68b512663da

coqはOCamlで記述している。OCamlを知っているとよい。

初心者が陥りそうな罠 〜なんでもintrosすればいいってわけじゃない〜
https://qiita.com/kimitaka@github/items/7879ea3133fe378b178c

Proof General が "Searching for program: No such file or directory, coqtop" というときの対処法
https://qiita.com/kimitaka@github/items/3790ec770887d55af540

Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた
https://qiita.com/erutuf13/items/98f15cc7e74b0570c971

Coq のカリー・ハワード同型周辺について
https://qiita.com/wgag/items/d44f683bfdc5eb297466

Coq: 引数にパターンが使えるようになったので試してみた
https://qiita.com/mathink/items/056c8d14d38ba848c839

autoで何が起きたのかわからないときに
https://qiita.com/OKU_K/items/e0bdd2b21dd9c708b31c

Coq の Variable と Parameter の違い
https://qiita.com/amutake/items/5ab7df143906ddbfc926

Coq: Set Primitive Projections と injection タクティックのお話
https://qiita.com/mathink/items/a986fb445d6d36b1a119

Coq(とか)のバージョンを簡単に切り替えたいスクリプト
https://qiita.com/mathink/items/4dfd32b1c9847ea23db9

Coqで型クラス
https://qiita.com/yoshihiro503/items/a6fe93ae0d867129f7b1

Coqでもあのニンジャパターンマッチが使えるぜ
https://qiita.com/yoshihiro503/items/c83fb2a6e2a6318db108

coqdocで日本語を含むPDFを生成する
https://qiita.com/yoshihiro503/items/2e3035cc602301c7c9fc

Verlang と Coq の Extraction について
https://qiita.com/amutake/items/db595761435c01356e88

wercker を使って Coq コードを CI する
https://qiita.com/amutake/items/d75bb63eeda9ec33df8d

vimでCoqを使えるようにする
https://qiita.com/Kitaryo/items/1c0a6ed3f6b8e1062859

Coqのemacsモードのプロンプトについて調査
https://qiita.com/shinsa82/items/b03f5202989ddf09a280

Proof Generalのholes-modeを無効化
https://qiita.com/OKU_K/items/c578b4b34e74f4c762f3

Ssreflect

Elgamal暗号でSSReflectのトライアル
https://qiita.com/junjihashimoto@github/items/dda7720dc49c346a7918

整数を使った証明(整数精度のHaar変換)のトライアル
https://qiita.com/junjihashimoto@github/items/310d87e504ee79d691af

リフレクションのしくみをつくる
https://qiita.com/suharahiromichi/items/9cd109386278b4a22a63

SSReflectノート (暫定版)
https://qiita.com/suharahiromichi/items/d16bebbe6f6c98f76d78

スタックコンパイラの証明
https://qiita.com/suharahiromichi/items/c5bfeb39f96b6199e67a

SSReflectのViewとView Hintについてのメモ
https://qiita.com/suharahiromichi/items/02c7f42809f2d20ba11a

「リストは自分自身のfoldr関数として定義される」について
https://qiita.com/suharahiromichi/items/4bd2483d7aa766a570da

形式化された不完全性定理の証明
https://qiita.com/suharahiromichi/items/d249d4a5c5a3072677e1

試作

Coq を使って「どう書く」の問題を解いてみた 〜五角形の世界であなたは過去の自分に出会う〜
https://qiita.com/t_uchida/items/a263656fe28067538895

Equiv_Jの練習問題assign_equivの証明 #ProofCafe
https://qiita.com/yoshihiro503/items/5a6eb6f0c8d2b96c4d4c

Equiv_Jの練習問題 WHILE_true
https://qiita.com/yoshihiro503/items/260b9342ab049778ef11

第33回 #ProofCafe での練習問題のssreflectを使った解答例。
https://qiita.com/yoshihiro503/items/0bca75e5ab52e40f01f6

Coqで鳩の巣原理の証明
https://qiita.com/yoshihiro503/items/0233bf2ada9b8bfa00fa

「The Little Prover」のCoqでの実現
https://qiita.com/suharahiromichi/items/723896ebfbc332f9d3dd

Coqで証明書いてみた
https://qiita.com/Thought_Nibbler/items/9ed7da5ecfa046c8f9f5

「Coqで証明書いてみた」の1行づつの実行を記録してみた。
https://qiita.com/kaizen_nagoya/items/6b8398bf6980315945c6

eqの性質の証明
https://qiita.com/lion/items/44b41c5e7a9c41887fe4

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

Falseの証明
https://qiita.com/lion/items/7e0b6b65700beec7dbd7

Coqコーディング規約
https://qiita.com/yoshihiro503/items/730eba53797de7a23328

CoqでFixを使って再帰関数を定義してみる
https://qiita.com/yoshihiro503/items/d92e67029929e4335022

Coqの初歩メモ
https://qiita.com/lion/items/b773d76538f57ead9599

二分探索木を Coq with SSReflect で弄くる
https://qiita.com/mathink/items/e56b138bb02133a179aa

Coq: Vernacular コマンド備忘録
https://qiita.com/mathink/items/9be0be5761625cc9e12e

Coq: nat を string で十進表記する
https://qiita.com/mathink/items/a8006421da7dec717849

Coq で map や filter の fun を省略したい。
https://qiita.com/mathink/items/93fe64cb51ec25c111e9

依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)
https://qiita.com/mathink/items/5bd5990c9202a3e55858

Coq で半環
https://qiita.com/mathink/items/a4f5ef2320e03e8ef0e0

Coq で環
https://qiita.com/mathink/items/0fff555fa1824248d88a

Coq で環のイデアルを作ってみる
https://qiita.com/mathink/items/0e40ba9d2324c6aaaa24

代数的構造と Coq:序
https://qiita.com/mathink/items/c5027bf2dc3727ffcf69
https://gist.github.com/mathink/99fd4c7693a4468894d0
入力して確認したら次の警告が出た。

Nested proofs are deprecated and will stop working in a future Coq
version [deprecated-nested-proofs,deprecated]

Setoid の Proper な Map を作る。
https://qiita.com/mathink/items/ab8037926f91b51d1e96

Coq で圏論:背景と普遍性について
https://qiita.com/mathink/items/2067c162fb7cf8f6c83f

Coq で圏論:自然変換とデータ型
https://qiita.com/mathink/items/6d635284ff4564e413f9

Coq で圏論:函手とその等価性
https://qiita.com/mathink/items/d827ee3b895ed80a3285

Coq で圏論:随伴、モナド、Kleisli triple
https://qiita.com/mathink/items/dc2a555436c90b23df00

Coqの余帰納法でハマってしまった
https://qiita.com/Nogikuchi/items/28f2f573537ff3e5aca5

Godel’s Incompleteness Theorem in coq
https://qiita.com/kaizen_nagoya/items/181cb3dae504f64d0619

資料

Coqで学ぶ定理証明入門メモ
https://qiita.com/R_Asa/items/471330f39020d222c792

「型システム入門」と「ソフトウェアの基礎」の対応
https://qiita.com/suharahiromichi/items/77801c26fe5fde0d166a

AffeldtさんのSsreflect練習問題exo4
https://qiita.com/yoshihiro503/items/bd142fdb69c1fd64ab86

AffeldtさんのSsreflectチュートリアルのソースをビルドする
https://qiita.com/yoshihiro503/items/f5a5d6d59e5d844b4779

Ssreflect Tutorial最初のコード
https://qiita.com/yoshihiro503/items/6a1f0c6933daafd4754b

ssreflect tutorial(意訳版) [作業中]
https://qiita.com/mzp/items/b485ff9baaa8bfef788c

software foundations Equiv.v [havoc_copy]
https://qiita.com/wataruY@github/items/4fadb287024839ce0ea5

Syntax error: [prim:var] expected after 'move' (in [tactic:simple_tactic]).

Proof General 等

Coq + Proof Generalで使うキーシーケンス
https://qiita.com/watertight/items/894cb1ed85a32f4ba863

Coq-8.5の実装内にプリンタを加える(メモ)
https://qiita.com/hist102/items/c615efb786907b352813

じぇねらるたんシールの注文方法
https://qiita.com/yoshihiro503/items/a0c7df7e73090ee2b9a3

「じぇねらるたん」は、Coq環境Proof Generalの公式「幸運の象徴」(mascot)。
https://proofgeneral.github.io/

関連資料

試して面白いプログラミング言語6選
https://qiita.com/egisatoshi/items/f728108344f87840dfef

参考文献(slideshare)

Coq for beginners
https://www.slideshare.net/yoshihiro503/coq-for-beginners?qid=31470cba-b5b4-494f-88c0-cfbb29a286b8&v=&b=&from_search=22

Coq Tutorial
https://www.slideshare.net/tmiya/coq-tutorial?qid=d52bdc11-b110-4a9d-9cd2-9360fcfcfe2a&v=&b=&from_search=2

Coqの公理
https://www.slideshare.net/qnighy/coq-61260896?qid=31470cba-b5b4-494f-88c0-cfbb29a286b8&v=&b=&from_search=24

Coq to Rubyによる証明駆動開発@名古屋ruby会議02
https://www.slideshare.net/mzpi/coq-to-rubyruby02?qid=a640f65d-794a-42aa-878c-476223646b6b&v=&b=&from_search=8

Coq関係計算ライブラリの開発と写像の性質の証明
https://www.slideshare.net/yoshihiromizoguchi/coq-49044889?qid=de688aba-2f8e-4b04-bbbe-e6080868cdf8&v=&b=&from_search=11

母語方式Coq
https://www.slideshare.net/kaizenjapan/coq-59179301

文書履歴

ver 0.10 初校 20180317
ver 0.11 追記、分類 20180318
ver 0.12 参考文献slideshare追記 20180320
ver 0.13 「不完全性定理の証明」等追記 20180324
ver 0.14 OCaml入門をリンクに 20180325