Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions の Chapter 2 です。
この章では概ね次の４つが語られているように見えます。
(1) Coq のコマンド
下記の様なコマンドがあります。
★
Require Import library.ライブラリをロードして environment に追加する。
libraryとしては、
Arith, ZArith, Boolなどがある。
★
Open Scope scope名.Scope は notation を interprete する規則。例えば
Z_scopeを指定すると各種演算子記号が Z の演算のものと判断される。
★
Print Scope scope名.Scopeで定義された notation の一覧を得る。
★
Check term.termのtypeを表示させる。
★
Parameter t:A.t:Aを environment に追加する。environmentはglobalなもの。
★
Section id. ...
End id.localなblockを作る。
★
Variable t:A.t:Aを context に追加する。contextはlocal。なので、
Section...Endの範囲内で有効。
(2) Inference Rules
様々な推論規則があります。
(x,A)∈E∪Γ
Var ------------ x:identifier
E,Γ |- x:A
E,Γ|- e_1:A->B E,Γ|- e_2:A
App ------------------------------ 関数適用
E,Γ|- e_1 e_2:B
E,Γ|- e:A_1 -> A_2 -> ... -> A_n -> B E,Γ|- e_i:A_i (i=1,...,n)
App* -------------------------------------------------------------------
E,Γ|- e e_1 ... e_n:B
E,Γ|- t_1:A E,Γ::(v:=t_1) |- t_2:B
Lam -------------------------------------- λ式
E,Γ|- fun v:A => e:A->B
E,Γ|- t_1:A E,Γ::(v:=t_1) |- t_2:B
Let-in -------------------------------------- let
E,Γ|- let v:=t_1 in t_2:B
E,Γ|- A:Set E,Γ|- B:Set
Prod-Set --------------------------
E,Γ|- A->B:Set
E,Γ|- t:A E,Γ|- A ≦_{beta delta iota zeta} B
Conv --------------------------
E,Γ|- t:B
(3) Eval
★cvb : call-by-value (cbvでなくlazyで遅延評価)
★delta-reduction : t ==> t{v/t'}。tのidentifier vをその定義t'で置換。
★beta-reduction : (fun v:T => e_1) e2 ==> e_1{v/e_2}。λ式を簡約。
★zeta-reduction : let v := e_1 in e_2 ==> e_2{v/e_1}。letを簡約。
★iota-reduction : 帰納的な処理で詳しくはChap.6でということで後回し。nat,Zは帰納的な定義なので計算する時はiota-reductionが必須。
★compute = cvb iota beta zeta delta の略
★
Eval compute in (....). :
...を実際に計算する。
Reductionに関する性質
- strong normalization : reductionはfinite
- confluence : t |> t_1, t |> t_2 ならば、あるt_3があって、t_1 |> t_3 かつ t_2 |> t_3。
(4) Universe
typeもtermだとすると、typeのtypeがあるはず。それをsortという。
CoqではSetというデフォルトのsortが定義されている。
更にその上の無限の階層まで考えるようだが、CoqではType(i)は全部ひっくるめてTypeにしてしまう様子。
Level 0 : 具体的な項とか関数。O, S, trinomial,...
Level 1 : データの型。nat, nat->nat, ...
Level 2 : ソート。Set
Level 3 : Type(0)
:
