---
title: Coq: Set Primitive Projections と injection タクティックのお話
tags: Coq Coq-8.5
author: mathink
slide: false
---Set Primitive Projections時はRecordとinjectionの相性が悪いよUnset Primitive Projectionsするか、Inductiveで定義してアクセサを別途定義する形にするといいかもね
Set Primitive Projections オプションを設定しているときに
Record Foo (X: Type) :=
make_Foo { foo: X }.とやってレコード Foo を定義したとする。
このとき、たとえば証明モード中に
Heq: make_Foo nat x = make_Foo nat yすなわち
Heq: {| foo := x |} = {| foo := y |}という仮定があったとする(上のように書いても下のように表記される)。
ゴールが f x = f y みたいな形をしていたら、これまでの Coq なら injection Heq とすることで x = y を導入して解決していたところなのだけど、これが出来ない。
(* > injection Heq. *)
(* > ^^^^^^^^^^^^^ *)
(* Error: Pattern-matching expression on an object of inductive type Foo *)
(* has invalid information. *)出来ないので、 foo {| foo := x |} = x という条件を間に挟んで x = y を推論することになる。
補題として {| foo := x |} = {| foo := y |} -> x = y を用意しておけば Heq に apply するだけでいいんだけど、本当なら injection で一纏めに出来ていたことを、データ型に分けて補題を用意するのはなんだか面倒である。
この状況への対策としては、以下の選択肢がある。
- 我慢して補題を作っておく
Fooを定義するときにUnset Primitive ProjectionsしておくInductive Foo (X: Type) := make_Foo: X -> Foo X.とやって、射影函数fooはあとで定義する
個人的には、アクセサを用意したいフィールドの数に応じて 2. か 3. を使い分けるのがよいのかな、と思っている。
アクセサを作っておきたいフィールド数が多い場合、 Record 使うのが楽なので、そうしたい。
そしてアクセサがあるということは、全体の等価性から対応する要素の等価性を使いたい場合もそれなりにあると思われるので、データ型に応じた補題を用意するよりは毎回 injection できる方がよい。
公式ドキュメントを読む限り、 Set Primitive Projections しておくと項のサイズが小さくなるらしいので速度的なメリットなどがあるんだろうけど、おそらく、複雑でない(規模が小さいとか、依存が少ないとかそういう感じの)レコード型については、あまり気にならないレベルなんじゃないかと思う。
また、 3. も推す理由は、 injection タクティックは「inductive な型のコンストラクタが埋め込みになっているという事実を元にしたもの」と謳われている(参考)ので、それならば injection を使う対象であるという意味も込めて、 Inductive で定義するとよいのではないかと思ったからである。
「じゃぁ make_Foo は埋め込みじゃないんかい」と言われると「埋め込みだと思う」が私の意見なのでなんとも言えない気持ちではあるんですが、現状、そういう仕組みになってしまっているということです。
Unset Primitive Projections してあるとき限定ですが、
Inductive Foo (X: Type) :=
| make_Foo { foo: X }.って定義すると
Foo is defined
Foo_rect is defined
Foo_ind is defined
Foo_rec is definedってなって普通に帰納型 Foo が定義されるんだけど、
Inductive Foo (X: Type) :=
make_Foo { foo: X }.ってやると(| がない)、
Foo is defined
Foo_rect is defined
Foo_ind is defined
Foo_rec is defined
foo is definedってなってアクセサ foo も一緒に定義してくれる。
見方を変えれば、帰納原理も生成する Record になっている。
ちなみに、
Inductive Foo (X: Type) :=
make_Foo ( foo: X ).ってした場合(括弧が丸括弧)は最初の例と同じ結果になります。
なお、 Set Primitive Projections してるときは
Inductive Foo (X: Type) :=
make_Foo { foo: X }.を試みると次のようなエラーが返ってきて型(というか多分帰納原理)を定義できません。
(* > Inductive Foo (X: Type) := make_Foo { foo: X }. *)
(* > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
(* Error: *)
(* In environment *)
(* X : Type *)
(* P : Foo X -> Type *)
(* f : forall foo : X, P (make_Foo X foo) *)
(* f0 : Foo X *)
(* The term "f (let (foo) := f0 in foo)" has type *)
(* "P (make_Foo X (let (foo) := f0 in foo))" while it is expected to have type *)
(* "P f0". *)なんというか、一連の挙動のどこかにバグが潜んでいるような気がしなくもない。