Coq の コアライブラリ(Prelude)を見て数学が分かった気になる

集合はどうも、数学の基礎にあたるようです。でも、集合を把握すする前に「定義、公理、命題、定理とは何か？」を把握すると良いです。この辺の話はCoqの構文を覚えることでプログラミング言語を覚えるように覚えることができます。

http://homepage3.nifty.com/rikei-index01/biseki/bisekiteiri8.html

集合論は型理論の基礎的な知識だそうですが、集合の前にある前提として論理とか、自然数の足し算やかけ算等があるようです。Coqで一からどう形作られているかを見れば、その関係が分かるはずです。

http://coq.inria.fr/stdlib/index.html

Init: The core library (automatically loaded when starting Coq)
Notations Datatypes Logic Logic_Type Peano Specif Tactics Wf (Prelude)

Coqで集合のライブラリを遡るとCoqのコアライブラリに行き着きます。
Coqが開始すると自動的にロードされるライブラリがコアライブラリであり、Preludeにまとめて書いてあります。

http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Prelude.html

Library Coq.Init.Prelude

Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
Add Search Blacklist "_admitted" "_subproof" "Private_".

Notations で記法(演算子の定義)がされていて、
Logicで論理的な定義、
Datatypesでデータの型、
Specifが基本仕様、
Peanoで、ペアノ数、
Wfで整礎関係 Well-founded relation や整礎帰納法 Well-founded inductionについて
Tacticsでタクティクが定義されていて、
検索から_admitted, _subproof Private_は検索されないように定義されています。
Ligic_typeはPreludeに書かれてませんが、最初に読み込まれるそうで、論理の型ってことでしょう。

Notationsを見て見ます。

http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Notations.html

Reserved Notation "x <-> y" (at level 95, no associativity).
Reserved Notation "x /\ y" (at level 80, right associativity).
Reserved Notation "x \/ y" (at level 85, right associativity).
Reserved Notation "~ x" (at level 75, right associativity).
:

ずらずらと、演算子と、優先順位、結合法則が書かれてます。
基本的な演算子はここで全て定義されている訳です。

Logicを次に開いてみましょう。
http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html

(* Propositional connectives *)
(* 命題の結合 *)

(* True is the always true proposition *)
(* Trueは常に真の命題 *)
Inductive True : Prop :=
  I : True.

(* False is the always false proposition *)
(* Falseは常に偽の命題 *)
Inductive False : Prop :=.

(* not A, written ~A, is the negation of A *)
(* Aでなければ、Aならfalse *)
Definition not (A:Prop) := A -> False.

Notation "~ x" := (not x) : type_scope.
(* ~ x は not *)

Hint Unfold not: core.
(* ヒント 逆展開 not: core *)

(* conjection 論理積 and型 *)

(* 定義 and A B : A ⇒ B ⇒ A ⋀ B *)
Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B
:

Coq立ち上げ時にはこのような沢山の定義や定理等が読み込まれます。
このような数学的な土台の上に、集合(Coq.Sets.*)が定義されているわけです。
全てを覚えるのは難しいですが、こういう構造だと理解したのであれば、それで十分ではないかと思います。後は、必要になったら見ればいいのです。

Javaだって、全てのAPIを覚えないですよね。
基本的な構文を覚えて、よく使うライブラリを覚えれば、あとは必要なときにライブラリを探せばいいのと一緒です。

そして、TAPLの2章についても、必要になったら見れば良いライブラリという認識をしておけば十分ではないかと思います。

という悟ったような状態になったのが今日の収穫です。

全てを理解した訳ではないし、全部を覚える事は出来ないけど、論理を決めて、論理で使う型を決めて、基本仕様を決めて、自然数を決めて、関係とかを決めて、タクティクを決めて、論理の型を決めてから、集合や関係、関数、順序集合、列、帰納法等の上に、型理論を構築するんだ、という事が分かったので、ずっと、気が楽になりました。