天泣記

よくある依存型の例として、長さも型で区別するリスト型がある。 Coq にはこれが Vector という名前のライブラリで提供されている。

ここで、2つの vector を連結するのは append という関数が提供されているが、 3つの vector を連結する関数は提供されていないので、定義してみよう。

From mathcomp Require Import all_ssreflect.
Require Import Vector.
Import VectorNotations.

Infix "++" := append.

Fail Definition append3 {T : Type} {a b c : nat}
  (x : Vector.t T a) (y : Vector.t T b) (z : Vector.t T c) :
  Vector.t T (a + b + c) :=
  x ++ y ++ z.
(*
The term "x ++ y ++ z" has type "t T (a + (b + c))"
while it is expected to have type "t T (a + b + c)".
*)

ところが、上記のような定義はエラーになる。

理由はエラーメッセージのとおりで "x ++ y ++ z" の型が "t T (a + (b + c))" なのに、返り値の型として "t T (a + b + c)" が期待されているので、違うじゃないか、ということである。 (t というのは Vector.t のことである。)

違うところは (a + (b + c)) と (a + b + c) なので、それは同じだろうと人間にはわかるし、 Coq のライブラリの中には自然数の加算の結合則の定理はあるのだが、 Coq は型の一致については convertible というごく限定された関係しか調べてくれないので型エラーになってしまう。

この型エラーが起きる原因はプログラムの x ++ y ++ z で使った ++ が右結合で x ++ (y ++ z) の意味なのに、 a + b + c で使った + が左結合で (a + b) + c という意味だというミスマッチである。だからどちらかにあわせるという手はある。ただ、x ++ y ++ z を (x ++ y) ++ z にすると、リストの作り直しの手間が増える (x が 2回コピーされることになる) のでよろしくない。また、a + b + c を a + (b + c) にすると、プログラムの内部的な都合で外部APIを変えるということになってこれもよろしくない。

ということで、なんとか x ++ y ++ z と a + b + c のままで定義できないか考えたところ、 Vector.t T (a + (b + c)) 型の値を受け取って Vector.t T (a + b + c) という型の値を返す関数があればいいのではないかと考えついた。

ということで以下のように定義してみる。まぁ、このくらいなら証明項を直接書けるような気もするけれど、面倒なので proof editing mode で定義した。 rewrite するだけだけど。

Definition f {T : Type} {a b c : nat}
  (v : Vector.t T (a + (b + c))) : Vector.t T (a + b + c).
Proof.
  by rewrite -addnA.
Defined.

ともあれ、この f を使うと、以下のように append3 が定義できる。

Definition append3 {T : Type} {a b c : nat}
  (x : Vector.t T a) (y : Vector.t T b) (z : Vector.t T c) :
  Vector.t T (a + b + c) :=
  f (x ++ y ++ z).

とはいえ、定義できることはできるが、型では保証されない性質 (要素の順序とか) が期待通りに実現されているかどうかは明らかでない。これを確かめるには、rewrite がけっきょく eq_rect の呼び出しを生成して、 eq_rect は (型は変えるけど) 値をそのまま返すから変えない、ということを確認すれば納得できるか。

それはそうと、動かしてみるか、とやってみると例えば以下のようになる。

Compute (append3 [1; 2; 3] [4; 5; 6] [7; 8; 9]).
= match addnA 3 3 3 in (_ = x) return (t nat x) with
  | erefl _ _ => [1; 2; 3; 4; 5; 6; 7; 8; 9]
  end
: t nat (3 + 3 + 3)

あー、addnA は展開できないので (Qed で定義されていて Opaque なので)、そこは計算が進まないなぁ。

あと、f を別に定義せずに済ますこともできる。

Definition append3' {T : Type} {a b c : nat}
  (x : Vector.t T a) (y : Vector.t T b) (z : Vector.t T c) :
  Vector.t T (a + b + c).
Proof.
  refine (_ (x ++ y ++ z)).
  by rewrite -addnA.
Defined.

ここでは、proof editing mode の中で refine を使って、 f があったところ以外は具体的なプログラムを与え、 f のところは tactic で埋めている。

#3 SSReflect の tuple

Vector みたいなものは SSReflect にあったっけか、と思って探してみると、tuple というのがあるようだ。

同じことを試してみよう。

まず、x ++ y ++ z が (a + b + c).-tuple T 型にならずにエラーになるのは同じである。

From mathcomp Require Import all_ssreflect.

Fail Definition cat3 {T : Type} {a b c : nat}
  (x : a.-tuple T) (y : b.-tuple T) (z : c.-tuple T) :
  (a + b + c).-tuple T :=
  [tuple of x ++ y ++ z].
(*
The term "[tuple of x ++ y ++ z]" has type "(a + (b + c)).-tuple T"
while it is expected to have type "(a + b + c).-tuple T".
*)

で、型を変換する必要があるのだが、これも同じようにできる。

Definition cat3 {T : Type} {a b c : nat}
  (x : a.-tuple T) (y : b.-tuple T) (z : c.-tuple T) :
  (a + b + c).-tuple T.
Proof.
  refine (_ [tuple of x ++ y ++ z]).
  by rewrite addnA.
Defined.

ここでは refine を使ってみたが、もちろん型を変換する関数を別に定義して使っても良い。

動かしてみると以下のようになる。

Compute (cat3 [tuple 1; 2; 3] [tuple 4; 5; 6] [tuple 7; 8; 9]).
= match
    match addnA 3 3 3 in (_ = x) return (x = 9) with
    | erefl _ _ => erefl (3 + (3 + 3))
    end in (_ = x) return (x.-tuple nat -> 9.-tuple nat)
  with
  | erefl _ _ => id
  end
    (Tuple (n:=9) (tval:=[:: 1; 2; 3; 4; 5; 6; 7; 8; 9])
       (cat_tupleP
          (Tuple (n:=3) (tval:=[:: 1; 2; 3])
             (valP
               ... 以下省略 ...

addnA は展開できないので計算が進んでいないのはそれとして、かなり大きな証明項がついている。これは、tuple は (Vector と違って) リストと、リストの長さが特定の値であるという証明をペアにしたものとして定義されているからで、その証明のところがかなり大きくなっている。

あと、SSReflect には tcast という、長さが等しいという証明を与えると型を変えてくれる関数があるようだ。それを使うと 3つの tuple の連結は以下のように定義できる。

Definition cat3' {T : Type} {a b c : nat}
  (x : a.-tuple T) (y : b.-tuple T) (z : c.-tuple T) :
  (a + b + c).-tuple T.
Proof.
  refine (tcast _ [tuple of x ++ y ++ z]).
  (* subgoal: a + (b + c) = a + b + c *)
  by apply addnA.
Defined.

これも動かしてみよう、と思って試すと、以下のようになる。

Compute (cat3' [tuple 1; 2; 3] [tuple 4; 5; 6] [tuple 7; 8; 9]).
= ecast x (x.-tuple nat) (addnA 3 3 3)
    (Tuple (n:=3 + (3 + 3)) (tval:=[:: 1; 2; 3; 4; 5; 6; 7; 8; 9])
       (cat_tupleP
          (Tuple (n:=3) (tval:=[:: 1; 2; 3])
  ... 以下省略 ...

ecast というのが一番外側に残っているが、そのちょっと内側に [:: 1; 2; 3; 4; 5; 6; 7; 8; 9] というのがあって、そのあたりが計算結果かな。

天泣記

2018-02-04 (Sun)

2018-02-22 (Thu)