RocqのInductiveで相互帰納型を作ったときの帰納法

背景

DLSなど設計していると相互帰納型がでてくることがよくあります。
例えば次のような構造の構文の言語を設計しているとします。

<statemnt> ::= 
  | "while" <expr> "{" <statement>* "}"
  | "return" <expr> ";"
  
<expr> ::=
  | <constant>
  | <variable>
  | <ident> "(" <expr> ")"  (* function application *)
  | "{" <statement>* "}"

Rocqで書くと次のような書き方になると思います。

Inductive statment :=
| While : expr -> statement list -> statement
| Return : expr -> statement
with expr :=
| Constant : nat -> expr
| Var : var -> expr
| FunCall : string -> expr -> expr
| Block : statement list -> expr.

問題点

RocqではInductive型に対して XXX_ind という名前で帰納法の原理を自動生成してくれますが、相互帰納型の場合これがうまく生成されないんです。

我々の例の場合 statement_ind という項が自動生成されるんですが、使ってみるとわかるように使い物になりません。 expr_ind も同様。

statement_ind :
   forall [P : statement -> Prop],
   (forall (e : expr) (l : seq statement), P (While e l)) ->
   (forall e : expr, P (Return e)) -> forall s : statement, P s

解決方

ではどうすればよいか。

Scheme statement_mut := Induction for statement Sort Prop
with expr_mut := Induction for expr Sort Prop.

↑これによって以下のような帰納法の原理が生成されます

statement_mut :
  forall [P : statement -> Prop] [P0 : expr -> Prop],
  (forall e : expr, P0 e -> forall l : seq statement, P (While e l)) ->
  (forall e : expr, P0 e -> P (Return e)) ->
  (forall n : nat, P0 (Constant n)) ->
  (forall v : var, P0 (Var v)) ->
  (forall (s : string) (e : expr), P0 e -> P0 (FunCall s e)) ->
  (forall l : seq statement, P0 (Block l)) -> forall s : statement, P s

参考文献

• Adam Chlipala 著 Certified Programs with Dependent Types 3.5節 Mutually Inductive Types