天泣記

Coq の dependent match (return を書くやつ) を調べていて、 inductive type の parameter というものに行き当たって調べてみた。

どうも、inductive type の型は parameter と arity というふたつで表現されるようだ。

以下のように、I1 と I2 を定義する。どちらも Type な引数をひとつ受け取ると Type になるという定義だが、書き方の違いにより、 I1 では parameter が (A:Type) で arity が Type となり、 I2 では parameter がなく arity が Type -> Type となる。 (parameter と arity という表現は <URL:https://coq.inria.fr/refman/cic.html> に出てくる。)

Inductive I1 (A:Type) : Type := c1 : A -> I1 A.
Inductive I2 : Type -> Type := c2 : forall (A : Type), A -> I2 A.

これらの違いは、I1, I2, c1, c2 の型には現れない。

About I1. (* I1 : Type -> Type *)
About I2. (* I2 : Type -> Type *)
About c1. (* c1 : forall A : Type, A -> I1 A *)
About c2. (* c2 : forall A : Type, A -> I2 A *)

しかし、コンストラクタの返値の型の中の A を A*A に変えると、 A が parameter の場合は失敗し、arity に入っている場合は成功する。これらはたしかに扱いが違うのである。

Fail Inductive I1' (A:Type) : Type := c1' : A -> I1 (A*A).
Inductive I2' : Type -> Type := c2' : forall (A : Type), A -> I2' (A*A).

また、dependent match の elimination predicate (return のところに書くやつ) や分岐において、 parameter は参照できないが、arity に入っている引数は参照できる。

A が parameter である I1 では、 in I1 B とか、c1 C v と書くとエラーになる (_ にしろといわれる)。

Check match c1 bool true as x in I1 _ return bool*(x=x) with c1 _ v => (v,eq_refl (c1 bool v)) end.
Fail Check match c1 bool true as x in I1 B return bool*(x=x) with c1 _ v => (v,eq_refl (c1 bool v)) end.
Fail Check match c1 bool true as x in I1 _ return bool*(x=x) with c1 C v => (v,eq_refl (c1 bool v)) end.

それに対して、A が arity に入っている I2 では、 in I2 B とか c2 C v と書けて、return の中で B を使えるし、分岐の中で C を使える。

Check match c2 bool true as x in I2 B return Type*B*(x=x) with c2 C v => (C,v,eq_refl (c2 C v)) end.

(Coq の内部的には、match の elimination predicate や分岐は関数として与えることになっていて、その関数に対して、 parameter は引数として与えられないが、arity 内の引数は実際に引数として与えられる、となっているようだ。上記の B や C はその引数の名前になるのだが、与えられない引数には名前を与えられないという表現もできる)

これをみると arity のほうが一般的なのでそれだけで済ませるような気もするが、にもかかわらずなぜ parameter を導入したのかという理由は昔の (Coq 8.4 のころの?) マニュアルに The information which says that for any A, (List A) is an inductively defined Set has been lost. と書いてあった。 <URL:https://github.com/coq/coq/commit/47377fa44143d409331dd7d0c662e6ebb34d9f4f#diff-cd87ec7e7676a1535a3f6bb1cfb4e511>

つまり、上の例だと I2' A のコンストラクタ c2' は I2' (A*A) を返すので (I2' A ではないので)、 I2' A は inductive に定義される型としては扱えないのが困るということだろうか。

この困り具合は、I1, I2 の定義時に同時に定義される induction principle にも現れている。

About I1_ind.  (* I1_ind :
  forall (A : Type) (P : I1 A -> Prop),
  (forall a : A, P (c1 A a)) -> forall i : I1 A, P i *)
About I2_ind.  (* I2_ind :
  forall P : forall T : Type, I2 T -> Prop,
  (forall (A : Type) (a : A), P A (c2 A a)) ->
  forall (T : Type) (i : I2 T), P T i *)

I1_ind では、A が最初の引数になっていて、I1_ind bool などと、 A を与えるだけで A を固定した (つまり I1 A に対する) induction principle を得られる。つまり、帰納法により、I1 bool に関する性質を (I1 nat などは無視して) 証明することができる。

しかし、I2_ind で同じことをするのは簡単でない。 P の中を工夫すれば可能だろうが、不便だろう。

なんでそんな induction principle になるかといえば、arity の部分は変わるかもしれないので、帰納法はそういう変化しうる全体に対して行わなければならないからだろう。

逆に、各コンストラクタが一貫して同じ引数を引き渡す形であれば、I1_ind のような induction principle を定義できるわけだ。で、I2 も実際はそういう形式なので、 I1_ind っぽい形の induction principle を I2 に対して定義することも可能なはず、ということで証明してみると以下のようになった。

Lemma I2ind_like_I1ind : forall (A : Type) (P : I2 A -> Prop),
  (forall a : A, P (c2 A a)) -> forall i : I2 A, P i.
Proof.
  intros A P H i.
  induction i.
  apply H.
Qed.

この証明だと明示的には現れていないが、induction i は I2_ind を使うので、 I2ind_like_I1ind は I2_ind に依存している。実際、証明項を表示させると以下のように I2_ind が含まれていることがわかる。

Print I2_ind_like_I1_ind.
(* I2_ind_like_I1_ind =
fun (A : Type) (P : I2 A -> Prop) (H : forall a : A, P (c2 A a)) (i : I2 A) =>
I2_ind
  (fun (A0 : Type) (i0 : I2 A0) =>
   forall P0 : I2 A0 -> Prop, (forall a : A0, P0 (c2 A0 a)) -> P0 i0)
  (fun (A0 : Type) (a : A0) (P0 : I2 A0 -> Prop)
     (H0 : forall a0 : A0, P0 (c2 A0 a0)) => H0 a) A i P H
     : forall (A : Type) (P : I2 A -> Prop),
       (forall a : A, P (c2 A a)) -> forall i : I2 A, P i
*)

天泣記

2018-03-13 (Tue)

2018-03-17 (Sat)

2018-03-24 (Sat)