参考にしたもの
同時機能的定義
例として，可変個の子供を持つ木を考える．Inductive を with でつなげる．
Inductive tree : Set :=
| node : nat -> forest -> tree
with forest : Set :=
| leaf : forest
| cons : tree -> forest -> forest.
帰納的に関数を定義する場合も，Fixpoint を with でつなげる．たとえばノードの数を数える場合
Fixpoint numnodes (t:tree) : nat :=
match t with
| node n f1 => 1 + numnodes_f f1
end
with numnodes_f (f:forest) : nat :=
match f with
| leaf => 0
| cons t1 f1 => numnodes t1 + numnodes_f f1
end.
さて，帰納法による証明だが，とりあえず2つくらい方法がある．
最初は，この定義による帰納法．
一般に，induction x. とすると，xの型をTとして，T_ind が用いられる．
(これは Prop の場合．goalの型によって T_rec (Set) だったり T_rect (Type) だったり
するのであろう．)
ところが，上の例だと，tree_ind とか forest_ind とか作られているのだけれど，あまり
役に立たない．たとえば tree_ind の型は，つぎのようなもの．
forall P : tree -> Prop,
(forall (n : nat) (f : forest), P (node n f)) -> forall t : tree, P t
ちゃんと同時帰納法に対応するものがほしい．
これは，Scheme という命令で生成することができる．
Scheme tree_forest_ind := Induction for tree Sort Prop
with forest_tree_ind := Induction for forest Sort Prop.
tree_forest_ind は，以下の型を持つ
forall (P : tree -> Prop) (P0 : forest -> Prop),
(forall (n : nat) (f : forest), P0 f -> P (node n f)) ->
P0 leaf ->
(forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1)) ->
forall t : tree, P t
これなら使える．使う時には induction に using でこれを指定する．
induction t using tree_forest_ind.
実際には，この例だと P0 がなにになるか Coq には不明なので，einduction を使うことになる.
もうひとつの方法は，証明すべき定理の方も両者同時に進行させること．
たとえば，同様に「高さ」も定義して，高さよりもノードの数の方が等しいか大きいという
ことを証明したいとしよう．定理を with でつないで次のように書く．
Lemma lem1t: forall t, height t <= numnodes t
with lem1f: forall f, height_f f <= numnodes_f f.
これで，induction t とすると，次のようになる．
2 subgoals, subgoal 1 (ID 77)
lem1t : forall t : tree, height t <= numnodes t
lem1f : forall f : forest, height_f f <= numnodes_f f
n : nat
f : forest
============================
height (node n f) <= numnodes (node n f)
subgoal 2 (ID 72) is:
forall f : forest, height_f f <= numnodes_f f
当然というか何というか，ここで apply lem1t; apply lem1f. Qed. ではいけない．
さいごの Qed で怒られる．
ちゃんと一つ前に進んで，lem1t や lem1f を帰納法の仮定として適用して良いところで
適用すれば，証明が完了する．
全体のソースコードを示す．
Require Import Arith.
Inductive tree : Set :=
| node : nat -> forest -> tree
with forest : Set :=
| leaf : forest
| cons : tree -> forest -> forest.
Check tree_ind.
Fixpoint numnodes (t:tree) : nat :=
match t with
| node n f1 => 1 + numnodes_f f1
end
with numnodes_f (f:forest) : nat :=
match f with
| leaf => 0
| cons t1 f1 => numnodes t1 + numnodes_f f1
end.
Fixpoint height (t:tree) : nat :=
match t with
| node n f1 => 1 + height_f f1
end
with height_f (f:forest) : nat :=
match f with
| leaf => 0
| cons t1 f1 => max (height t1) (height_f f1)
end.
(* le_S_n: forall n m : nat, S n <= S m -> n <= m *)
(* le_n_S: forall n m : nat, n <= m -> S n <= S m *)
(* le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p *)
Lemma max_le_plus: forall x y, max x y <= x + y.
Proof.
admit.
Qed.
Lemma monotone_plus:
forall x1 y1 x2 y2, x1 <= x2 -> y1 <= y2 -> x1 + y1 <= x2 + y2.
Proof.
admit.
Qed.
(* From here, we can proceed (1) as follows *)
Scheme tree_forest_ind := Induction for tree Sort Prop
with forest_tree_ind := Induction for forest Sort Prop.
(* This command generates the following induction scheme.
tree_forest_ind
: forall (P : tree -> Prop) (P0 : forest -> Prop),
(forall (n : nat) (f : forest), P0 f -> P (node n f)) ->
P0 leaf ->
(forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1)) ->
forall t : tree, P t
*)
Lemma lem0: forall t, height t <= numnodes t.
Proof.
einduction t using tree_forest_ind.
simpl.
apply le_n_S.
apply IHt0.
simpl; auto.
simpl in *.
eapply le_trans.
apply max_le_plus.
apply monotone_plus; auto.
Qed.
(* Or, alternatively, the following method (2) is also possible. *)
Lemma lem1t: forall t, height t <= numnodes t
with lem1f: forall f, height_f f <= numnodes_f f.
Proof.
induction t.
(* The following does not work, of course :-)
apply lem1t.
apply lem1f.
Qed.
*)
simpl.
apply le_n_S.
apply lem1f.
induction f; simpl; auto.
eapply le_trans.
apply max_le_plus.
apply monotone_plus.
apply lem1t.
apply IHf.
Qed.
keyword: simultaneous induction, simultaneous recursion, tree, variable number of children,