CoqEx15.v

Require Import Arith.

Inductive Tree : Set := | Node : list Tree -> Tree.

Require Import Max.
Require Import List.
Fixpoint depth (a : Tree) :nat :=  
match a with
| Node l => 
(fix f (l : list Tree) : nat := match l with | nil => 0 | x :: xs => max (depth x+1) (f xs) end) l end.

Lemma depth_cons : forall a : Tree, forall l : list Tree, depth (Node (a :: l)) = max (depth a+1) (depth (Node l)).
Proof.
intros.
simpl.
reflexivity.
Qed.

Definition Child (a b : Tree) : Prop := match   b with
   | Node l => In a l end.

Lemma depth_child : forall (a b :Tree), Child a b -> depth a < depth b.
Proof.
intros.
destruct b.
simpl in H.
induction l.
apply False_ind.
apply (in_nil H).
simpl in H.
destruct H.
subst.
rewrite depth_cons.
apply (lt_le_trans (depth a) (depth a + 1)).
rewrite NPeano.Nat.add_1_r.
auto.
apply le_max_l.
rewrite depth_cons.
apply (lt_le_trans (depth a) (depth (Node l))).
apply IHl.
apply H.
apply le_max_r.
Qed.

Fixpoint zip (xs ys : list Tree) : list (Tree * Tree) :=
    match xs with
        | nil => nil
        | x :: xs => match ys with
            | nil => nil
            | y :: ys => (x,y) :: zip xs ys
        end
    end.

Functional Scheme zip_rec := Induction for zip Sort Set.

Lemma Tree_dec_n : forall n : nat, forall a b : Tree, depth a < n /\ depth b < n -> {a = b} + {a <> b}.
Proof.
induction n.
intros.
destruct H.
apply left.
apply False_ind.
apply (lt_n_0 (depth a)).
apply H.

intros.
destruct H.
destruct a.
destruct b.
assert (forall (x : Tree), In x l -> depth x < n).
intros.
apply (lt_le_trans (depth x) (depth (Node l))).
apply depth_child.
unfold Child.
apply H1.
apply (lt_n_Sm_le).
apply H.

assert (forall (x : Tree), In x l0 -> depth x < n).
intros.
apply (lt_le_trans (depth x) (depth (Node l0))).
apply depth_child.
unfold Child.
apply H2.
apply (lt_n_Sm_le).
apply H0.
assert (forall (x y: Tree), In x l -> In y l0 -> {x = y} + {x <> y}).
intros.
apply IHn.
split.
apply H1.
apply H3.
apply H2.
apply H4.
assert ({ l = l0 } + { l <> l0 }).
clear H1.
clear H2.
functional induction (zip l l0).
destruct ys.
left.
reflexivity.
right.
discriminate.
right.
discriminate.
assert ({xs0 = ys0 } + {xs0 <> ys0}).
apply IHl1.
apply (le_lt_trans (depth (Node xs0)) (depth (Node (x :: xs0)))).
rewrite depth_cons.
apply le_max_r.
apply H.
apply (le_lt_trans (depth (Node ys0)) (depth (Node (y :: ys0)))).
rewrite depth_cons.
apply le_max_r.
apply H0.
intros.
apply H3.
apply in_cons.
apply H1.
apply in_cons.
apply H2.
assert ({ x = y } + { x <> y } ).
apply IHn.
split.
apply (lt_le_trans (depth x) (depth (Node (x :: xs0)))).
rewrite depth_cons.
apply (lt_le_trans (depth x) (depth x + 1)).
rewrite NPeano.Nat.add_1_r.
apply lt_n_Sn.
apply le_max_l.
apply lt_n_Sm_le.
apply H.
apply (lt_le_trans (depth y) (depth (Node (y :: ys0)))).
rewrite depth_cons.
apply (lt_le_trans (depth y) (depth y + 1)).
rewrite NPeano.Nat.add_1_r.
apply lt_n_Sn.
apply le_max_l.
apply lt_n_Sm_le.
apply H0.
destruct H2.
destruct H1.
left.
subst.
reflexivity.
right.
intro.
apply n0.
injection H1.
intros.
contradiction.
right.
intro.
injection H2.
intro.
apply n0.
destruct H4.
left.
f_equal.
apply e.
right.
intro.
apply n0.
injection H4.
trivial.
Qed.

Theorem Tree_dec: forall a b: Tree, {a = b} + {a <> b}.
Proof.
intros.
remember (depth a).
remember (depth b).
remember (S (max n n0)).
apply (Tree_dec_n n1).
split.
subst.
apply le_lt_n_Sm.
apply (le_max_l).
subst.
apply le_lt_n_Sm.
apply (le_max_r).
Qed.