Setoid の Proper な Map を作る。: Theorem Prover Advent Calendar 2014 Day 15

1 この記事は、

  1. Theorem Prover Advent Calendar 2014 の 15 日目の記事です。
  2. Setoid の間の「写像」である Map を定義します。
  3. Morphisms モジュールの Proper を同値関係の保存の記述に用いています。
  4. Proper クラスについても、少しだけ説明をしています。
  5. 載っているコードはそのまま coqc 出来ます。コードを抽出したものは こちら

1.1 参考文献など

A Gentle Introduction to Type Classes and Relations in Coq.
Setoid の時と同じく。この文書はとてもよいものです。

2 準備とか

前回Setoid を定義しました。 Gist には setoid_advent_2014.v というファイル名で上げたので、 coqc した上でインポートしておきます。

Set Implicit Arguments.
Unset Strict Implicit.

Require Import setoid_advent_2014.

今回インポートしているのは前回の記事にあたる coq_setoid のみです。 Setoid とか Morphisms とかは coq_setoid でエクスポートすることにしましたので、 coq_setoid のみをインポートすれば事足ります。

3 Map 型の定義

型の間の「写像」は関数です。 nat 型のコンストラクタ S は、コンストラクタであると同時に 型 nat から型 nat への関数だと見做すことが可能です。

一般に「関数」は二項関係の特殊な場合として定義されることが多いようです。例えば、集合 \(A,B\) に対して関係 \(f \in A\times B\) が関数であるとは \[ \forall a \in A.\; \exists! b \in B.\; (a,b)\in f \] が成り立つことである、と定義されたりします。

Setoid は型と同値関係の組なので、 Setoid の間の写像は少なくとも関数であるとしてよいでしょう。 そして、その関数が Setoid の間の写像として well-defined であるための条件は、「同値関係の保存」となります。

ということで、 Setoid から Setoid への写像を次のように定義します。

Structure Map (X Y: Setoid) :=
  {
    map_body:> X -> Y;

    prf_Map:> Proper ((==) ==> (==)) map_body
  }.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'").

フィールド map_body の型は X -> Y となっていますが、 coercion が効いているため、実際の型は carrier X -> carrier Y となります。

map_body についても coercion を施しているので、例えば f: Map X Yx: X については f x という形の適用が可能になります。

ここで気になるのは Map の定義中にある Proper が何者なのかということと、 なんかよくわからん Notation コマンドでしょうか。

4 Proper な写像

Map の定義中に表われている Proper 、 これは Morphisms モジュールで定義されている型クラスです。 流れから、これが「同値関係の保存」を意味する命題の記述に使われていることは推測できると思います。 しかし Proper の定義を覗いてみても

Proper = 
fun (A : Type) (R : relation A) (m : A) => R m m
     : forall A : Type, relation A -> A -> Prop

Argument A is implicit and maximally inserted
Argument scopes are [type_scope signature_scope _]

ふむ?あまり情報が手に入りませんね。 実は、重要な役割を果たすのは Proper の第二引数に与えられる関係です。

4.1 Proper のイミ

Map の定義では Notation が使われているので Locate コマンドで中身を見てみると

Notation            Scope     
" R ==> R' " := respectful R R'
                      : signature_scope

ということで、実体である respectful の定義を Print すると

respectful = 
fun (A B : Type) (R : relation A) (R' : relation B) (f g : A -> B) =>
forall x y : A, R x y -> R' (f x) (g y)
     : forall A B : Type, relation A -> relation B -> relation (A -> B)

Arguments A, B are implicit and maximally inserted
Argument scopes are [type_scope type_scope signature_scope signature_scope _
  _]

という定義であることがわかります。すると、定義を展開していけば

\begin{eqnarray*} & &{\tt Proper\ ((==)\ ==>\ (==))\ f} \\ &\Leftrightarrow& {\tt (==)\ ==>\ (==)\ f\ f} \\ &\Leftrightarrow& {\tt \forall\ x\ y,\ x==y\ ->\ f\ x==f\ y} \end{eqnarray*}

となり、確かに prf_Map の型が「同値関係の保存」を意味するものであることがわかります。

4.2 Proper クラスと rewrite タクティク

恥ずかしながら、私が Proper を使う用途は今のところ同値関係の保存についてのみなので、 Proper クラスそのものの意味を説明することはできません。

しかし逆に言うと、同値関係の保存という点だけを見ても、 Proper クラスには利用するだけの価値が備わっているということでもあります。

私自身がとっても気に入っており、そもそも Proper を使うことになった理由は 同値関係の保存性を Proper で記述しそれを証明すると、その同値関係を基にして rewrite タクティクを使える というものです。

参考文献に挙げた A Gentle Introduction to Type Classes and Relations in Coq. はまさにこの点について解説しています。 次回の記事(予定)では多少の出番はありますが、 今回の記事では証明中で rewrite をしないので、 気になる方は是非こちらの文書を読んでみてください。

私は普段、圏論絡みの証明を記述する際に非常にお世話になっています。 射の等価性がジャンジャンバリバリですから。

5 再帰的な記法、あるいは手抜きのための努力

Map のために用意した記法をここに再掲します。

Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'").

あまり Notation コマンドを使ったことがないと何をしているのかわからないと思います。

しかし、私がこの形の命令を書けたのはしっかり元ネタがあるからに他なりません。

Reference Manual の 12.1.13 を御覧下さい。 ここでは例として存在量化子の再帰的な記法を定めています。 exists 記法はその後に任意個の束縛変数を記述することができました。 それをどのようにして実現しているのかが書かれています。

Map のための再帰的記法は、この exists と「同形」ですね。

再帰的な記法の代表例としてはリストの [1; 2; 3; ... 5] が挙げられますが、リストと存在量化の大きな違いは、変数による束縛の有無です。 x bindery binder といったオプションは、 xy が束縛子であることを明示するもので、少なくとも一方の指定は欠かせません。

再帰的な記法の定義は基本的に、記法とそれの意味するところの両者の繰り返し部分に .. を挿入することで可能となります。 繰り返す要素が一つであれば、大体思った通りの書き方で定義することができるでしょう。 繰り返すパラメータが複数あるような複雑なものは、そもそも Notation コマンドの限界を越えている可能性がありますので定義できない可能性が高いと思います。

パーサの実装は恐しいことになっているんだろうなぁ。

6 具体例

さて、 Map に対してもその具体例を定義してみましょう。

前回の記事では Coq に元々ある eq と、関数の外延的等価性の二つの同値関係について Setoid を定義しました。 まずは eq についての Setoid の間の Map を定義することにしましょう。

6.1 eq と Map

要は「通常の関数は全て Map である」ということです。

Program Definition eq_Map
	(A B: Type)(f: A -> B): Map (eq_Setoid A) (eq_Setoid B) :=
  [ x :-> f x ].

と定義を始めると、結果は

eq_Map has type-checked.
eq_Map is defined

となりました。どうやら、通常の関数が eq を保存することはもう自明のようですね。

これで、関数は Map であることが示せましたが、あまり面白くはなかったですね。 次いきましょう。

6.2 外延的等価性と Map

外延的等価性で以って関数が Setoid を構成しています。 その間の Map となれば、それは高階関数(の一種)ですね。

定義のステートメントは以下のようになります。

Definition fun_Map
	{X Y Z W: Type}(F: (X -> Y) -> (Z -> W))
: Map (fun_Setoid X Y) (fun_Setoid Z W).
  refine ([ f :-> F f ]).

さきほどとは違い Program コマンドを使わず、 refine タクティクを使ってみました。

先に結論を述べてしまいますが、 この定義は上手くいきません 。 アプローチが間違っているのではなく、そもそも 達成不可能な目標 です。

とはいえ、どこまで進めるのか見てみましょう。

ゴールは

1 subgoals, subgoal 1 (ID 35)
  
  X : Type
  Y : Type
  Z : Type
  W : Type
  F : (X -> Y) -> Z -> W
  ============================
   Proper ((==) ==> (==)) (fun f : fun_Setoid X Y => F f)


(dependent evars:)

となっています。まずは Proper などの定義を解いて simpl しておきます。

unfold Proper, respectful; simpl.

するとゴールはこのようになります。

1 subgoals, subgoal 1 (ID 37)
  
  X : Type
  Y : Type
  Z : Type
  W : Type
  F : (X -> Y) -> Z -> W
  ============================
   forall x y : X -> Y,
   (forall x0 : X, x x0 = y x0) -> forall x0 : Z, F x x0 = F y x0


(dependent evars:)

展開してみればあっさりしたものです。 intros で変数を仮定に上げてしまえば

intros f g Heq z.
1 subgoals, subgoal 1 (ID 85)
  
  X : Type
  Y : Type
  Z : Type
  W : Type
  F : (X -> Y) -> Z -> W
  f : X -> Y
  g : X -> Y
  Heq : forall x : X, f x = g x
  z : Z
  ============================
   F f z = F g z


(dependent evars:)

となるのですが、証明はここでストップとなります。 ここから先には進めません。 Heq の型を見ても、このゴールだと rewrite することもできませんね。

Abort.

今回、 F は単に (X -> Y) -> Z -> W という型を持つことしか制約がありません。 これが一般的に過ぎたのです。

例えば定数関数を与える const

Definition const {A B: Type}(a: A): forall _: B, A := fun _ => a.

と定義すると、これは AB をそれぞれ X -> YZ で具体化したとき、上述の F の一例となります。 最後のゴールの Fconst で置き換えると const f z = const g z となりますが、これはさらに f = g となります。

仮定には、 fg の間を関連づけるものは外延的等価性を意味する Heq しかありません。 これは Coq の eq よりも弱い命題ですから、 f = g を示すことはできない、という結論に至るわけです。

6.3 Map の存在意義

fun_Setoid 間の Map を構成する場合、 eq_Setoid の場合とは異なり、 具体的な関数それぞれについて行うことになります。

Map の具体例を構成することは即ち Proper クラスのインスタンスを構成することでもあります。 そして、 関数 f から(同値関係についての) Proper のインスタンスを構成できれば、

X : Setoid
Y : Setoid
f : Map X Y
x : X
y : X
Heq: x == y
============================
 f x == f y

という形のゴールの下で rewrite Heq. とすることができるようになります。

本記事では利用例を挙げることができませんでしたが、 Map の具体例を作る目的はこのように「 rewrite タクティクを使えるようにする」というところが大きいので、 そもそも具体的な定義もないような関数について Map を作れる場面の方が特殊だといえます。

7 おわりに

ということで、 Setoid 間の「写像」である Map を定義して、具体例の構成について触れつつ、ややこしい話を盛りこんでおきました。

同値関係を基準にして話をしたいときに eq が現れると、どうしても話がややこしくなってしまいます。 なのでいっそのこと始めから Setoid ベースでいいじゃないか、という考えに至ったりするのです。

同値関係を基にした rewrite は便利なので、 Setoid を使う使わないに限らず、作れるときには Proper クラスのインスタンスはなるべく作っておくとよいと思います。 ただし、あまりにも大規模になると、 rewrite タクティク一回で数十秒持っていかれますので、ご注意ください。

私の場合は Universe Polymorphism と併用したのが原因である可能性は非常に高いですが、 いずれにせよ Proper のインスタンスを探索するコストはかかりますからね。うん。 そういうことです。

次回(今週?来週?)はこの続きとしてマグマを取り扱う予定です。

Date: 2015/6/28 1:51:44

Author: mathink

Created: 2015-06-28 Sun 02:42

Validate