新しい型を追加する

前回までの言語には関数型と型の型しか型がなかったので、新しい型を追加します。型を追加するには以下の情報が必要です。

型のコンストラクタを表す項
値のコンストラクタを表す項
値のデストラクタを表す項
計算規則

例えば、リスト型を追加したい場合はそれぞれ以下のようになります。

型コンストラクタ list : forall A : Type, Type
値コンストラクタ
- nil : forall A : Type, list a
- cons : forall A : Type, a -> list A -> list A
デストラクタ

list_rec
     : forall (A : Type) (P : list A -> Set),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (cons a l)) ->
       forall l : list A, P l

計算規則
- list_rec A P Hnil Hcons nil ===> Hnil
- list_rec A P Hnil Hcons (cons a l) ===> Hcons (list_rec A P Hnil Hcons l) a l

Coq ではこれらをまとめて

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A

と書くだけで一度に全部やってくれます。

ここではリスト型を追加してもたいして面白くないので、eq型を追加します。

eq型

Coqでは以下のように定義されています。

Inductive eq (A : Type) (x : A) : A -> Prop :=
  eq_refl : eq A x x

これを追加するためには、リストと同じように必要な項の一覧と計算規則を作ります。われわれはPropを作っていないので、適当な i を選んで Univ i を使います。さらに、Coqでは x = y の両辺は対称ではありません。今回はもっと対称的な形の、

Inductive eq' (A : Type) : A -> A -> Type :=
  eq_refl' : forall x, eq' A x x

を使います。使い勝手ではCoqの定義のほうがはるかに簡単なのですが、やっぱり対称なほうが綺麗なのでこっちにします。

というわけで、eq型に必要なものは

型コンストラクタ eq : forall A : Univ i, A -> A -> Univ i
値コンストラクタ eq_refl : forall (A : Univ i) (x : A), eq A x x
デストラクタ

eq_rec
     : forall (A :  Univ i) (P : forall x y : A, eq A x y -> Type),
       (forall z : A, P z z (eq_refl A z)) ->
       forall (x y : A) (p : eq A x y),
       P x y p

計算規則 eq_rec A P H z z (eq_refl A z) ===> H z

になります。

なお、元ネタは http://homotopytypetheory.org/book/ の付録にあります。

項の定義に追加

色々とやり方はありそうですが、今回はアンチョクに必要な引数を全部持っている形でエンコードします。

data Term = Var String
         | ...
         | Eq Type Term Term
         | Refl Type Term
         | EqRec Type Term Term Term Term Term

課題: typeofを改造してこれらの項に対応させて見ましょう。規則は上に書いたとおりです。

課題: reduceFullを改造して計算規則を追加しましょう。

時間なくて手抜きになってしまいましたが、
次回はやっとタクティックの実装を始めます。たぶん年末に書きます。

Write Yourself a Theorem Prover in 48 Hours (その3)

新しい型を追加する

eq型

項の定義に追加