導入

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

資料

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

Sign up for free and join this conversation.
Sign Up
If you already have a Qiita account log in.