Coq: Set Primitive Projections と injection タクティックのお話

  • 0
    いいね
  • 0
    コメント

    まとめ

    • Set Primitive Projections 時は Recordinjection の相性が悪いよ
    • 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 を用意しておけば Heqapply するだけでいいんだけど、本当なら injection で一纏めに出来ていたことを、データ型に分けて補題を用意するのはなんだか面倒である。

    対策

    この状況への対策としては、以下の選択肢がある。

    1. 我慢して補題を作っておく
    2. Foo を定義するときに Unset Primitive Projections しておく
    3. 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". *)
    

    一言

    なんというか、一連の挙動のどこかにバグが潜んでいるような気がしなくもない。

    この投稿は Theorem Prover Advent Calendar 201613日目の記事です。