Coqで多重再帰のデータ構造を証明する

Coqでは一重の再帰的なデータは例えば次の様に定義できる。

Inductive list (A: Set) : Set :=
  Nil | Cons (x: A) (xs: list A).

Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。
list_indは次の様な型を持っている。

Coq < Check list_ind.
list_ind
     : forall (A : Set) (P : list A -> Prop),
       P (Nil A) ->
       (forall (x : A) (xs : list A), P xs -> P (Cons A x xs)) ->
       forall l : list A, P l

このlist_indは帰納法に関して非常に強力である。
リストを引数に持つような任意の述語Pに対して apply list_ind. をすればこのlistに関して構造的な帰納法で証明をすることができる。
また、そのための特別な induction という tactic さえ用意されている。

ただし、この *_ind は多重再帰のデータ型に関してはしょぼい物になってしまうという問題を発見した。*1

多重再帰のデータ型とは例えば相互再帰になっているものや次の様に再帰構造が入れ子になっているものだ。

module HTML.
  Inductive elem : Set :=
  | PCDATA (_: string)
  | TAG (_: list elem).

このとき先ほどと同様に elem_ind が定義されるが、それは次の型になっている。

Coq < Check elem_ind.
elem_ind
     : forall P : elem -> Prop,
       (forall s : string, P (PCDATA s)) ->
       (forall l : list elem, P (TAG l)) ->
       forall e : elem, P e

しかしこの形だとTAGの場合の帰納法の仮定で、小要素に関して帰納的に証明することができない。

この問題を解決するために以下の項を定義した。

Fixpoint elem_ind0
  (P : elem -> Prop)
  (H1 : forall s : string, P (PCDATA s))
  (H2 : P (TAG nil))
  (H3 : forall e es, P e -> P (TAG es) -> P (TAG (e :: es)))
  (e : elem) : P e
 :=
  match e as x return P x with
  | PCDATA s => H1 s
  | TAG es => list_ind (fun xs => P (TAG xs)) H2 (fun a l H => H3 a l (elem_ind0 P H1 H2 H3 a) H) es
  end.

ちょっと苦労したが、これで以下の型の項を得ることができた。これを使えばelem型の帰納法もばっちりだ。

Check elem_ind0 : forall P : elem -> Prop,
   (forall s : string, P (PCDATA s)) ->
   (P (TAG nil)) ->
   (forall e es, P e -> P (TAG es) -> P (TAG (e :: es))) ->
   forall e : elem, P e

*1:これはv8.2pl1時点の話。将来的にこの問題は改善するかもしれない。