前回のエントリと同じ気持ちを，
list を使って書いてみる．

Inductive tree : Type :=
  | node : nat -> list tree -> tree.

今回も，Coqが生成する tree_ind は役に立たない．

forall P : tree -> Prop,
       (forall (n : nat) (l : list tree), P (node n l)) ->
       forall t : tree, P t

そこで，「t1はt2の子ノード」という有基底的関係 child(t1, t2)
に関する帰納法を使ってみることにする．

Inductive child (t: tree) : tree -> Prop :=
  | child_w: forall n l, In t l -> child t (node n l).

使うためには，child が well_founded であることを証明する
必要がある．現状，この証明が汚い (下のソースを参照)．

Lemma child_well_founded: well_founded child.

ここで，well_founded (など) は，以下のように定義されている．

Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
    Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x

well_founded = 
  fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
     : forall A : Type, (A -> A -> Prop) -> Prop

これができると，次のように帰納法を使うことができる．

induction t using (well_founded_ind child_well_founded).

もっと簡単な書き方があるのかもしれないが，一応これで
動いている．
ちなみに，well_founded_ind child_well_founded は，以下の
型を持つ:

forall P : tree -> Prop,
       (forall x : tree, (forall y : tree, child y x -> P y) -> P x) ->
       forall a : tree, P a

ソース全体は以下の通り

Require Import List.
Require Import Arith.

Inductive tree : Type :=
  | node : nat -> list tree -> tree.

Definition multi_max (l:list nat) : nat := 
  fold_left (fun x y => if (le_lt_dec x y) then y else x) l 0.

Definition total (l:list nat) : nat := fold_left (fun x y => x + y) l 0.

Fixpoint height (t: tree) : nat :=
  match t with
  | node a l => (multi_max (map height l)) + 1
  end.

Fixpoint numnodes (t: tree) : nat :=
  match t with
  | node a l => (total (map numnodes l)) + 1
  end.

(* "child t1 t2" means t1 is a child of t2 *)
Inductive child (t: tree) : tree -> Prop :=
  | child_w: forall n l, In t l -> child t (node n l).

Search ((_ < S _) -> _ ) .
Lemma lt_n_Sm_lt_or_eq: forall n m : nat, n < S m -> n < m \/ n = m.
Proof. admit. Qed.

Lemma in_le_total: forall a l, In a l -> a <= total l.
Proof.  admit.  Qed.

Lemma plus_S_lt: forall x y z, x + S y = z -> x < z.
Proof.  admit.  Qed.

Lemma child_acc_n : forall n t, numnodes t < n -> Acc child t.
Proof.
  induction n; intros.
    inversion H.
  apply lt_n_Sm_lt_or_eq in H.
  destruct H.  
    apply IHn; auto.
  destruct t.
  apply Acc_intro; intros.
  apply IHn.
  simpl in H.
  assert (In (numnodes y) (map numnodes l)).
    apply in_map.
    inversion H0; auto.
  apply in_le_total in H1.
  apply plus_S_lt in H.
  eapply le_lt_trans; [apply H1|].
  trivial.
Qed.

Lemma child_well_founded: well_founded child.
Proof.
  unfold well_founded.
  intros.
  apply child_acc_n with (n:=S (numnodes a)).
  apply le_lt_n_Sm.
  apply le_refl.
Qed.


Lemma plus_monotone: 
    forall x1 y1 x2 y2, x1 <= x2 -> y1 <= y2 -> x1 + y1 <= x2 + y2.
Proof.  admit.  Qed.

Lemma plus_left_monotone: forall x y z, x <= y -> x + z <= y + z.
Proof.  admit.  Qed.

Lemma multi_max_cons x l: multi_max (x::l) = max x (multi_max l).
Proof.  admit.  Qed.

Lemma total_cons x l: total (x::l) = x + total l.
Proof.  admit.  Qed.

Lemma max_le_plus: forall x y, max x y <= x + y.
Proof.  admit.  Qed.

Lemma lem1: forall t, height t <= numnodes t.
Proof.
  induction t using (well_founded_ind child_well_founded).
  destruct t; simpl; auto.
  apply plus_left_monotone.
  generalize l H; clear l H.
  induction l; intros; simpl; auto.
  rewrite multi_max_cons, total_cons.
  eapply le_trans.
    apply max_le_plus.
  apply plus_monotone.
    apply H.
    apply child_w.
    simpl; auto.
  apply IHl.
  intros; apply H.
  apply child_w.
  right.
  inversion H0; auto.
Qed.