カーネル

Lean の信頼の中心はカーネルです． カーネルは，エラボレータが作った定義や証明項が，Lean のコア型理論の規則に従っているかを検査します．

重要なのは，tactic やエラボレータは大きく複雑であっても，最終的な証明項はカーネルで検査されるという点です． したがって，通常の tactic にバグがあっても，間違った証明項を作ればカーネルで拒否されます．

逆に言うと，カーネルは Lean のすべての機能を直接知っているわけではありません． Reference では，カーネルはコア型理論の type checker であり，構文上の termination checker や unification は含まない，と説明されています． 再帰定義や pattern matching は，エラボレータ側で再帰子，整礎再帰，partial fixpoint などを使う形へ変換されます． 通常の数学的証明で使う定理は最終的にこの検査を通りますが，partial や unsafe を含むプログラム実行の話は， 論理的な証明項の検査とは分けて理解する必要があります．

ただし，カーネルが検査するのは「形式化された命題が証明されたか」です． その命題が人間の意図した数学的主張を正しく表しているか，どの公理や imported theorem に依存しているかは別の確認事項です．

#check Eq.refl
#check Nat.rec
#check False

theorem fooKernelExample (n : Nat) : n = n :=
  Eq.refl n

#print fooDouble
#print fooKernelExample
#print axioms fooKernelExample
#check Lean.Declaration
#check Lean.ConstantInfo
#check Lean.ConstantInfo.defnInfo
#check Lean.ConstantInfo.thmInfo
#check Lean.DefinitionVal
#check Lean.TheoremVal
#check Lean.Environment.find?
#check Lean.addDecl
#check Lean.addAndCompile

Eq.refl n は等式の反射律を表す証明項です． by rfl のような tactic は，このような証明項を作るための便利な表面構文だと考えられます．

#print fooDouble や #print fooKernelExample は，環境に登録された名前の型や本体を pretty printer で表示します． これは .lean ファイルに書いた文字列そのものではなく，エラボレーションとカーネル検査を通って環境に入った後の定義・定理を表示している，と考えるとよいです． #print axioms fooKernelExample は，その定理がどの公理に依存しているかを調べるコマンドです．

内部的には，環境に追加される宣言は Declaration や ConstantInfo として表されます． たとえば定義は ConstantInfo.defnInfo，定理は ConstantInfo.thmInfo のような形で区別されます． addDecl や addAndCompile は，メタプログラム側から新しい宣言を追加するための関数であり，通常の def や theorem の裏側で起こる処理の雰囲気を知る手がかりになります．