[Coq] Coq'Art Chap.2

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)
   :