Coq: Vernacular コマンド備忘録

  • 11
    いいね
  • 2
    コメント
この記事は最終更新日から1年以上が経過しています。

おまじないのように使っているといつの間にか意味を忘れてしまうので、記録していく。

  • 随時更新されるはずである。
  • 分類は適当。
  • 量が増えるにつれて自然と整っていくことが期待されている。
  • 今のところ引数関連の話題が多い。
  • 気になるところ、指摘などなどコメントは歓迎です。

TODO

Structure とか Class とか。定義する系。

Coercion: 暗黙的な型の変換

基本的な使い方

二つの型 A, B と変換函数 f: A -> B があるとする。このとき

Coercion f: A >-> B.

というコマンドを実行すると、 B 型の値が求められている場所に A 型の値を与えた場合、暗黙的に f が適用されるようになる。

例えば、

Definition nat_to_bool (n: nat): bool :=
  match n with
    | O => false
    | _ => true
  end.

という nat から bool への変換函数を用意して

Coercion nat_to_bool: nat >-> bool.

とすると、

Check (andb 3 true).

のという式が使えるようになる。この andb 3 true は、実際には andb (nat_to_bool 3) true として処理される。

coercion には型強制という訳が充てられているみたいだけど、 Coq の場合、 implicit に変換函数を適用してみるという感じなので、 強制 ってほどでもないなぁと思わなくもない。

Set Printing Coercions.

変換函数の暗黙の適用は、基本的に Coq の出力上には現れない。
コードに書かれていないのだから、表示もされてない方が自然だ。

ただまぁ、変換函数についての性質を使うときとか、やっぱり変換函数が見えていたほうが良い時もある。
そんなときは事前に Set Printing Coercions. を実行しておくと良い。

解除は Unset Printing Coercions. で。
coercion を多用しているときに表示すると鬱陶しくてたまらない。

Set Printing Coercion hoge. で特定の coercion のみに限定したりもできるみたいだけど、いっぱい使ってる時は名前なんか覚えてないので、案外使われない(個人の感想です)。

細かい話

  • TODO: 具体的コード

先ほどの例は型が Set のデータ型間の変換だった。
場合によっては変換先の型が Set でない場合もある。

変換函数の final type の型が Type である場合や函数型である場合、
Coercion コマンドの >-> の右側にはそれぞれ SortclassFunclass と書く。

「型とその上の演算」をひとまとめにした型を作った時、 Sortclass への coercion は便利。

Coercion コマンドで登録されたものたちは Print Graph. コマンドで確認できる。
見てみるとわかるのだけど、複数の変換函数を合成することで新たな変換函数による coercion も成立している。

変換函数を辺としたグラフが構築されているわけだけれど、coercion は、与えられた値の型から求められている型へのパスが存在するとき、その経路にしたがって順次変換函数を適用することで行われている。

となると、複数の経路があったら? と思うわけだけど、Coercion コマンドを実行した時点で「ambiguous な path だよ」と言われてそのコマンドによって生じるはずだった coercion は無視されるので、曖昧性がもたらす問題は起きない。

複雑な話

上記の例では変換函数の型が A -> B という「直接的な」ものだったけれど、 corecion に使える函数はこれよりももうちょっと複雑でも良い。

Record 系: 複数のデータから構成される型を作る

ひとまず Inductive コマンドの基本的な使い方は知っている前提で。

Record

Record は複数のフィールドを持つデータ型を定義するコマンドである。

Record Position := { pos_x: nat; pos_y: nat }.

とすることで2つの nat 型の値を持つデータ型 Position が定義できる。
Record で定義されたデータ型を単にレコードと呼ぶ(ことが多い気がする)。

Position 型の値を構成するには

Definition origin: Position :=
  {|
    pos_x := 0;
    pos_y := 0
   |}.

とすればよい。パラメータを与える順番は前後しても大丈夫。

また、フィールド名はフィールドへのアクセス函数の名前となっている。例えば

Compute pos_x origin.

の結果は 0 である。

RecordInductive

レコードを定義してみればわかるが、型を定義すると、型以外にも同時にいろいろなものが定義されている。

上記の Position であれば、

  • Position_rect
  • Position_ind
  • Position_rec
  • Build_Position
  • pos_x
  • pos_y

といった面々が定義される。下2つはフィールドへのアクセサであり、上3つは帰納原理である。

では Build_Position は何なのか。
いやいや、そもそも何故帰納原理が生成されているのか。
これらに対する答えはまとめて与えられる。

それは、Record によるレコード型の定義は

  • 単一コンストラクタの帰納型を定義し
  • コンストラクタの各パラメータを取り出す函数を定義する

ための糖衣構文に過ぎない、というものである。

具体的に言えば、さきほどの Position の定義は

Inductive Position :=
| Build_Position (pos_x: nat)(pos_y: nat).

Definition pos_x (p: Position): nat :=
  match p with
    | Build_Position x y => x
  end.

Definition pos_y (p: Position): nat :=
  match p with
    | Build_Position x y => y
  end.

という一連のコマンドと対応している。
帰納原理は最初の Inductive コマンドによって生じたものであり、 Build_Position はコンストラクタのことである。

なお、 Build_Position についてはレコードの定義時に名前を自分でつけることもできる。
make_Pos といった名前にしたければ

Record Position := make_Pos { pos_x: nat; pos_y: nat }.

とすればよい。

RecordVariant

現在、 Coq は 8.5 の beta をリリースしている。
この記事は 8.4pl5 を対象としているので取り上げる必要性はないのだけれど、上記の項目、 RecordInductive の関係に変化があったので簡単に記しておくことにする。

8.5 から Variant というコマンドが新たに追加された。
これは、再帰構造を許さない Inductive と思えば良い。
普通に variant type を定義するコマンドと思っても良い。

とにかく再帰構造を許さないので、帰納原理を生成する必要はなく、実際に生成されない。
そして 8.5 からの RecordInductive ではなく Variant をベースにしている(と思われる)ので、同様に ..._rect のような帰納原理を生成しなくなった。

Record は元々フィールドに自身を利用できなかったので、この変更の影響はほぼないと思われる。

もしも Record が自動生成する帰納原理を使っているのであれば、帰納原理の存在を明示する意味でも Inductive に書き換えましょう(今までも Record の代わりに Inductive って書いても OK なことをさっき知った)。

Structure

StructureRecord全く同じ 。単なるシノニム。
え、じゃぁ説明する必要なくない?という感じなのですが、幾つか Structure 関連で良い機能があるので記します。
Record についても全く同じ話が成り立つんですが、DefinitionTheorem のように、どういうつもりで定義しているのかを読むときに区別できるので、その辺り意識しつつ。

StructureCoercion

Structure で型を定義するとき、その型からフィールドへの coercion を設定できる。
型とその上の二項演算子を纏めた Magma 型を定義するとしよう。

Structure Magma :=
  {
    carrier:> Type;
    binop: carrier -> carrier -> carrier
  }.

このとき、フィールドの型の前が :> という記号になっており、こうすると定義時に

Coercion carrier: Magma >-> Sortclass

という coercion を設定するのと同じ効果が得られる。

私はこういう「型+何か」を纏めた型について、よく :> を使う。

Definition hoge (m: Magma)(x: m) := ...

みたいな書き方ができるのでとても便利。
数学でいう $M = \langle M, \bullet\rangle$ みたいな記法に近い感覚。

この :> は複数のフィールドに設定できるので、曖昧性がなければひとつの記号を複数の目的に使いまわす、みたいなことも可能。

実際に自分が使っている例だと

Structure Category :=
  {
    obj:> Type;
    hom:> obj -> obj -> Type;
    ...
  }.

という具合に圏の型から「対象型」と「ホム型」への coercion を設定して

forall (C: Category)(X Y: C)(f: C X Y), ...

みたいな書き方ができるようにしている。
objCategory から Sortclass への coercion , homCategory から Funclass への coercion なので曖昧さがない。

Canonical Structure

TODO: 中身

StructureRecord をどう使い分けるか。

好み。

といってもあれなので、自分なりの使い分け方を書いておきます。
どんな感じで使い分けているかというと、

  • Record は複数のデータ型が集まって一つの型になっており、データ型間に優劣があまりないとき。
  • Structure は主役になるようなデータ型とそれに付随するものを纏めたいとき。

という具合でしょうか。優劣って何よ?とか思うかもしれませんが、なんとなくです。
一応もうちょっとだけ詳しく説明すると、基本的に Record を使うときは本当に只のデータ型の寄せ集めって感じの型を定義するときだけで、フィールド間に依存関係があったり満たして欲しい規則があるときは Structure を使うことが多いです。
後者は「構造」を持っている感がありますよね?ありません?

StructureRecord と全く同一なわけですが、逆に何らかのポリシーに則って使い分けることで、書いている人の気持ち的なものを反映できるので、読むときの助けになったりするんじゃないかなぁと思っています。

Class

Record を使っているけど、 Record のように使うものではない、そんなもの。

  • 基本は
  • フィールド

TODO:続き

StructureClass の違い

Structure Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> carrier
  }.
Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> carrier
  }.

Implicit 系: 引数の implicitness を制御する

Set Implicit Arguments.

これを唱えると、何かを定義した時、引数の implicitness が自動設定される。
例えば Set Implicit Arguments. を実行したあとの状態で

Definition Apply (X Y: Type)(f: X -> Y)(x: X) := f x.

という函数を定義すると、 Apply の引数 X,Y は implicit な引数になる。
引数が implicit かどうかは About コマンドを使えば見れる。

また、大抵の場合 Set Implicit Arguments. した後に Unset Strict Implicit. を続ける。
そうしない場合には Coq によって implicit かどうかを判定される引数が (strict implict な引数) + (non strict implicit な引数の一部) となっているのが、これを使うと判定の対象が可能な限り広くなるらしい。
多分、 implicit かどうかの判定を行う対象が広がるということでいいはず。

なんでデフォルトでそうなってないのかなぁと思うんだけど、 historical reason がどうのうこうのという記述を見つけたので、とりあえず使っとけば良い感じである。

詳しい挙動なり言葉遣いはrefman を見よう。

Set Contextual Implicit.

文字通り、その引数、文脈からわかるでしょ?という時にちゃんと動いてくれるようにするコマンド。
一番わかり易い用途は nil

list に対して

Fixpoint rep (n: nat){A}(a: A): list A :=
  match n with
    | O => nil
    | S n' => cons a (rep n' a)
  end.

みたいな函数が定義できるのだけど、普通に

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

という定義を与えるだけだと、実は rep の定義が通らない。
nilA が implicit な引数になっていないので、nil A と書かなければならない。

Coq の標準ライブラリでは Arguments コマンドを使って nilA を implicit に設定しているけど、
Set Contextual Implicit. をしてから定義をすれば Arguments コマンドはいらない。

Arguments コマンドを使う場合、コンストラクタ毎に設定しなければならないので、コンストラクタの数が多いデータ型については事前にこのコマンドを使うことを検討してもよいかもしれない。

Set Reversible Pattern Implicit.

後ろにある引数から前にある引数が推論できるよって時にもうまく取り計らってくれるようにするコマンド。らしい。
具体例がパッと出てこないのだけど、過去の記憶を思い返すとこれでいい感じになるような例があったような気がしなくもない......

とりあえず、今は Contextual と一緒におまじないのごとくスクリプトの最初に書いている。
ないよりあったほうが良いの精神。

Arguments コマンド使い方集

気づいたら Arguments コマンドが万能になってるので使い方をメモる。

引数の implicitness の設定

特に Set Implicit Arguments. とかしていないと仮定して

Definition comp (X Y Z: Type)(f: X -> Y)(g: Y -> Z): X -> Z :=
  fun (x: X) => g (f x).

みたいな函数を定義したとする。
定義した時点では comp に implicit な引数はない。

いざ使うときには X とかいちいち書きたくないしワイルドカード挟むのも億劫だし、っつうかわかるでしょ、ということで

Arguments comp {X Y Z}(f g x).

とすると、波括弧で囲まれた引数は implicit になる。このとき引数名は函数定義のそれと一致させないといけない。
函数定義で名前が与えられていなければ、そこは好きに名前を設定可能。

また、final type の直前まで設定を要求されるので g のあとの x も必要。
この名前は地味に色んな所で使われるので、それっぽくつけるとよい。

ちなみに、丸括弧は explicit であると指定する ものではない
特に設定を変えないという意味。
今のところ、一度 implicit に設定したものを explicit に戻す方法は知らなかったが、最近見つけた

引数の implicitness の解除。

Arguments hoge: clear implicits.

とすると、 hoge の引数の implicitness が解除される。
引数全部一括でリセットなので、一部の引数だけ implicitness を解除したいって場合はこの後に改めて設定しよう。

引数の名前変え

上の続きみたいなもんなのだけど、引数の名前は証明モードの時とかで地味に出てくるので、それらしいものにしておきたい。
その引数名は基本的に定義時のそれを引きずるのだけど、あとから変更も可能。
具体的には

Arguments comp {A B C}(f g x): rename.

という風にコマンドの末尾に : rename とつけてあげれば良い。
今回、元々 X,Y,Z という名前だった引数を A,B,C という名前に変更した。
もちろん、一文字である必要はない。

simpl 時の unfold 制御。

Definition とか使うと基本的に unfold しない限り定義が展開されないのだけど、しかしなんでもかんでも unfold するのは面倒。

Arguments コマンドを使うと、どの引数まで与えられたら simpl 時に定義を展開するかを制御できる。
またしても comp を例に使うが、

Arguments comp X Y Z f g / x.

というように引数列の間に / を挿入すると、その直前の引数まで与えられたら simpl 時に定義が展開されるようになる。
この場合なら comp f はそのままだけど comp f gfun x => g (f x) に展開されることになる。

ちょっと展開早いわーっていうなら

Arguments comp X Y Z f g x /.

とするとよい。一応、本来なら comp f g x でも展開されないので、引数リストの末尾であっても / は意味を持つ。

地味に便利。

捕捉、あるいはフォロー

Definition と引数の implicitness

引数の implicitness を制御するのはどうしたって別のコマンドを使わなきゃならんの?
という疑問に対する否定的結論を以下に記す。

またもや comp を例にとる。

Definition comp {X Y Z: Type}(f: X -> Y)(g: Y -> Z): X -> Z :=
  fun (x: X) => g (f x).

とすれば

Arguments comp {X Y Z}(f g x).

としたのと同じ効果を定義時に得られる。便利。

注意すべきは、うっかり f とかを implicit にしないこと。
この場合、 Arguments コマンドを Coq は受け付けてくれちゃうので、そのあとに comp h とかやってしまうと、引数 f が何なのかわかりません!と文句を言われる。

むやみに implicit にしないようにしよう。

Arguments による implicitness 制御の出番

Coq のコマンドには、実行すると付随して色んな函数が自動的に生成されるというものが多い。
Inductive とか Structure とか Class とか Scheme とか、とにかく色いろある。
フィールドへのアクセス函数やら、帰納原理やらがその例。

自動的に生成される以上、 Definition のように、これらの生成時に引数の implicitness を個別に制御することはできない。

コマンドの機能として、生成する函数の引数の implicitness を設定してくれることもあるし(例えば Class)、Set hoge とかしておけばそれに合わせた設定になったりもする。

しかし、あくまで自動的に設定される implicitness なので、使い方次第ではちょちょいと弄りたい場合も出てくる。
そういう時はやっぱり Arguments コマンドで implicitness を制御することになる。