事情があって、AgdaかCoqを触ってみようか、と。
事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。
それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。
それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンスマニュアル）を眺めることにしました。ありっ？ こっちのほうが全然分かりやすいじゃん。まー、量がどえらく多い（全26章）ので第1章（Chapter 1）を斜め読みしただけですが、それでも、最初に抱いた疑問点や不満感はだいぶ解消しました。
僕の目的は、等式的な命題の証明を「紙と鉛筆」より楽に出来ればいいというだけで、それ以上に追求する気はサラサラないわけで、スタートラインから2,3歩進めればいい、と。以下、その程度の低い志の「Coq入門以前」の話です。
内容：
Coq処理系の使い方
Coqもプログラミング言語なんだから、コンパイラがあるでしょ？ あります。coqcってのがそうらしい。ですが、テキストエディタでCoqのソースコードを書いて、コマンドラインからコンパイルってスタイルはあんまり現実的じゃないですね。原則、Coqは対話的に使うものでしょう。
で、coqtopという対話的コマンドラインインタープリタがあります。プロンプトに対して1行ずつコマンドを入れていくスタイル。何かをお手軽に試したいときはこれでいいですが、少し長いコードになるとキビシイ。以前の入力を取り消したり修正したりしたいことは多いですが、コマンドラインインタープリタ（シェル）だと、それが困難です。
そんなわけで結局、coqideか、Proof Generalのような編集実行環境がないとCoq使えないです。僕は、Proof Generalを使うことにしましたが、C-c C-n、C-c C-u、C-c C-RET の3つのキーと、ツールバー（(tool-bar-mode 1) しておく）の操作で、何かをさせることは出来ます。インターネットからサンプルコーﾄﾞを拾ってきて、C-c C-nとかすると「あー、なんかやってるなー」と。
だけど、何やってんだ？ コレ。
Coqの言語って何なの？
「Coqのソースコード」とか「Coqのコマンド」とか書きましたが、何らかの構文に従ったCoq言語があるわけですよね。その言語でなにかを書くと、処理系がなにかやってくれる、と。
で、見よう見まねで（意味は分からずに）Coqコードを書いてみたのですが、異常に冗長じゃないですか、Coq。コマンド名の最初が大文字なので、シフトキーを押さなきゃならないし、DefinitionとかFixpointとか、それ、letとletrecでいいじゃん。モジュールの取り込みが Require Import Arith. って、RequireかImportのどっちか1つでいいじゃん。1 + 2 を評価するのに、Eval compute in 1 + 2. って、どんだけ丁寧に言えばいいの、あんた。それと、ソースコードの標準拡張子が「.v」ってなに？「.coq」だとばっかり思っていたのに。
と、こんな印象でした。まだ腑に落ちない点もありますが、リファレンスマニュアルの第1章（https://coq.inria.fr/distrib/current/refman/Reference-Manual003.html）だけでも、ある程度の察しは付きました。
まず、Coqの言語ってのは1つではないのですよね。
Gallina（ガリーナ）という仕様記述言語がCoqの主要言語のようですが、式（項、term）の構文は、pCic（ピーシック？ predicative Calculus of Inductive Constructions）の構文が使われ、処理系に命令を与えるコマンド言語はVernacular（バーナキュラー）です。タクティク（特別な種類のコマンド）定義にはLtac（エルタック？）という言語もあるらしいです。
Gallina、pCic、Vernacular、Ltacの相互関係はいまいち分かってないのですが、いずれにしても一枚岩の単一言語でないのは確かです。例えばpCicの構文では、ラムダ式を「fun 束縛 => 式」の形で書けます。例： fun (n:nat) => n * 2 。letもlet fix（letrec相当）もあります。pCicの構文は、普通の関数型言語で、特に違和感はないです。
通常「Coqのソースコード」と呼んでいるものは、Vernacularのコマンドスクリプトだったんですね。だから、拡張子が「.v」だったんだ。Vernacularスクリプトは、文（sentence）の並びです。大文字で始まり、ピリオドで終わるのが一文です。Vernacular文は、処理系への命令ですから当然に手続き的／動作（操作）的です。Evalはeval式ではなくて、Eval命令文のコマンド名です。大文字で始まるLetは、pCic構文のletとは別でLet命令、あくまで命令です。
VernacularインタープリタとしてのCoq処理系は、Vernacularスクリプトを一文ずつ順に読んでは内部状態を変更するという、極めて手続き的な動作をします。そのVernacular文のなかにラムダ計算ベースの純関数型言語のpCicの式（項）が含まれるわけです。
[追記]「極めて手続き的」とか言うと語弊があるかも知れません。「メンタルモデルとして、手続き的に動作していると解釈してもいい」くらいが穏当でしょうが、この記事全体が、心理的違和感を取り除くメンタルモデルの話です。[/追記]
僕の先入観として、仕様記述や証明をする言語が「文の順序列」からなる「命令スクリプト」とは思ってなかったので、無理やり宣言的（動作を仮定しない）に解釈しようとして困惑していたわけです。
事例：式の評価と名付け
Evalは「評価せよ」という命令であり、computeは評価にcall-by-value方式を使えというオプションです。だから、Eval compute in 1 + 2. となったわけです。1 + 2 以外の式でも評価は可能ですからやってみます。
Eval compute in fun (n:nat) => n * 2.
これの評価結果（下）は型付きラムダ式そのものですが、自然数（nat）の計算が入るのでなにやら複雑です。
= fun n : nat => (fix mult (n0 m : nat) {struct n0} : nat := match n0 with | 0 => 0 | S p => (fix plus (n1 m0 : nat) {struct n1} : nat := match n1 with | 0 => m0 | S p0 => S (plus p0 m0) end) m (mult p m) end) n 2 : nat -> nat
恒等関数なら単純です。
Eval compute in fun (x:nat) => x. = fun x : nat => x : nat -> nat
関数に引数を渡してみます。ラムダ式のapply、計算処理はβ変換ですね。
Eval compute in (fun (n:nat) => n * 2) 3. = 6 : nat
納得できる結果でしょ。
関数に名前を付けることは、式ではなくて命令（VernacularコマンドDefinition）で行います。処理系が保持している束縛の状態を変えるので、これが命令なのは妥当です。
Definition double: nat->nat := fun (n:nat) => n * 2. double is defined
Eval compute in double 3. = 6 : nat
事例：モノイドの仕様
Vernacularスクリプトは文の並びですが、どうやら多少でも自然言語に近づけようという意図があるようです。Vernacularスクリプトを、本や論文のような体裁で書けるように配慮されています。（とはいえ、Vernacularで論文とかは無理があると思いますがね。）例えばスクリプトを次の形にレイアウトできます。
Section セクション名.
Theorem 定理名: 命題.
Proof.
(* なにやらかにやら *)
Qed.
End セクション名.確かにレイアウトはそれらしいです。しかし、証明の内部はタクティクと呼ばれるコマンドの並びなので、普通の人には意味不明です。Coq処理系で証明（と呼ばれる計算過程）を再現しないと理解不能でしょう。
論理や数学で使われる用語はマチマチですから、Vernacularコマンドにも同義語がたくさん用意されています。例えば、AxiomとParameterとConjectureは同義なのだそうです。DefinitionとExampleも同じとマニュアルに書いてあります -- なんだか変な気もしますがね。
マニュアル第1章の「名前に使える文字」を見ると、なんとユニコード文字が自由に使えると。日本語の名前がOKなので、日本語でモノイドの定義（仕様）を書いてみました。（書いてみただけで、それからどうするか分かっていません。）
[追記]以下のモノイドの定義では、集合の帰納的構成と代数的仕様を混同しています。Inductiveは集合の帰納的構成法を与えるだけのようです。修正はせず、適宜追記を挟みます。[/追記]
Section モノイド. (* モノイドには単位元と積演算がある *) Inductive モノイド : Type := | 単位 : モノイド | 積 : モノイド -> モノイド -> モノイド. (* 単位元を I、積を * で書けるようにする *) Notation I := 単位. Notation "x * y" := (積 x y). Axiom 結合律: forall (x y z:モノイド), (x * y) * z = x * (y * z) . Axiom 左単位律: forall (x :モノイド), I * x = x . Axiom 右単位律: forall (x :モノイド), x * I = x . End モノイド.
教科書通りにモノイドの定義を書けるのは気持ちいいですね。でも、これだけだと、モノイドの要素は単位元しか表現できないです。人間は、この定義から一般的なモノイドを想像できますが、コンピュータ（Coq）は、モノイド仕様を満たす最小の実現（始代数）しか計算できません。
[追記]
CafeOBJだと、モノイドを次のような（modキーワードで始まる）モジュールで定義できます。
mod MONOID {
[M]
op _*_ : M M -> M
op 1 : -> M
vars X Y Z : M
eq X * (Y * Z) = (X * Y) * Z .
eq 1 * X = X .
eq X * 1 = X .
}opで始まる2行が演算や定数を定義する代数的指標（algebraic signature）です。varsで変数を導入して、eqが変数を使った等式的な公理（制約）です。
指標からモノイド要素を表す項の形が決まり、等式的公理から項が等値であることを判断する基準が与えられます。すべてのモノイド項の集合に等値性で同値関係を入れるとモノイド仕様の始代数（モデル圏の始対象）が得られます。
CafeOBJでは、モジュールの意味を始代数だとすることを「タイトセマンティクス」、モデル（対象）を特定しないでモジュールは圏を表すと考えるのを「ルーズセマンティクス」と呼んでいたと思います。僕は、OBJ風のタイト（始代数）セマンティクスとCoqの帰納的定義を混同していました。
コメント欄のmsakaiさんのご指摘によれば、CoqのInductiveは項の集合を帰納的に定義するだけで、Axiomを書いたからといって同値関係が入るわけではないようです。モノイドの積（乗法）は自分で関数で書くとか、法則は公理ではなくて定理として証明するとかが必要なんでしょう、たぶん。
リファレンスマニュアルの19章に型クラスがあるので、型クラスで代数的指標が書けるのかも知れません。（でも、 型クラスは extremely experimental だそうで。）
[/追記]
次のようにすると、単位元以外に1個の生成元を持つモノイドを定義できます。
Section モノイド. (* モノイドには単位元と積演算がある *) Inductive モノイド : Type := | 単位 : モノイド | 積 : モノイド -> モノイド -> モノイド | 生成元 : モノイド . (* 単位元を I、積を * で書けるようにする *) Notation I := 単位. Notation "x * y" := (積 x y). (* 生成元を a と書けるようにする *) Notation a := 生成元. Axiom 結合律: forall (x y z:モノイド), (x * y) * z = x * (y * z) . Axiom 左単位律: forall (x :モノイド), I * x = x . Axiom 右単位律: forall (x :モノイド), x * I = x . End モノイド.
単位（Iと略記）と生成元（aと略記）が、モノイド型（代数的／帰納的な型）のコンストラクタなのですが（積もコンストラクタです）、単位Iのほうは単位律の公理から潰れてしまいます。aは潰れないので、a*a とか a*a*a とかがモノイドの要素（型がモノイドである項）として認識されます。
[追記]この例も先の指摘と同じで、単位元が単位元とはならずに、2つの生成元を持つような帰納的に定義された集合が出来上がります。Iとaと*の記号から組み立てられたwell-formedな項をすべて含み、異なる項はイコールとはみなされません。[/追記]
モノイドの定義のような仕様記述と、背後にある（pCic項を評価する）ラムダ計算のエンジンがどういう関係か？ ということも理解したほうがいいとは思いますが、ナントナークうっすらと分かればVernacularは使える気もします。
まとめ
僕にとって、Coqの入り口での障壁は、Vernacular言語の意味不明さ／違和感でした。中途半端な先入観だったのですが、Cog言語＝ラムダ式ベースの言語だろうと思っていたせいです。Vernacular言語はラムダ式ではなくて、Coqの対話的フロントエンドとオシャベリするためのオマジナイです。自然言語風のシンタックスシュガーをふんだんに振り掛けてあります。
高階型付きラムダ計算の項（term）を記述するpCic構文だけを取り出せば、これはこれで素直で綺麗な構文になっていると思います（好みもあるでしょうが）。
Coqという単一のシステムのなかに複数の言語が入り混じっていることを、知っておいたほうが混乱・誤解・不満を招かないで済むんじゃないかな―、というのが僕の感想です。
