Coqの新機能、Primitive Projectionについて

Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。

• Universe Polymorphism
• Primitive Projection

Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをしたい場合(Homotopy n-typeやCategoryなどを定義したい場合)に宇宙ごとに異なる定義をする必要がなくなるという利点があります。

というのはさておき、この記事ではPrimitive Projectionを紹介します。

Primitive Projectionは、レコード型を定義したときにできる射影関数がプリミティブになるという機能です。Coqの内部で、普通の関数とは異なる特別な値として扱われるようです。

利点は次の2点のようです。

• 型検査の効率Up
• η変換ができる

ここでは後者の点についてサンプルコードを示します。

(* 従来のレコード型 *)
Record Foo := Build_Foo {
  foo : unit
}.

Set Primitive Projections.

(* Primitive Projectionを有効にしたレコード型 (Primitive Recordと呼ぶ) *)
Record Bar := Build_Bar {
  bar : unit
}.

(* 従来のレコード型では、η変換はできない *)
Goal forall f : Foo, f = Build_Foo (foo f).
Proof.
  Fail reflexivity.
Abort.

(* Primitive Projectionを有効にしたレコード型では、η変換ができる *)
Goal forall b : Bar, b = Build_Bar (bar b).
Proof.
  reflexivity.
Qed.


(* どうやら、射影関数を自分で定義しても、同じ結果になるらしい？ *)

Definition foo2(f:Foo) : unit :=
  let (foo2) := f in foo2.

Goal forall f : Foo, f = Build_Foo (foo2 f).
Proof.
  Fail reflexivity.
Abort.

Definition bar2(b:Bar) : unit :=
  let (bar2) := b in bar2.

Goal forall b : Bar, b = Build_Bar (bar2 b).
Proof.
  reflexivity.
Qed.

補足

そもそも、関数に関するη変換が入ったのが最近 (Coq 8.4以降) です。サンプルコードを示します。

Goal (fun (f:nat->nat) (n:nat) => f n) = (fun (f:nat->nat) => f).
Proof.
  reflexivity.
Qed.

面倒なので確かめていませんが、このような証明は以前は成立しなかったはずです。