天泣記

まず最初に結論を書いておく: Coq 標準ライブラリの Vector.t や Fin.t は使わず、SSReflect の tuple や fintype を使うことを勧める

インデックス付き帰納型 (indexed inductive type) の場合分けは難しい。 (インデックス付き帰納型は、依存型と重なる部分もあるが、厳密には違うと思う。後述する)

例として Coq 標準ライブラリの Vector.t を使う。 (ただし、Vector の利用を推奨するわけではない。SSReflect の tuple のほうが苦労がない)

From mathcomp Require Import all_ssreflect.
Require Vector.

Print Vector.t.
(*
Inductive t (A : Type) : nat -> Type :=
    nil : Vector.t A 0
  | cons : A -> forall n : nat, Vector.t A n -> Vector.t A n.+1.
*)

依存型の例としてよくあげられる、型で長さが指定されたリストである。例えば、Vetor.t bool 3 は長さ 3 で要素が bool のリストである。

ここで、長さ 0 の vector は nil であることを証明したいとする。 vector 型の値は、vector のコンストラクタのいずれかで生成されているので、 vector 型の変数を case で場合分けすれば、nil の場合と cons の場合に場合分けされて証明が進む、と期待するところであるが、やってみるとエラーになる。

Lemma vector_nil: forall A (v : Vector.t A 0), v = Vector.nil A.
Proof.
  move=> A.
  case.
(*
Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "Vector.t A n" : "Type"
 "t" : "Vector.t A n"
 "Vector.nil A" : "Vector.t A 0"
The 3rd term has type "Vector.t A 0" which should be a subtype of
 "Vector.t A n".
*)

真面目に考えずにいろいろ試すと、以下のようになった

case は上記のようにダメ
destruct もダメ
dependent destruction は Program.Equality が必要
Require Import Program.Equality とすると、dependent destruction が使えて証明できる (cons の場合のサブゴールは生成されない) ただし、Print Assumptions vector_nil で公理 Eqdep.Eq_rect_eq.eq_rect_eq を使っていると出てくる

dependent destruction で成功した証明は以下である。

From mathcomp Require Import all_ssreflect.
Require Vector.
Require Import Program.Equality.

Lemma vector_nil: forall A (v : Vector.t A 0), v = Vector.nil A.
Proof.
  move=> A v.
  by dependent destruction v.
Qed.
Print Assumptions vector_nil.
(*
Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
    x = eq_rect p Q x p h
*)

これで証明できたからいいか、と済ませるのもひとつの手だが、 dependent destruction がなにをやっているのかわからないし、公理 eq_rect_eq がなんで必要なのか、絶対に必要なのかどうかもわからない。

もうちょっと真面目に考えてみよう。しばらく考えた結果、以下のような結論に達した。

Vector.t や Fin.t は使わず、SSReflect の tuple や fintype を使うのが一番よい
どうしても Vector を使う場合、Vector の場合分けは Vector ライブラリで提供されている補題を使う (Fin も同様)
eq_rect を使わずに場合分けする (Vector.t, Fin.t)
eq_rect を使って場合分けする (eq, le)

#2 インデックス付き帰納型

Coq で扱える難しい型のことをなんでも依存型と呼ぶ風潮がある気がするのだが、型システム入門によれば依存型は「項でインデックス付けされた型」なので、ここで議論したい対象とはちょっとずれている。

Coq の帰納型は一般には以下のように定義される。 (実際には、さらに mutual な場合があるが、それは無視している)

Inductive D (a1 : A1) ... (ap : Ap) : B1 -> ... -> Bn -> sort :=
| C1 : forall ..., -> D a1 ... ap b11 ... b_{1n_1}
...
| Ck : forall ..., -> D a1 ... ap b1k ... b_{1n_k}

- (a1 : A1) ... (ap : Ap) はパラメータ
- B1 -> ... -> Bn -> sort は arity
- B1, ..., Bn は正式な呼び名がない気がするのだが、インデックスと呼ぶことにする
- C1, ..., Ck はコンストラクタ
- Ci の forall ..., はコンストラクタの引数
  実際に呼び出すときには引数としてパラメータも与える必要がある:
  Ci : forall (a1 : A1) ... (ap : Ap) ..., D a1 ... ap b1 ... bn
- Ci の D a1 ... ap b1 ... bn はコンストラクタの返値の型
  a1 ... ap はパラメータをそのまま与えなければならない
  b1 ... bn はパラメータ a1 ... am を含むコンストラクタの引数を含んでよい

まぁ、パラメータだって引数なんだからインデックス (添字) と呼びたくなるかもしれないが、ここではパラメータはインデックスとは呼ばないことにする。

ここで議論したいインデックス付き帰納型というのは、帰納型の定義で、インデックス B1, ..., Bn が空でない (0 < n) もののことである。

インデックス付き帰納型 (indexed inductive type) というのは一般的な用語ではない気がするが、この名前は、Coq のマニュアルの Simple indexed inductive types という節タイトルからとってきた。

そして、依存型というのは値を添字としてもつ型である。ということは、上の帰納型の定義で言えば、A1, ..., Ap, B1, ..., Bn のひとつ以上が値の型であるものである。

なので、インデックス付き帰納型でない場合 (インデックスがない場合) であっても、パラメータ A1, ..., Ap に値の型が現れれば依存型である。また、インデックス付き帰納型である場合 (インデックスがある場合) であっても、A1, ..., Ap, B1, ..., Bn がすべて型の型 (ソート) であれば依存型でない。

というわけで、インデックス付き帰納型と依存型は異なるものである。

具体例でいえば、Vector.t A n は、Vector.t が Inductive t (A : Type) : nat -> Type := ... と定義されていて、n = 1 (B1 が nat) なので、インデックス付き帰納型であり、また、nat は値の型なので、依存型でもある。

また、GADT の例ででてくる、exp T 型 (結果が T 型であるような式の型) は、添字 T が型なので依存型とはいえないが、インデックス付き帰納型とはいえるだろう。

また、SSReflect の tuple は Record tuple_of (n : nat) (T : Type) : Type := ... という定義になっていて、 (Inductive ではなく Record になっているがその違いはここでは重要ではない) パラメータ ((a1 : A1) ... (ap : Ap)) の部分に (n : nat) (T : Type) があり、B1, ..., Bn は空である。つまり、インデックス付き帰納型ではないが、依存型ではある。

なお、nat は Inductive nat : Set := O : nat | S : nat -> nat. と定義され、パラメータもインデックスもないので、インデックス付き帰納型でも依存型でもない。

当然だが、帰納型のコンストラクタは、その帰納型の値を返さなければならない。帰納型 t a1...ap b1...bn の値を返すコンストラクタ C の型は C : forall (a1 : A1) ... (ap : Ap) (x1 : T1) ... (xm : Tm), t a1...ap b1...bn という形になる。これはコンストラクタ C がまず最初に帰納型のパラメータ (a1...ap) を受け取り、その他の引数を受け取り、その帰納型の値を返すという意味である。ここで、a1...ap は、引数として受け取ったパラメータを return type のところにそのまま書かなければならない。そして、b1...bn には、引数 a1...ap, x1...xm を使った式を記述することができる。

つまり、ある帰納型 t a1...ap b1...bn の値は、その帰納型のコンストラクタで作られており、そのコンストラクタに与えられたパラメータは (型についている) a1...ap そのものである。そして、それ以外の引数 x1...xm は、インデックスが b1...bn になるような値であるはずである。

インデックス付き帰納型の場合分けで問題になるのは、「それ以外の引数 x1...xm は、インデックスが b1...bn になるような値であるはず」というところである。インデックスがなければ、x1...xm にはとくに制約はなく、任意の値と考えればよいのだが、インデックスがあると、インデックスによる制約を扱う必要がある。これが難しい。

最初に書いた Vector.t の場合分けをちょっと一般的にすると、forall (v : Vector.t A n), P v を証明するのに nil の場合と cons の場合に場合分けして証明したいわけである。インデックスがないなら P (Vector.nil A) と forall (n' : nat) (v' : Vector.t A n'), P (Vector.cons A n' v') のふたつを証明すればよいのだが、 Vector.t にはインデックスがあるのでこれはうまくいかない。どううまくいかないかというと、P の型が Vector.t A n -> Prop なのに、 Vector.nil A の型は Vector.t A 0 で、 Vector.cons A n' v' の型は Vector.t A n'.+1 で、どちらにしても型が異なる (nil の場合は n と 0 が異なり、cons の場合は n と n'.+1 が異なる) のが問題で、場合分けできないというわけである。

#3 (1) Vector.t や Fin.t は使わず、SSReflect の tuple や fintype を使うのが一番よい

繰り返すが、インデックス付き帰納型は使わないのがいちばんである。 Coq 標準ライブラリの Vector.t と Fin.t はインデックス付き帰納型であるが、それに同等な表現能力をもちインデックスを使わない tuple と fintype が SSReflect に用意されているので、そちらを使うのがよい。

なお、Coq の標準ライブラリの Vector を replace/deprecate しようという issue があるが、そうなる感じではなさそう。

GitHub coq/coq/issues/6459: Vector library needs to replaced/deprecated.

あと、検索していて見つけたが、帰納型の定義の中で、Vector.t は使えるが、tuple は使えないということがあるようだ。

ただ個人的な感想としては、これは positivity condition が十分に一般的でない (改善の余地がある) ためな気がする。

#4 (2) どうしても Vector を使う場合、Vector の場合分けは Vector ライブラリで提供されている補題を使う (Fin も同様)

さて、tuple や fintype を使わない、苦難の道を選んだとしよう。

この場合、場合分けをどうすればいいかというと、いちばんマシなのは、ライブラリに用意されている補題を使うというものだろう。

場合分けが難しいことはライブラリの作者もわかっているので、必要な道具は用意されているのである。

ただ、マニュアルに載っているなかでどれを使えばいいか、という問題はある。 Vector については rectS, case0, caseS, caseS' のどれを使えばいいか。あと、マニュアルには載っていないのだが、帰納型を定義したときに自動的に t_rect, t_rec, t_ind, t_sind という4つも定義されていて、これも提供されている。これら 8つのどれを使うのがいいだろうか。

これらの型は以下のとおりである。

Vector.rectS :
  forall {A : Type} (P : forall n : nat, Vector.t A n.+1 -> Type),
  (forall a : A, P 0 (Vector.cons A a 0 (Vector.nil A))) ->
  (forall (a : A) (n : nat) (v : Vector.t A n.+1),
   P n v -> P n.+1 (Vector.cons A a n.+1 v)) ->
  forall (n : nat) (v : Vector.t A n.+1), P n v

Vector.case0 :
  forall {A : Type} (P : Vector.t A 0 -> Type),
  P (Vector.nil A) -> forall v : Vector.t A 0, P v

Vector.caseS :
  forall {A : Type} (P : forall n : nat, Vector.t A n.+1 -> Type),
  (forall (h : A) (n : nat) (t : Vector.t A n), P n (Vector.cons A h n t)) ->
  forall (n : nat) (v : Vector.t A n.+1), P n v

Vector.caseS' :
  forall {A : Type} {n : nat} (v : Vector.t A n.+1)
    (P : Vector.t A n.+1 -> Type),
  (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v

Vector.t_rect :
  forall (A : Type) (P : forall n : nat, Vector.t A n -> Type),
  P 0 (Vector.nil A) ->
  (forall (h : A) (n : nat) (t : Vector.t A n),
   P n t -> P n.+1 (Vector.cons A h n t)) ->
  forall (n : nat) (t : Vector.t A n), P n t

Vector.t_rec :
  forall (A : Type) (P : forall n : nat, Vector.t A n -> Set),
  P 0 (Vector.nil A) ->
  (forall (h : A) (n : nat) (t : Vector.t A n),
   P n t -> P n.+1 (Vector.cons A h n t)) ->
  forall (n : nat) (t : Vector.t A n), P n t

Vector.t_ind :
  forall (A : Type) (P : forall n : nat, Vector.t A n -> Prop),
  P 0 (Vector.nil A) ->
  (forall (h : A) (n : nat) (t : Vector.t A n),
   P n t -> P n.+1 (Vector.cons A h n t)) ->
  forall (n : nat) (t : Vector.t A n), P n t

Vector.t_sind :
  forall (A : Type) (P : forall n : nat, Vector.t A n -> SProp),
  P 0 (Vector.nil A) ->
  (forall (h : A) (n : nat) (t : Vector.t A n),
   P n t -> P n.+1 (Vector.cons A h n t)) ->
  forall (n : nat) (t : Vector.t A n), P n t

どれも型が長くてどこが重要なのかわかりにくいのだが、大きな違いとして、P が n を引数にとるかとらないか、という違いがある。 case0, caseS' はとらないが、他はとる。

つまり、P は Vector.t A n 型の値に関する述語なのだが、場合分けしたい対象の式が Vector.t A n 型であるとすると、 case0, caseS' の P はその特定の長さ n の vector についての述語なのに対し、他の P は任意の長さ n の vector についての述語なのである。

この違いは、単なる場合分けと帰納法の違いに対応する。単なる場合分けならば、P は場合分けしたい対象の長さ n についてだけ扱えればよいのだが、帰納法だと帰納法の各ステップについて P を使える必要があるので特定の長さだけでは足りないのである。 (ただし、caseS (ダッシュがつかないほう) は単なる場合分けなのに P が n を引数にとるのはどういう意図かわからない。)

この違いはまた、case0, caseS' を使う前にゴールを P v という形に beta expansion する必要があるのに対して、それ以外は P n v という形に beta expansion する必要があるということを意味している。

この beta expansion が成功するか失敗するかは、ゴールによって異なるのだが、前出の vector_nil の場合は、P n v という形にはできないが、P v という形にはできる。

Lemma vector_nil: forall A (v : Vector.t A 0), v = Vector.nil A.
Proof.
  move=> A v.
  Fail pattern 0, v.
  (*
  The command has indeed failed with message:
  Illegal application:
  The term "@eq" of type "forall A : Type, A -> A -> Prop"
  cannot be applied to the terms
   "Vector.t A n" : "Type"
   "t" : "Vector.t A n"
   "Vector.nil A" : "Vector.t A 0"
  The 3rd term has type "Vector.t A 0" which should be a subtype of
   "Vector.t A n".
  *)
  pattern v.
  (* (eq^~ (Vector.nil A)) v *)
  apply Vector.case0.
  (* Vector.nil A = Vector.nil A *)
  by [].
Qed.
Print Assumptions vector_nil.
(* Closed under the global context *)

ここでは、vector の長さは 0 なので、pattern 0, v によって 0 と v を引数に括り出すような beta expansion に挑戦して失敗している。まぁ、等式の右辺に Vector.nil A があって、これは Vector.t A 0 型なので、左辺も長さ 0 でなければならない。なので、長さを引数に受け取る関数の形にすると、引数として受け取った長さと右辺の長さが一致しないことになるのである。

長さを引数にせず、単に v だけを引数に括り出すのは pattern v で成功している。これにより、apply Vector.case0 とすると、v が Vector.nil A に置き換わり、左辺右辺が一致するので、あとは自明に証明できる。

そして、このようにして証明した vector_nil には公理は使われていない。つまり、この場合は証明に公理は不要なのであった。

なお、apply Vector.case0 する前に pattern で beta expansion するのは、 Vector.case0 の結論 P v の P と v になにを対応させるかを制御するためである。 pattern しないで (ゴールが v = Vector.nil A のままで) apply Vector.case0 すると一見なにも変化がないが、じつは、P に (eq v), v に (Vector.nil A) が対応されていて、(Vector.nil A) が (Vector.nil A) が置き換わるがなにも変わっていない、ということになる。

また、後述する tuple_of_vector や vector_of_tuple_of_vector では、Vector.t_rect を使っていて pattern n, v が必要になるが、特に問題なく成功する。これは vector と tuple の変換関数や、その逆変換が可能という話なのだが、この状況では、上記の Vector.nil A のような、長さが固定される要素がないので、任意の長さの vector についての命題とみなせるからである。

ちなみに、有限集合 Fin.t も rectS, case0, caseS, caseS', t_rect, t_rec, t_ind, t_sind があるが、 case0 と caseS' が単純な場合分けのためのものである。

#5 (3) Vector.case0 と Vector.caseS' の仕掛け

不幸にしてインデックス付き帰納型を使わなければならず、ライブラリが適切な場合分けの補題を用意してくれていないという場合、自分で補題を用意する必要があるかもしれない。

Vector についてはライブラリが提供してくれているので問題ないのだが、自分でやるならどうするか、ということで、Vector.case0 と Vector.caseS' を例として、これらがなにをやっているのか説明してみよう。

これらの型は以下のとおりである。

Vector.case0 :
  forall {A : Type} (P : Vector.t A 0 -> Type),
  P (Vector.nil A) -> forall v : Vector.t A 0, P v

Vector.caseS' :
  forall {A : Type} {n : nat} (v : Vector.t A n.+1)
  (P : Vector.t A n.+1 -> Type),
  (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v

ここで重要なのは、結論 P v の v の型が、Vector.t A 0 と Vector.t A n.+1 になっている点である。

最初に書いた Vector.t の場合分けがうまくいかないのは、forall (v : Vector.t A n), P v を証明するのに P (Vector.nil A) と forall (n' : nat) (v' : Vector.t A n'), P (Vector.cons A n' v') のふたつの証明で済ましたいというのが P と引数の型があわないので無理だった、というのはここでは、P の型がそれぞれ Vector.t A 0 -> Type と Vector.t A n.+1 -> Type になっていることで解決されている。 Vector.case0 の場合だと P : Vector.t A 0 -> Type なので、P v を P (Vector.nil A) に置き換えても型は合う。

case0 を自分で定義してみよう。標準ライブラリの実装を見ずに書いたら以下のようになった。

From mathcomp Require Import all_ssreflect.
Require Vector.

Definition my_case0 :
    forall {A : Type} (P : Vector.t A 0 -> Type),
    P (Vector.nil A) -> forall v : Vector.t A 0, P v.
  move=> A P H v.
  move: H.
  (* P (Vector.nil A) -> P v *)
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
    (* P (Vector.nil A) -> P (Vector.nil A) *)
    by apply.
  (* IDProp *)
  by exact idProp.
Defined.

ゴールを P (Vector.nil A) -> P v という形にした後に、 refine で match v with ... end という証明項を作っている。 match の各分岐にはとくになにも書いていなくて、後で埋めることになる。

そうすると、nil と cons に対応したふたつのゴールができる。それぞれ P (Vector.nil A) -> P (Vector.nil A) と IDProp となる。

nil の場合の P (Vector.nil A) -> P (Vector.nil A) は、自明に証明できる。 P (Vector.nil A) の証明を受け取って P (Vector.nil A) の証明を返す関数を書けばいいので、単に引数を返す恒等関数が証明となる。

cons の場合には IDProp という謎の命題が出てくるが、検索すると idProp: IDProp というのがあるので、idProp で証明できる。 v : Vector.t A 0 であることから、v が cons で作られることはありえないので、簡単に証明できる命題として IDProp が出てくるのだろう。

ちなみに、IDProp の中身は forall A : Prop, A -> A というもので、 idProp は fun (A : Prop) (x : A) => x である。簡単に証明できるというなら True とかでもいいと思うのだが、たぶん、Coq の内部から、True みたいなライブラリの定義を参照するのを嫌ったのではないかという気がする。（とはいえ、IDProp と idProp も Coq.Init.Datatypes で定義される定数なので、結局ライブラリ定義を参照しているのだが。昔の Coq だと定数になっていなかったりしないだろうか? 調べてないけど）

さて、この定義は簡単に書けたが、じつは Coq がたくさん助けてくれているのである。定義を表示すると以下のようになる。

Print my_case0. (* my_case0 =
fun (A : Type) (P : Vector.t A 0 -> Type) (H : P (Vector.nil A))
  (v : Vector.t A 0) =>
match
  v as v0 in (Vector.t _ n)
  return
    (match n as x return (Vector.t A x -> Type) with
     | 0 => fun v1 : Vector.t A 0 => P (Vector.nil A) -> P v1
     | n0.+1 => fun=> IDProp
     end v0)
with
| @Vector.nil _ => id
| @Vector.cons _ _ _ _ => idProp
end H
     : forall (A : Type) (P : Vector.t A 0 -> Type),
       P (Vector.nil A) -> forall v : Vector.t A 0, P v
*)

自分では書かなかったが match に as-in-return 節が付加されていて、そのなかでさらに match しているという複雑なことになっている。

return節は、match 式自体の型を指定するもので、ここでは、n が 0 の場合とそうでない場合 (n0.+1 の場合) で場合分けしている。それぞれの場合は nil と cons の場合に対応しているのだが、 cons の場合は (今回は n が 0 なので) ありえなくて、その場合はすぐに証明できる IDProp という命題としている。 nil の場合は、P (Vector.nil A) -> P v1 という命題にしている。 v1 というのはさらに match が関数を返してそれを即座に呼び出しているといった複雑なことになっているが、最終的には、match の (nil の) 分岐の中では Vector.nil A になり、外では v になる、というように指示されている。

なお、match が関数を返して、その関数を即座に呼び出すのは convoy pattern と呼ばれているテクニックで、型を変えるためもものである。ここでは、v0 の型が Vector.t A n 型であって P には渡せないのを、Vector.t A 0 型の v1 で受け取って、P に渡せるようにしている。

では、caseS' も自前で証明してみよう。こっちは難航した。

From mathcomp Require Import all_ssreflect.

Definition my_caseS' :
    forall {A : Type} {n : nat} (v : Vector.t A n.+1)
    (P : Vector.t A n.+1 -> Type),
    (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
  move=> A n v P.
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
  (* IDProp と
     (forall (h : A) (t0 : Vector.t A n), P (Vector.cons A h n t0)) -> P v に
     なるが、話が進んでいない。どうやら、自分で as-in-return 節を書く必要があるようだ *)
  Undo.
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => True
      | n1.+1 =>
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end); [by constructor|].
  (* nil の場合は True ということにして、即座に by constructor で証明してしまう。
     残りのが (forall (h : A) (t0 : Vector.t A n), P (Vector.cons A h n t0)) -> P v
     のまま変わらないことを確認 *)
  Undo.
  (* P v の部分は、match の中と外で変えたいので、as 節に書いた v0 に置き換える。 *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => True
      | n1.+1 =>
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end); [by constructor|].
  (* The term "v0" has type "Vector.t A n0" while it is expected to have type
 "Vector.t A n.+1". というエラーになってしまう。*)
  (* P の型は Vector.t A n.+1 -> Type なので、n.+1 を n0 に置き換えないといけないのだろうな、ということで P を convoy pattern で変えてみよう *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n0 -> Type),
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* 今度は The term "Vector.cons A h n t" has type "Vector.t A n.+1"
while it is expected to have type "Vector.t A n0". というエラーになった。*)
  (* あぁ、n1.+1 の分岐にも n がふたつ使われているので match の内外で変わるやつにしないといけないか。
    n.+1 が n0 に対応していて、n0 が n1.+1 に対応しているので、n を n1 にすればいいだろう。
 *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n0 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term "Vector.cons A h n1 t" has type "Vector.t A n1.+1"
while it is expected to have type "Vector.t A n0". になった *)
  (* P が Vector.t A n0 を受けとるのではダメで、n1.+1 にしないといけなさそう *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term "v0" has type "Vector.t A n0" while it is expected to have type
 "Vector.t A n1.+1". というエラーになった *)
  (* v0 の型を Vector.t A n0 から Vector.t A n1.+1 に変えるために convoy pattern を使う *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => fun v1 => forall P, True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term
       "forall P : Vector.t A n1.+1 -> Type,
        (forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1"
     has type "Type" while it is expected to have type "Prop"
     (universe inconsistency: Cannot enforce max(Set, Top.25711, Top.25872+1) <=
     Prop). というエラーになった *)
  (* えーと、なんだろ？　match n0 の return 節が変に補完されてるのか?
     自分で書いてみよう *)
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 as x return Vector.t A x -> Type with
      | 0 => fun v1 => forall P, True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* やった。成功した。でも、nil の場合が
     ?Goal@{n0:=0; v0:=Vector.nil A; v1:=Vector.nil A} -> True
     という謎の前提がくっついてるな。P の型を書かなかったからか? *)
  Undo.
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 as x return Vector.t A x -> Type with
      | 0 => fun v1 => forall (P : Vector.t A 0 -> Type), True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* 謎の ?Goal は消えたのでこれでよし *)
    (* (Vector.t A 0 -> Type) -> True *)
    by [].
  (* forall P0 : Vector.t A n0.+1 -> Type,
     (forall (h : A) (t0 : Vector.t A n0), P0 (Vector.cons A h n0 t0)) ->
     P0 (Vector.cons A a n0 t) *)
  (* 結局、P0 (Vector.cons A h n0 t0)) -> P0 (Vector.cons A a n0 t) なので自明に証明できる *)
  by [].
Qed.

Print my_caseS'. (* my_caseS' =
fun (A : Type) (n : nat) (v : Vector.t A n.+1) =>
[eta match
       v as v0 in (Vector.t _ n0)
       return
         (match n0 as x return (Vector.t A x -> Type) with
          | 0 => fun=> (Vector.t A 0 -> Type) -> True
          | n1.+1 =>
              fun v1 : Vector.t A n1.+1 =>
              forall P0 : Vector.t A n1.+1 -> Type,
              (forall (h : A) (t : Vector.t A n1), P0 (Vector.cons A h n1 t)) ->
              P0 v1
          end v0)
     with
     | @Vector.nil _ => fun=> I
     | @Vector.cons _ h n0 t =>
         fun (P0 : Vector.t A n0.+1 -> Type)
           (X : forall (h0 : A) (t0 : Vector.t A n0),
                P0 (Vector.cons A h0 n0 t0)) => X h t
     end]
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1)
         (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v
*)

難航したが、証明できた。基本的には (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v の v を Vector.cons A h n t に置き換えるという方針のもとに、型エラーにひとつずつ対処していくという話である。

なお、IDProp でなくても簡単に証明できるものであればいいはず、ということで True を使ってみた。

しかし、見直してみると、P の型を convoy pattern で変えているが、最初に Coq に補助させようとしたときには P がゴールに入っていなかったのがうまくいかなかった理由かもしれない。ゴールに P を残したまま refine するとどうだろうか。

Definition my_caseS'' :
    forall {A : Type} {n : nat} (v : Vector.t A n.+1)
    (P : Vector.t A n.+1 -> Type),
    (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
  move=> A n v.
  (* forall P : Vector.t A n.+1 -> Type,
     (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v *)
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
    by exact idProp.
  (* forall P : Vector.t A n0.+1 -> Type,
      (forall (h : A) (t0 : Vector.t A n0), P (Vector.cons A h n0 t0)) ->
      P (Vector.cons A a n0 t) *)
  move=> P.
  by apply.
Qed.

おぉ、うまくいった。

#6 (4) eq_rect を使って場合分けする

さて、Vector.t の場合はなんとか場合分けの補題を定義できたが、一般にはどうだろうか。

標準ライブラリにあるインデックス付き帰納型としては、他に Fin.t, eq, le がある。 Fin.t はライブラリが case0 と caseS' を提供しているので、Vector.t と同様である。

eq や le については、しばらく試した限りでは、case0 や caseS' みたいな証明はできなかった。

ではできないのかというと、(条件はあるけれど) できなくはなくて、以下に方法が紹介されている。 (条件というのは、インデックスの型に decidable equality があることである)

James Wilcox, Dependent Case Analysis in Coq without Axioms, September 14, 2014

マニュアルを探すと、inversion_sigma のところの Example: Using inversion_sigma は関連しているような気がする。

Coq Manual: inversion_sigma

また、Coq FAQ にも関連する記載があるようだ。

基本的なアイデアは、型が合わなければ eq_rect で型を変えてしまえ、というものである。

eq_rect は、eq 型の induction principle (ないし recursor) であるが、 rewrite が生成する証明項で使うやつ、という認識が簡単かも知れない。 (実際に rewrite が使うのは、eq_ind_r と eq_ind だけど。sort が違って Type と Prop だが。) rewrite はゴールを書き換えるわけだが、ゴールというのは命題であってつまり型なので、型を変えるものである。ということで、eq_rect を使うと型を変えられるので、型が合わないところに eq_rect を入れて型を合わせてしまうことができる、という話である。もちろん、自由に変えられるわけではなく、a を b に変えるには、それらが等しいという a = b の証明が必要である。

この方法を使って vector_nil を証明してみよう。

From mathcomp Require Import all_ssreflect.
Require Vector.

Lemma vector_nil: forall A (v : Vector.t A 0), v = Vector.nil A.
Proof.
  move=> A v.
  refine (match v as v' in Vector.t _ n'
                return forall pf : n' = 0,
                         eq_rect n' (Vector.t A) v' 0 pf = v ->
                         v = Vector.nil A with
            | Vector.nil => _
            | Vector.cons _ _ _ => _
          end erefl erefl).
    (* forall pf : 0 = 0,
       eq_rect 0 (Vector.t A) (Vector.nil A) 0 pf = v -> v = Vector.nil A *)
    move=> pf.
    (* eq_rect 0 (Vector.t A) (Vector.nil A) 0 pf = v -> v = Vector.nil A *)
    rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
    by [].
  (* forall pf : n.+1 = 0, ... *)
  by [].
Qed.

Print Assumptions vector_nil.
(* Closed under the global context *)

要点は、match の return 節で forall pf : n' = 0, eq_rect n' (Vector.t A) v' 0 pf = v -> (その時点のゴール) として、その時点のゴールにふたつの等式を加えることである。ゴール自体はいじらないので、そこで型が壊れることはない。最初の等式は n' = 0 で、これは match 式全体としては 0 = 0 となり、nil の分岐では 0 = 0, cons の分岐では n.+1 = 0 となる。後の等式は eq_rect n' (Vector.t A) v' 0 pf = v で、 match 式全体としては eq_rect 0 (Vector.t A) v 0 pf = v となり、 nil の分岐では eq_rect 0 (Vector.t A) (Vector.nil A) 0 pf = v, cons の分岐では eq_rect n.+1 (Vector.t A) (Vector.cons A a n t) 0 pf = v となる。

とくに cons の分岐で現れる eq_rect n.+1 (Vector.t A) (Vector.cons A a n t) 0 pf = v は、左辺の Vector.cons A a n t : Vector.t A n.+1 と右辺の v : Vector.t A 0 が等式で結ばれていて、本来は型が異なって等式にできなかったはずのものが、eq_rect で型を変えることによって等式で表現できている。 (もちろん、pf : n.+1 = 0 という矛盾する等式があるからできることである)

cons の分岐は n.+1 = 0 という矛盾する前提があるので証明は簡単に終わる。

nil の分岐では eq_rect 0 (Vector.t A) (Vector.nil A) 0 pf を Vector.nil A に書き換えるのに、 Eqdep_dec.eq_rect_eq_dec を使っている。ここで Eqdep_dec.eq_rect_eq_dec は decidable equality を必要とするので、PeanoNat.Nat.eq_dec を与えている。

match 式全体としては、eq_rect 0 (Vector.t A) v 0 pf = v であるが、match 式が返す関数には引数として erefl がふたつ与えられており、最初の erefl がこの pf に束縛される。そうすると eq_rect の計算が進むので、結局 v = v と convertible となり、ふたつめの erefl でこれを満たせることになる。

case0 と caseS' を eq_rect を使って証明してみよう。

Definition my_case0 :
    forall {A : Type} (P : Vector.t A 0 -> Type),
    P (Vector.nil A) -> forall v : Vector.t A 0, P v.
  move=> A P H v.
  refine (match v as v' in Vector.t _ n'
              return forall pf : n' = 0,
                eq_rect n' (Vector.t A) v' 0 pf = v ->
                P v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end erefl erefl).
    (* forall pf : 0 = 0, eq_rect 0 (Vector.t A) (Vector.nil A) 0 pf = v -> P v *)
    move=> pf.
    rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
    move=> <-.
    by [].
  (* forall pf : n.+1 = 0,
     eq_rect n.+1 (Vector.t A) (Vector.cons A a n t) 0 pf = v -> P v *)
  by [].
Qed.

Definition my_caseS' :
    forall {A : Type} {n : nat} (v : Vector.t A n.+1)
    (P : Vector.t A n.+1 -> Type),
    (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
  move=> A n v P H.
  refine (match v as v' in Vector.t _ n'
              return forall pf : n' = n.+1,
                eq_rect n' (Vector.t A) v' n.+1 pf = v ->
                P v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end erefl erefl).
    (* forall pf : 0 = n.+1, eq_rect 0 (Vector.t A) (Vector.nil A) n.+1 pf = v -> P v *)
    by [].
  (* forall pf : n0.+1 = n.+1,
     eq_rect n0.+1 (Vector.t A) (Vector.cons A a n0 t) n.+1 pf = v -> P v *)
  move=> pf.
  move: (pf).
  case: pf => pf.
  rewrite {}pf in v P H t *.
  move=> pf.
  rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
  by move=> <-.
Qed.

とくに迷うところはない。

さて、Vector.t については、べつに eq_rect を使わなくても証明できるので、必要ないともいえる。試行錯誤が必要なく、迷わずに証明できるだけでも便利だけど。

しかし、インデックス付き帰納型でも、eq や le については (たぶん) eq_rect が必要になる。

eq と le は Coq 標準の帰納型で、それぞれ、任意の型の値の等価性および、nat の「<=」を表現し、以下のように定義されている。 (ただし、SSReflect では mathcomp.ssreflect.eqtype.eq_refl でこのコンストラクタの eq_refl は隠されているので、erefl で参照する)

Inductive eq (A : Type) (x : A) : A -> Prop :=
| eq_refl : x = x.

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n m.+1.

あらためてみると、eq_refl と le_n はパラメータとインデックスに同じものを指定していて、同じ形だな。ということは、le は eq 以上に難しそうである。

eq_rect を使って、eq と le の場合分けの補題を証明してみよう。

eq の場合分けは、eq にはコンストラクタが erefl のひとつしかないので、 eq x y 型の式 e があったら、じつは x と y は等しくて、e は erefl で作られている、というわけで、いろいろな事情を無視すると P (erefl x) -> P e という補題を作りたい。

しかし、P は x = y -> Prop 型なのに erefl x は x = x 型なので型が合わない。というわけで、型を合わせるために (forall (pf : x = y), P (eq_rect x (eq x) erefl y pf)) -> P e としよう。

あとは e はなんでもいいので forall をつけて、ぜんぶ型をつけると、この補題は以下のように証明できる。

Lemma eq_case :
  forall (T : Type) (x y : T) (P : x = y -> Prop),
    (forall (pf : x = y), P (eq_rect x (eq x) erefl y pf)) ->
    (forall e, P e).
Proof.
  move=> T x y P H e.
  refine (match e as e' in _ = y'
              return forall pf : y' = y,
                       eq_rect y' (eq x) e' y pf = e ->
                       P e with
          | erefl => _
        end erefl erefl).
  move=> pf <-.
  by apply H.
Defined.

ここでは eq_rect を除去する Eqdep_dec.eq_rect_eq_dec は使っていない。それはこの補題を使う側の役割である。 (また、eq_rect_eq_dec は、この補題を使うと出てくる pf : x = y を使って、x と y のどちらかを消してから使うのだが、そのときに、コンテキストに含まれる x と y (のどちらか) も同様に消してから使う必要があるので、補題の中で使うわけにはいかないのである。上の my_caseS' では、rewrite {}pf in v P H t * がその除去を行っている。)

le の場合分けも同様に証明できる。 le_n は eq_refl に似ていて、le_S は Vector.cons に似ている。

Lemma le_case :
  forall a b (P : le a b -> Prop),
    (forall (pf : a = b), P (eq_rect a (le a) (le_n a) b pf)) ->
    (forall b' (pf : b'.+1 = b) (x : le a b'), P (eq_rect b'.+1 (le a) (le_S a b' x) b pf)) ->
    (forall x, P x).
Proof.
  move=> a b P H1 H2 x.
  refine (match x as x' in le _ b'
                return forall pf : b' = b,
                         eq_rect b' (le a) x' b pf = x ->
                         P x with
            | le_n  => _
            | le_S b' le_ab' => _
          end erefl erefl).
    move=> pf <-.
    by exact (H1 pf).
  move=> pf <-.
  by exact (H2 b' pf le_ab').
Defined.

#7 eq_irrelevance

eq と le の場合分けの補題を証明したが、これはどんな状況で必要になるのだろうか。

そもそも一般的に、証明が具体的にどう構成されているかは気にするべきでない (そんなことに依存すべきでない) ことになっている。そういう理念なので、Coq の証明 (Qed で終わるもの) は展開できない。

しかし、証明を値に埋め込むと、値の等価性は証明の等価性に依存することになる。証明が埋め込まれた値の例としては、SSReflect の tuple がある。 tuple は、レコードとして以下のように定義されている。

Record tuple_of (n : nat) (T : Type) : Type := Tuple
  { tval : seq T;  _ : is_true (size tval == n) }.

このレコードにはふたつの要素があり、ひとつは T型のリスト (seq T) であり、もうひとつはそのリストのサイズが n であるという証明 (is_true (size tval == n)) である。前者には tval という名前が付いているが、後者には名前が付いていない。なお、Tuple というのがコンストラクタである。

このように証明を値のなかに入れることで、Vector と同様に、型で長さを指定したリストを表現できる。 (そして、インデックス付き帰納型を使わずに済む)

ただここで、tuple の等価性を項の等価性 t1 = t2 で扱おうとすると、項の等価性は同じコンストラクタと同じ引数で作ったものは等しいというものなので、 Tuple s1 p1 = Tuple s2 p2 であり、リスト s1 と s2 が等しく、さらに証明 p1 と p2 が等しい、ということになる。

ここで、is_true (size tval == n) というひとつの命題に対して複数の証明があると、長さ n のリストで、リストの内容が等しいのに証明が等しくないばかりにタプルとして等しいとはいえないということが起きてしまう。

そこで重要なのが、証明の唯一性である。じつは、is_true (size tval == n) という命題に対して、証明はひとつしかないのである。そのため、リストの内容が等しいのと、タプルとして等しいのは、等価になる。

これはなんでかというと、is_true b は b = true と定義されており、eq の証明は (コンストラクタが eq_refl しかなく、あと再帰的でもないので) ひとつしかないからである。そのため、実際の証明項は複雑かもしれないが、証明項を簡約していけば eq_refl になるはずである。 (しかし、Qed で終わった証明は展開できないので、この簡約は進められないことがほとんどではある。)

そのような証明の唯一性は、SSReflect では eq_irrelevance という定理で証明されている。

eq_irrelevance : forall [T : eqType] [x y : T] (e1 e2 : x = y), e1 = e2

ここで、T : eqType となっていることにより、T が decidable equality をもつことが保証される。 (Eqdep_dec.eq_rect_eq_dec を使うには decidable equality が必要だったことを思い出そう)

この eq_irrelevance を自前で証明してみよう。もちろん、eq_case を使うわけである。

まず、eqType に対する decidable equality が必要なので、それを eqtype_dec として証明しておく。

Lemma eqtype_dec (T : eqType) (x y : T) : {x = y} + {x <> y}.
Proof.
  by case: (boolP (x == y)) => /eqP H; [left|right].
Qed.

あとは、e1 = e2 で、e1 について (eq_case で) 場合分けして、e2 について (これも eq_case で) 場合分けすれば、ゴールが erefl y = erefl y になって、自明に証明できるようになる。

Lemma my_eq_irrelevance : forall [T : eqType] [x y : T] (e1 e2 : x = y), e1 = e2.
Proof.
  move=> T x y e1 e2.
  pattern e1.
  apply eq_case.
  move=> pf.
  move: (pf).
  rewrite {}pf in e1 e2 *.
  move=> pf.
  rewrite -(Eqdep_dec.eq_rect_eq_dec (eqtype_dec T)).
  clear e1 pf.
  pattern e2.
  apply eq_case.
  move=> pf.
  rewrite -(Eqdep_dec.eq_rect_eq_dec (eqtype_dec T)).
  by [].
Qed.

#8 le の証明の唯一性

le の証明の唯一性も証明してみよう。もちろん、le_case を使う。

Lemma le_irrelevance a b (p1 p2 : le a b) : p1 = p2.
Proof.
  move: a b p1 p2.
  fix IH 3.
  move=> a b p1 p2.
  pattern p1.
  apply le_case.
    clear IH.
    move=> pf.
    move: (pf).
    rewrite {}pf in p1 p2 *.
    move=> pf.
    rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
    clear a p1 pf.
    pattern p2.
    apply le_case.
      move=> pf.
      rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
      by [].
    clear p2.
    move=> b' pf p2.
    exfalso.
    move: p2 => /leP.
    rewrite -{}pf.
    by rewrite ltnn.
  clear p1.
  move=> b' pf p1.
  move: (pf).
  rewrite -{}pf in p1 p2 *.
  move=> pf.
  pattern p2.
  apply le_case.
    clear IH.
    move=> pf1.
    exfalso.
    clear b p2 pf.
    move: p1 => /leP.
    rewrite pf1.
    by rewrite ltnn.
  rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
  clear pf p2.
  move=> b'' pf p2.
  move: (pf).
  case: pf => pf.
  rewrite pf in p2 *.
  clear b'' pf.
  move=> pf.
  rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
  congr (le_S a b' _).
  apply IH.
Qed.

だいたい問題はないのだが、 fix tactic を使って帰納法をしていて、意図せず IH が使われてしまうと Recursive definition of IH is ill-formed. というエラーになってしまうので、 IH を使わないところでは明示的に clear IH で消しておく必要があった。

なお、The Coq FAQ にも le の証明の唯一性の証明は載っていて、ここでも eq_rect を使っている。

The Coq FAQ: Case Studies: How to prove that two proofs of n <= m on nat are equal?

#9 Vector と tuple

さて、不幸を避けるためには、Vector ではなく SSReflect の tuple を使うのが良いのだが、これらが同じ表現能力を持っていることを証明してみよう。

From mathcomp Require Import all_ssreflect.
Require Vector.

Print Vector.t.
(*
Inductive t (A : Type) : nat -> Type :=
    nil : Vector.t A 0
  | cons : A -> forall n : nat, Vector.t A n -> Vector.t A n.+1.
*)
(* arity が nat -> Type となので、インデックス付き帰納型である。 *)

Print Tuple.
(*
Record tuple_of (n : nat) (T : Type) : Type := Tuple
  { tval : seq T;  _ : is_true (@size T tval == n) }.
*)
(* arity が Type なのでインデックス付き帰納型ではない。 *)

(* Vector.nil と [tuple] が対応する *)
About Vector.nil. (* forall A : Type, Vector.t A 0 *)
Check [tuple]. (* [tuple] : 0.-tuple ?T *)

About Vector.cons. (* forall A : Type, A -> forall n : nat, Vector.t A n -> Vector.t A n.+1 *)

(* Vector.cons に対応する tuple 版の関数はなさそうなので、ここで定義する *)
(* なお、SSReflect の leq (<=) が減算で定義されていることにより、
   m.+1 <= n.+1 の証明は m <= n の証明と同じなので、証明をそのまま利用できる *)
Definition tcons {n : nat} {T : Type} (h : T) (t : n.-tuple T) : n.+1.-tuple T.
  case: t => s H.
  by exact (@Tuple n.+1 T (h :: s) H).
Defined.

About Vector.t_rect.
(*
Vector.t_rect :
forall (A : Type) (P : forall n : nat, Vector.t A n -> Type),
P 0 (Vector.nil A) ->
(forall (h : A) (n : nat) (t : Vector.t A n),
 P n t -> P n.+1 (Vector.cons A h n t)) ->
forall (n : nat) (t : Vector.t A n), P n t
*)

Definition tuple_of_vector : forall {n : nat} {T : Type} (v : Vector.t T n), n.-tuple T.
  move=> n T v.
  pattern n, v.
  apply Vector.t_rect.
    by exact [tuple].
  clear n v.
  move=> h n v t.
  by exact (tcons h t).
Defined.

Definition vector_of_tuple : forall {n : nat} {T : Type} (t : n.-tuple T), Vector.t T n.
  move=> n T [] s H.
  elim/nat_rect: n s H.
    move=> _ _.
    by exact (Vector.nil T).
  move=> n IH [].
    by [].
  move=> h s /=.
  change ((size s).+1 == n.+1) with ((size s) == n).
  move=> H.
  apply (Vector.cons T h _).
  by exact (IH s H).
Defined.

Lemma tuple_of_vector_cons (n : nat) (T : Type) (h : T) (v : Vector.t T n) :
  tuple_of_vector (Vector.cons T h n v) =
  tcons h (tuple_of_vector v).
Proof.
  by [].
Qed.

Lemma vector_of_tuple_cons (n : nat) (T : Type) (h : T) (t : n.-tuple T) :
  vector_of_tuple (tcons h t) =
  Vector.cons T h n (vector_of_tuple t).
Proof.
  by case: t.
Qed.

Lemma vector_of_tuple_of_vector (n : nat) (T : Type) (v : Vector.t T n) :
  vector_of_tuple (tuple_of_vector v) = v.
Proof.
  pattern n, v.
  apply Vector.t_rect.
    by [].
  clear n v.
  move=> h n t IH.
  rewrite tuple_of_vector_cons.
  rewrite vector_of_tuple_cons.
  by rewrite IH.
Qed.

Lemma vector_of_tuple_Tuple_cons (n : nat) (T : Type) (h : T) (s : seq T) H :
  vector_of_tuple (Tuple (n:=n.+1) (tval:=h :: s) H) =
  Vector.cons T h n (vector_of_tuple (Tuple (n:=n) (tval:=s) H)).
Proof.
  by [].
Qed.

Lemma tuple_of_vector_of_tuple (n : nat) (T : Type) (t : n.-tuple T) :
  tuple_of_vector (vector_of_tuple t) = t.
Proof.
  case: t => s H.
  elim/nat_rect: n s H.
    simpl.
    move=> s H.
    move: (size0nil (elimT eqP H)) => s0.
    rewrite {}s0 in H *.
    rewrite /tuple /=.
    congr (Tuple _).
    by apply eq_irrelevance.
  move=> n IH [].
    by [].
  move=> h s H.
  change (size (h :: s) == n.+1) with (size s == n) in H.
  rewrite vector_of_tuple_Tuple_cons.
  rewrite tuple_of_vector_cons.
  by rewrite IH.
Qed.

Lemma vector_of_tupleK n T : cancel (@vector_of_tuple n T) (@tuple_of_vector n T).
Proof.
  move=> t.
  by rewrite tuple_of_vector_of_tuple.
Qed.

Lemma tuple_of_vectorK n T : cancel (@tuple_of_vector n T) (@vector_of_tuple n T).
Proof.
  move=> v.
  by rewrite vector_of_tuple_of_vector.
Qed.

Lemma vector_of_tuple_bij n T : bijective (@vector_of_tuple n T).
Proof.
  apply (Bijective (vector_of_tupleK n T)).
  by apply tuple_of_vectorK.
Qed.

Lemma tuple_of_vector_bij n T : bijective (@tuple_of_vector n T).
Proof.
  apply (Bijective (tuple_of_vectorK n T)).
  by apply vector_of_tupleK.
Qed.

変換関数 vector_of_tuple と tuple_of_vector を定義し、 vector_of_tuple (tuple_of_vector v) = v と tuple_of_vector (vector_of_tuple t) = t が証明できたので、Vector と tuple はどっちも同じ表現能力を持つことが確認できた。

#10 Fin と fintype

有限集合を表現する Fin と fintype がある。前者は Coq 標準ライブラリにあり、後者は SSReflect で提供される。

Fin は Coq.Vectors.Fin という階層なので、Vector といっしょに提供されているのだと思う。

n個の要素をもつ型として、 Fin では Fin.t n という型を利用でき、 fintype では 'I_n という型を利用できる。 n は nat である。

これらが同じ表現能力を持っていることを証明してみよう。

From mathcomp Require Import all_ssreflect.
Require Fin.

Print Fin.t.
(*
Inductive t : nat -> Set :=
    F1 : forall n : nat, Fin.t n.+1
  | FS : forall n : nat, Fin.t n -> Fin.t n.+1.
*)
(* arity が nat -> Set となので、インデックス付き帰納型である。 *)

Print ordinal.
(*
Inductive ordinal (n : nat) : predArgType :=
    Ordinal : forall m : nat, m < n -> 'I_n.
*)
Print predArgType.
(* predArgType = Type
     : Type *)

(* arity が predArgType つまり Type なので、インデックス付き帰納型ではない。 *)

(* Fin.F1 と ord0 が対応する *)
About Fin.F1. (* Fin.F1 : forall {n : nat}, Fin.t n.+1 *)
About ord0. (* ord0 : forall {n' : nat}, 'I_n'.+1 *)

About Fin.FS. (* Fin.FS : forall {n : nat}, Fin.t n -> Fin.t n.+1 *)

(* Fin.FS に対応する fintype の関数として、ordinalS を定義する *)
(* 証明 pf をそのまま使えるのは tcons と同様 *)
Definition ordinalS {n : nat} (i : 'I_n) : 'I_n.+1 :=
  let: Ordinal m pf := i in @Ordinal n.+1 m.+1 pf.

About Fin.t_rect.
(*
Fin.t_rect :
forall P : forall n : nat, Fin.t n -> Type,
(forall n : nat, P n.+1 (@Fin.F1 n)) ->
(forall (n : nat) (t : Fin.t n), P n t -> P n.+1 (@Fin.FS n t)) ->
forall (n : nat) (t : Fin.t n), P n t
*)

Definition ord_of_fin : forall {n : nat} (f : Fin.t n), 'I_n.
  apply Fin.t_rect.
    by exact @ord0.
  move=> n f IH.
  by exact (ordinalS IH).
Defined.

Definition fin_of_ord : forall {n : nat} (i : 'I_n), Fin.t n.
  case; first by case.
  move=> n [] m.
  elim/nat_rect: m n.
    move=> n _.
    by exact Fin.F1.
  move=> n IH [].
    by [].
  move=> m H.
  apply Fin.FS.
  by exact (IH m H).
Defined.

Lemma ord_of_fin_FS (n : nat) (f : Fin.t n) :
  (@ord_of_fin n.+1 (@Fin.FS n f)) =
  @ordinalS n (@ord_of_fin n f).
Proof.
  by [].
Qed.

Lemma fin_of_ord_ordinalS (n : nat) (i : 'I_n) :
  (@fin_of_ord n.+1 (@ordinalS n i)) =
  @Fin.FS n (@fin_of_ord n i).
Proof.
  case: i.
  by case: n.
Qed.

Lemma fin_of_ord_of_fin (n : nat) (f : Fin.t n) : fin_of_ord (ord_of_fin f) = f.
Proof.
  pattern n, f.
  apply Fin.t_rect.
    by [].
  clear n f.
  move=> n f IH.
  rewrite ord_of_fin_FS.
  rewrite fin_of_ord_ordinalS.
  by rewrite IH.
Qed.

Lemma fin_of_ord_S (m p : nat) (H : m.+1 < (m + p).+2) :
  @fin_of_ord (m + p).+2 (@Ordinal (m + p).+2 m.+1 H) =
  Fin.FS (@fin_of_ord (m + p).+1 (@Ordinal (m + p).+1 m H)).
Proof.
  by [].
Qed.

Lemma ord_of_fin_of_ord (n : nat) (i : 'I_n) : ord_of_fin (fin_of_ord i) = i.
Proof.
  case: i => m H.
  set p := n - m.+1.
  move: (H).
  rewrite (_ : n = m.+1 + p); last first.
    by rewrite /p subnKC.
  change (m.+1 + p) with (m + p).+1.
  move: p => p {}H {n}.
  change (is_true (m <= m + p)) in H.
  elim: m H.
    simpl.
    move=> H.
    change (0 + p) with p.
    rewrite /ord0.
    congr (@Ordinal p.+1 0 _).
    by apply eq_irrelevance.
  move=> m.
  change (m.+1 + p) with (m + p).+1.
  change (m < (m + p).+1) with (m <= m + p).
  move=> IH H.
  rewrite fin_of_ord_S.
  rewrite ord_of_fin_FS.
  rewrite IH.
  by [].
Qed.

Lemma fin_of_ordK n : cancel (@fin_of_ord n) (@ord_of_fin n).
Proof.
  move=> i.
  by rewrite ord_of_fin_of_ord.
Qed.

Lemma ord_of_finK n : cancel (@ord_of_fin n) (@fin_of_ord n).
Proof.
  move=> f.
  by rewrite fin_of_ord_of_fin.
Qed.

Lemma fin_of_ord_bij n : bijective (@fin_of_ord n).
Proof.
  apply (Bijective (fin_of_ordK n)).
  by apply ord_of_finK.
Qed.

Lemma ord_of_fin_bij n : bijective (@ord_of_fin n).
Proof.
  apply (Bijective (ord_of_finK n)).
  by apply fin_of_ordK.
Qed.

変換関数 fin_of_ord と ord_of_fin を定義し、 fin_of_ord (ord_of_fin f) = f と ord_of_fin (fin_of_ord i) = i を証明できたので、Fin と fintype の表現能力が同じと確認できた。

#11 公理は必要なのか?

Eqdep_dec.eq_rect_eq_dec はインデックスに decidable equality があれば使えるので、その条件が満たされれば公理は必要なさそうである。

公理が必要になるのは、インデックスに decidable equality がない場合、ということは、型をインデックスに使った場合とかだろうか。

#12 インデックス付き帰納型の場合分けが必要になることはあるか?

ここまでいろいろ証明しつつ考えたのだが、そもそも、インデックス付き帰納型の場合分けを実際に使う機会はあるだろうか?

(extraction で残る) 値と、(extraction で消える) 証明それぞれに分けて考えよう。

(extraction で残る) 値で、インデックス付き帰納型の例は、Vector.t と Fin.t である。標準ライブラリを眺めた限りでは、他にはないと思う。しかし、これらよりは、同じ表現能力を持つ tuple と fintype を使った方がよい。したがって、インデックス付き帰納型を使う必要は無く、インデックス付き帰納型の場合分けも不要である。

(extraction で消える) 証明で、インデックス付き帰納型の例は、eq, le などがある。こちらは他にもたくさんある。(Coq の標準ライブラリの Inductive Index を眺めてみた。) しかし、証明の中身を調べる必要は基本的にはない。例外的に証明の唯一性が必要になるが、 (インデックスが eqType の場合の eq の) 証明の唯一性は、eq_irrelevance が提供されているので、自分で証明する必要は無い。ということで、こちらの場合でもインデックス付き帰納型の場合分けを使う機会はないと思う。

ということは、インデックス付き帰納型の場合分けというのは、結局使う機会はないような...

どうしても必要になるのは、Vector.t と Fin.t 以外のインデックス付き帰納型を自前で定義するかどこかで定義されていたのを使う場合?

あとは、eq では表現できない述語をインデックス付き帰納型を定義した場合?

#13 dependent destruction とかの説明

マニュアルのなかで、dependent destruction とかの説明を探すと、個々の tactic の説明の他に、例がいくつか載っているようだ。

Coq Manual: Examples of dependent destruction / dependent induction

公理の話は少ししか触れていない気がする。

#14 わからないこと

Vector.t や Fin.t の場合分けの補題は eq_rect を使わなくても証明できるのに、 eq や le の場合分けの補題はできないのか、どういう条件で可能なのか、はっきりとはわからない。

追記: SSReflect の eq_irrelevance の証明を読んだところ、eq_rect を使わずに証明されていたので、eq の場合分けも不可能ではないのだと思う。

天泣記

2024-05-07 (Tue)