---
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". *)
なんというか、一連の挙動のどこかにバグが潜んでいるような気がしなくもない。