coqは、今井宜洋　@yoshihiro503　さんから教わった。

Proof Cafeという名古屋の勉強会を主催されていた。

最近Youtubeに動画を登録された。

Coq勉強会 by 今井宜洋

動画で出て来る単語の説明。

3110 Coq Tactics Cheatsheet

「simple」
Simplifies the goal or hypotheses in the context.

「unfold」
unfold: Unfolds the definitions of terms.

Command Index

「print」

「omega」
Omega: a solver for quantifier-free problems in Presburger Arithmetic

導入

MacintoshでCoqide

なぜCoqが重要か

Coqで学ぶ定理証明入門　TOP SE seminor at Nii

Coq IDEの導入と利用(TOP SE セミナ受講者のために）

macOSにbrewでcoq_jupyterをインストールする

Coqチュートリアル

VimでCoq 改

Visual Studio CodeでCoqの環境作ってみた

vimでCoqを使えるようにする

WSLにcoq-jupyterをインストールする

確認・説明

「OCaml入門」入門

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

初心者が陥りそうな罠 〜なんでもintrosすればいいってわけじゃない〜

Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた

Coq のカリー・ハワード同型周辺について

Coq: 引数にパターンが使えるようになったので試してみた

autoで何が起きたのかわからないときに

Coq の Variable と Parameter の違い

Coq: Set Primitive Projections と injection タクティックのお話

Coq(とか)のバージョンを簡単に切り替えたいスクリプト

Coqで型クラス

Coqでもあのニンジャパターンマッチが使えるぜ

coqdocで日本語を含むPDFを生成する

Verlang と Coq の Extraction について

wercker を使って Coq コードを CI する

超絶技巧演習問題 - Coq

coqでド・モルガンの法則の証明をするまで (命題論理版)

Coqのemacsモードのプロンプトについて調査

Coqメモ

直観主義論理 五つの定理の同値性

Ssreflect

Ssreflectは四色問題の現代的証明で著名。

Coq/SSReflect/MathCompの文献

数学ガールの「数学的帰納法」の問題

Coqでカタラン数

SSReflectノート (暫定版)

SSReflectのViewとView Hintについてのメモ

Elgamal暗号でSSReflectのトライアル

第33回 #ProofCafe での練習問題のssreflectを使った解答例。

二分探索木を Coq with SSReflect で弄くる

AffeldtさんのSsreflect練習問題exo4

AffeldtさんのSsreflectチュートリアルのソースをビルドする

Ssreflect Tutorial最初のコード

ssreflect tutorial(意訳版) [作業中]

@nekonibox

Coq/SSReflectでたった1行のコマンドで完全帰納法を適用する方法

Coq/SSReflectで辞書式順序で引数が構造的に小さくなる再帰関数をFixpointで定義する

Coq/SSReflectでperm_eqが不変条件であるような命題を証明するための帰納原理
https://qiita.com/nekonibox/items/233d23bf0fb7cad79e01

Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数を定義する

Coq/SSReflectで子ノード数が不定である一般の根付き木をInductiveに定義する

Coq/SSReflectで自然数nを引数に取ってn分木の型を返す型をInductiveに定義する

試作

Coq を使って「どう書く」の問題を解いてみた 〜五角形の世界であなたは過去の自分に出会う〜

Equiv_Jの練習問題assign_equivの証明 #ProofCafe

Equiv_Jの練習問題 WHILE_true

Coqで鳩の巣原理の証明

証明された Common Lisp / Emacs Lisp コードを手に入れる

「The Little Prover」のCoqでの実現

Coqで証明書いてみた

「Coqで証明書いてみた」の１行づつの実行を記録してみた。

eqの性質の証明

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

Falseの証明

Coqコーディング規約

CoqでFixを使って再帰関数を定義してみる

Coqの初歩メモ

Docker上にOCaml+Coqの環境を構築して動かしてみるまで

Ubuntu 18.04/19.10にcoq-jupyterをインストールする

Ubuntu18.04にCoqIDEをインストール

coq-hammerを試してみる

Coq: Vernacular コマンド備忘録

Coq: nat を string で十進表記する

Coq で map や filter の fun を省略したい。

依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)

Coq上で論理学を展開するとは？

Coq で半環

Coq で環

Coq で環のイデアルを作ってみる

代数的構造と Coq：序

入力して確認したら次の警告が出た。

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

Setoid の Proper な Map を作る。

Coq で圏論：背景と普遍性について

Coq で圏論：自然変換とデータ型

Coq で圏論：函手とその等価性

Coq で圏論：随伴、モナド、Kleisli triple

Coqの余帰納法でハマってしまった

Godel’s Incompleteness Theorem in coq

整数を使った証明（整数精度のHaar変換）のトライアル

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

スタックコンパイラの証明

「リストは自分自身のfoldr関数として定義される」について

形式化された不完全性定理の証明

資料

Coqで学ぶ定理証明入門メモ

「型システム入門」と「ソフトウェアの基礎」の対応

software foundations Equiv.v [havoc_copy]

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

Proof General 等

Spacemacs上のProofGeneralでEasyCryptを動かす

Emacs & ProofGeneral で Coq 使い分け

Proof General が "Searching for program: No such file or directory, coqtop" というときの対処法

Proof Generalのholes-modeを無効化

Coq + Proof Generalで使うキーシーケンス

Coq-8.5の実装内にプリンタを加える（メモ）

じぇねらるたんシールの注文方法

「じぇねらるたん」は、Coq環境Proof Generalの公式「幸運の象徴」(mascot)。

関連資料

試して面白いプログラミング言語6選

参考文献(slideshare)

Coq for beginners

Coq Tutorial

Coqの公理

Coq to Rubyによる証明駆動開発@名古屋ruby会議02

Coq関係計算ライブラリの開発と写像の性質の証明

母語方式Coq

errors

coq error

Coq Seminorの演習結果（2）

link

Coq関係計算ライブラリの開発と写像の性質の証明

Coqで学ぶ定理証明入門　TOP SE seminor at Nii

文書履歴

ver. 0.10 初校 20180317
ver. 0.11 追記、分類 20180318
ver. 0.12 参考文献slideshare追記 20180320
ver. 0.13 「不完全性定理の証明」等追記 20180324
ver. 0.14 OCaml入門をリンクに 20180325
ver. 0.15 URL追記 20190822
ver. 0.16 Coq勉強会 by 今井宜洋 追記 20200321
ver. 0.17 @nekonibox 追記 20210812
ver. 0.18 資料追記　分類見直し 20210901