Coqをはじめる

　数学の証明がわからないのでCoqを使いたいとまえから思っていた。
日本語で書かれた本もあるけれどよくわからなかった。
もっとわかりやすく書いてほしい。

Coq/SSReflect/MathCompによる定理証明 フリーソフトではじめる数学の形式化 [ 萩原 学 ]

結城浩さんや平山尚さんの本のようにわかりやすく文章を書いてほしい。

Java言語で学ぶデザインパターン入門増補改訂版 [ 結城浩 ]

ゲームプログラマになる前に覚えておきたい技術 [ 平山尚 ]

　Coqのドキュメントではじめた。moveをみてみた。
https://coq.github.io/doc/master/refman/proof-engine/ssreflect-proof-language.html#coq:tacn.move

Example

Require Import ssreflect.

Goal not False.

1 subgoal

============================
~ False

move.

1 subgoal

============================
False -> False

わからない。
ドキュメントの見方がわかったのはよかった。

SSReflectライブラリを使ってるんだから、ここからはじめることにした。

The SSReflect proof language — Coq 8.11+alpha documentation

 少しずつつづく。