(* File: Trees.v  (last edited on 25/10/2000) (c) Klaus Weich  *)

Require Export My_Arith.
Require Import Le.


(******   Tree stuff  ********************************************)

Section Trees.


Variable A : Set.


Inductive Tree : Set :=
    node : A -> Forest -> Tree
with Forest : Set :=
  | Nil_Forest : Forest
  | Cons_Forest : Tree -> Forest -> Forest.


Fixpoint height_tree (t : Tree) : nat :=
  match t with
  | node a succs => S (height_forest succs)
  end
 
 with height_forest (succs : Forest) : nat :=
  match succs with
  | Nil_Forest => 0
  | Cons_Forest t0 succs => max (height_tree t0) (height_forest succs)
  end.


(*
Inductive Tree : Set :=
| node : A -> (list Tree) -> Tree.

Fixpoint height_tree [t:Tree] : nat :=
  Cases t of
  | (node a succs) => (S (height_forest succs))
  end
with height_forest[succs:(list Tree)] : nat :=
  Cases succs of
  | nil => O
  | (cons t0 succs) => (max (height_tree t0) (height_forest succs))
  end.
Does not work!!
*)


Definition root (t : Tree) := match t with
                              | node a _ => a
                              end.
Definition successors (t : Tree) := match t with
                                    | node _ succs => succs
                                    end.


Inductive In_Forest (t0 : Tree) : Forest -> Prop :=
  | in_forest_head :
      forall succs : Forest, In_Forest t0 (Cons_Forest t0 succs)
  | in_forest_tail :
      forall (t1 : Tree) (succs : Forest),
      In_Forest t0 succs -> In_Forest t0 (Cons_Forest t1 succs).


Lemma height_in_le :
 forall (t : Tree) (succs : Forest),
 In_Forest t succs -> height_tree t <= height_forest succs.                    
(* Goal: forall (t : Tree) (succs : Forest) (_ : In_Forest t succs), le (height_tree t) (height_forest succs) *)
intros t succs in_t.
(* Goal: le (height_tree t) (height_forest succs) *)
elim in_t; clear in_t succs.

(* Goal: forall succs : Forest, le (height_tree t) (height_forest (Cons_Forest t succs)) *)
(* Goal: forall (t1 : Tree) (succs : Forest) (_ : In_Forest t succs) (_ : le (height_tree t) (height_forest succs)), le (height_tree t) (height_forest (Cons_Forest t1 succs)) *)
intros succs.
(* Goal: forall (_ : In_Forest t1 (successors (node a succs))) (_ : P (root (node a succs)) i), P (root t1) i *)
simpl in |- *.
(* Goal: le (height_tree t) (max (height_tree t) (height_forest succs)) *)
(* Goal: forall (t1 : Tree) (succs : Forest) (_ : In_Forest t succs) (_ : le (height_tree t) (height_forest succs)), le (height_tree t) (height_forest (Cons_Forest t1 succs)) *)
apply le_n_max1.

(* Goal: forall (t1 : Tree) (succs : Forest) (_ : In_Forest t succs) (_ : le (height_tree t) (height_forest succs)), le (height_tree t) (height_forest (Cons_Forest t1 succs)) *)
intros t1 succs in_t le_t.
(* Goal: le (height_tree t) (height_forest (Cons_Forest t1 succs)) *)
apply le_trans with (height_forest succs).
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: forall (_ : In_Forest t1 (successors (node a succs))) (_ : P (root (node a succs)) i), P (root t1) i *)
simpl in |- *.
(* Goal: le (height_forest succs) (max (height_tree t1) (height_forest succs)) *)
apply le_n_max2.
Qed.


Lemma My_Tree_ind :
 forall P : Tree -> Prop,
 (forall (a : A) (succs : Forest),
  (forall t : Tree, In_Forest t succs -> P t) -> P (node a succs)) ->
 forall t : Tree, P t.
(* Goal: forall (P : forall _ : Tree, Set) (_ : forall (a : A) (succs : Forest) (_ : forall (t : Tree) (_ : In_Forest t succs), P t), P (node a succs)) (t : Tree), P t *)
intros P step.
(* Goal: forall t : Tree, P t *)
cut (forall (n : nat) (t : Tree), height_tree t <= n -> P t).
(* Goal: forall (_ : forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree), P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intro claim.
(* Goal: forall t : Tree, P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intro t.
(* Goal: P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
apply claim with (height_tree t).
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intros n; elim n; clear n.

(* Goal: forall (t : Tree) (_ : le (height_tree t) O), P t *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
intros t; elim t; clear t.
(* Goal: forall (a : A) (f : Forest) (_ : le (height_tree (node a f)) (S n)), P (node a f) *)
intros a succs u0.
(* Goal: P (node a succs) *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
inversion_clear u0.

(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
intros n ih t.
(* Goal: forall _ : le (height_tree t) (S n), P t *)
elim t; clear t.
(* Goal: forall (a : A) (f : Forest) (_ : le (height_tree (node a f)) (S n)), P (node a f) *)
intros a succs u0.
(* Goal: P (node a succs) *)
apply step; clear step.
(* Goal: forall (t : Tree) (_ : In_Forest t succs), P t *)
intros t in_t.
(* Goal: P t *)
apply ih; clear ih P.
(* Goal: le (height_tree t) n *)
apply le_S_n.
(* Goal: le (S (height_tree t)) (S n) *)
apply le_trans with (S (height_forest succs)).
(* Goal: le (S (height_tree t)) (S (height_forest succs)) *)
(* Goal: le (S (height_forest succs)) (S n) *)
apply le_n_S.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
apply height_in_le; assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
Qed.


Lemma My_Tree_rec :
 forall P : Tree -> Set,
 (forall (a : A) (succs : Forest),
  (forall t : Tree, In_Forest t succs -> P t) -> P (node a succs)) ->
 forall t : Tree, P t.
(* Goal: forall (P : forall _ : Tree, Set) (_ : forall (a : A) (succs : Forest) (_ : forall (t : Tree) (_ : In_Forest t succs), P t), P (node a succs)) (t : Tree), P t *)
intros P step.
(* Goal: forall t : Tree, P t *)
cut (forall (n : nat) (t : Tree), height_tree t <= n -> P t).
(* Goal: forall (_ : forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree), P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intro claim.
(* Goal: forall t : Tree, P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intro t.
(* Goal: P t *)
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
apply claim with (height_tree t).
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.
(* Goal: forall (n : nat) (t : Tree) (_ : le (height_tree t) n), P t *)
intros n; elim n; clear n.

(* Goal: forall (t : Tree) (_ : le (height_tree t) O), P t *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
intros t; elim t; clear t.
(* Goal: forall (a : A) (f : Forest) (_ : le (height_tree (node a f)) (S n)), P (node a f) *)
intros a succs u0.
(* Goal: P (node a succs) *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
inversion_clear u0.

(* Goal: forall (n : nat) (_ : forall (t : Tree) (_ : le (height_tree t) n), P t) (t : Tree) (_ : le (height_tree t) (S n)), P t *)
intros n ih t.
(* Goal: forall _ : le (height_tree t) (S n), P t *)
elim t; clear t.
(* Goal: forall (a : A) (f : Forest) (_ : le (height_tree (node a f)) (S n)), P (node a f) *)
intros a succs u0.
(* Goal: P (node a succs) *)
apply step; clear step.
(* Goal: forall (t : Tree) (_ : In_Forest t succs), P t *)
intros t in_t.
(* Goal: P t *)
apply ih; clear ih P.
(* Goal: le (height_tree t) n *)
apply le_S_n.
(* Goal: le (S (height_tree t)) (S n) *)
apply le_trans with (S (height_forest succs)).
(* Goal: le (S (height_tree t)) (S (height_forest succs)) *)
(* Goal: le (S (height_forest succs)) (S n) *)
apply le_n_S.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
apply height_in_le; assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
Qed.


(* Successor relation  *)

Inductive Successor : Tree -> Tree -> Prop :=
  | successor_refl : forall t : Tree, Successor t t
  | successor_trans :
      forall t0 t1 : Tree,
      In_Forest t1 (successors t0) ->
      forall t2 : Tree, Successor t2 t1 -> Successor t2 t0.


Lemma succs_trans :
 forall t1 t2 : Tree,
 Successor t2 t1 -> forall t0 : Tree, Successor t1 t0 -> Successor t2 t0.
(* Goal: forall (t1 t2 : Tree) (_ : Successor t2 t1) (t0 : Tree) (_ : Successor t1 t0), Successor t2 t0 *)
intros t1 t2 u0 t0 u1.
(* Goal: Successor t2 t0 *)
generalize u0; clear u0.
(* Goal: forall _ : Successor t2 t1, Successor t2 t0 *)
elim u1; clear u1 t0 t1.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.

(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t3 : Tree) (_ : Successor t3 t1) (_ : forall _ : Successor t2 t3, Successor t2 t1) (_ : Successor t2 t3), Successor t2 t0 *)
intros t0 t1 in_t1 t3 suc_t3_t1 ih suc_t2_t3.
(* Goal: Successor t2 t0 *)
apply (successor_trans t0 t1 in_t1 t2).
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
apply ih; assumption.
Qed.


Lemma succs_refl : forall t : Tree, Successor t t.
(* Goal: forall _ : forall (t : Tree) (_ : In_Forest t Nil_Forest), P t, P (node a Nil_Forest) *)
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (t0 : Tree) (_ : In_Forest t0 (Cons_Forest t f)), P t0), P (node a (Cons_Forest t f)) *)
intros.
(* Goal: Successor t1 t1 *)
(* Goal: P (root t1) i *)
apply successor_refl.
Qed.



Lemma Succs_Tree_ind :
 forall P : Tree -> Prop,
 (forall a : A, P (node a Nil_Forest)) ->
 (forall t0 t1 : Tree, Successor t0 t1 -> P t0 -> P t1) ->
 forall t : Tree, P t.
(* Goal: forall (P : forall _ : Tree, Prop) (_ : forall a : A, P (node a Nil_Forest)) (_ : forall (t0 t1 : Tree) (_ : Successor t0 t1) (_ : P t0), P t1) (t : Tree), P t *)
intros P leaf step t.
(* Goal: P t *)
apply My_Tree_ind.
(* Goal: forall (a : A) (succs : Forest) (_ : forall (t : Tree) (_ : In_Forest t succs), P t), P (node a succs) *)
intros a succs; case succs; clear succs. 
(* Goal: forall _ : forall (t : Tree) (_ : In_Forest t Nil_Forest), P t, P (node a Nil_Forest) *)
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (t0 : Tree) (_ : In_Forest t0 (Cons_Forest t f)), P t0), P (node a (Cons_Forest t f)) *)
intros.
(* Goal: P (node a Nil_Forest) *)
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (t0 : Tree) (_ : In_Forest t0 (Cons_Forest t f)), P t0), P (node a (Cons_Forest t f)) *)
apply leaf.
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (t0 : Tree) (_ : In_Forest t0 (Cons_Forest t f)), P t0), P (node a (Cons_Forest t f)) *)
intros t0 succs ih.
(* Goal: P (node a (Cons_Forest t0 succs)) *)
apply step with t0.
(* Goal: Successor t0 (node a (Cons_Forest t0 succs)) *)
(* Goal: P t0 *)
apply successor_trans with t0.
(* Goal: forall (_ : In_Forest t1 (successors (node a succs))) (_ : P (root (node a succs)) i), P (root t1) i *)
simpl in |- *.
(* Goal: In_Forest t0 (Cons_Forest t0 succs) *)
apply in_forest_head.
(* Goal: Successor t1 t1 *)
(* Goal: P (root t1) i *)
apply successor_refl.
(* Goal: P (root t1) i *)
apply ih.
(* Goal: In_Forest t0 (Cons_Forest t0 succs) *)
apply in_forest_head.
Qed.


(* In_tree *)
(* ------- *)

Inductive In_tree : A -> Tree -> Prop :=
  | in_leave : forall (a : A) (succs : Forest), In_tree a (node a succs)
  | in_succs :
      forall (succs : Forest) (t : Tree),
      In_Forest t succs ->
      forall a : A, In_tree a t -> forall a' : A, In_tree a (node a' succs).


Lemma in_successor_in :
 forall (a : A) (t : Tree),
 In_tree a t -> forall t' : Tree, Successor t t' -> In_tree a t'.
(* Goal: forall (a : A) (t : Tree) (_ : In_tree a t) (t' : Tree) (_ : Successor t t'), In_tree a t' *)
intros a t in_t t' suc.
(* Goal: In_tree a t' *)
generalize in_t; clear in_t.
(* Goal: forall _ : In_tree a t, In_tree a t' *)
elim suc; clear suc.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall _ : In_tree a t2, In_tree a t1) (_ : In_tree a t2), In_tree a t0 *)
clear t t'.
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall _ : In_tree a t2, In_tree a t1) (_ : In_tree a t2), In_tree a t0 *)
intros t0 t1 in_t1 t2 suc_t2 ih in_t2.
(* Goal: forall _ : Is_Monotone_Forest a succs, P (root t1) i *)
generalize in_t1; clear in_t1.
(* Goal: forall _ : In_Forest t1 (successors t0), In_tree a t0 *)
elim t0; clear t0.
(* Goal: forall (a0 : A) (f : Forest) (_ : In_Forest t1 (successors (node a0 f))), In_tree a (node a0 f) *)
intros a' succs in_t1.
(* Goal: In_tree a (node a' succs) *)
apply in_succs with (t := t1).
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: P (root t1) i *)
apply ih.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
Qed.

(********************************************************************)
(*  Monotone Trees                                                  *)

Variable I : Set.
Variable P : A -> I -> Prop.

Inductive Is_Monotone_Tree : Tree -> Prop :=
    is_monotone_tree_intro :
      forall (a : A) (succs : Forest),
      Is_Monotone_Forest a succs -> Is_Monotone_Tree (node a succs)
with Is_Monotone_Forest : A -> Forest -> Prop :=
  | is_monotone_forest_nil : forall a : A, Is_Monotone_Forest a Nil_Forest
  | is_monotone_forest_cons :
      forall (a : A) (t : Tree) (succs : Forest),
      (forall i : I, P a i -> P (root t) i) ->
      Is_Monotone_Tree t ->
      Is_Monotone_Forest a succs ->
      Is_Monotone_Forest a (Cons_Forest t succs).




Lemma is_monotone_tree_successor :
 forall t : Tree,
 Is_Monotone_Tree t ->
 forall t0 : Tree, Successor t0 t -> Is_Monotone_Tree t0.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (t0 : Tree) (_ : Successor t0 t), Is_Monotone_Tree t0 *)
intros t is_mon_t t0 suc_t0.
(* Goal: Is_Monotone_Tree t0 *)
generalize is_mon_t; clear is_mon_t.
(* Goal: forall _ : Is_Monotone_Tree t, Is_Monotone_Tree t0 *)
elim suc_t0; clear suc_t0 t0.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall _ : Is_Monotone_Tree t1, Is_Monotone_Tree t2) (_ : Is_Monotone_Tree t0), Is_Monotone_Tree t2 *)
intros t0 t1 in_t1 t2 suc_t2 ih is_mon_t0.
(* Goal: Is_Monotone_Tree t2 *)
apply ih; clear ih suc_t2 t2.
(* Goal: forall _ : Is_Monotone_Forest a succs, P (root t1) i *)
generalize in_t1; clear in_t1.
(* Goal: forall _ : In_Forest t1 (successors t0), Is_Monotone_Tree t1 *)
inversion_clear is_mon_t0.
(* Goal: forall (_ : In_Forest t1 (successors (node a succs))) (_ : P (root (node a succs)) i), P (root t1) i *)
simpl in |- *.
(* Goal: forall _ : P (root t0) i, P (root t1) i *)
generalize H; clear H.
(* Goal: forall (_ : In_Forest t1 succs) (_ : Is_Monotone_Forest a succs), P (root t1) i *)
elim succs; clear succs.
(* Goal: forall (_ : Is_Monotone_Forest a Nil_Forest) (_ : In_Forest t1 Nil_Forest), Is_Monotone_Tree t1 *)
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (_ : Is_Monotone_Forest a f) (_ : In_Forest t1 f), Is_Monotone_Tree t1) (_ : Is_Monotone_Forest a (Cons_Forest t f)) (_ : In_Forest t1 (Cons_Forest t f)), Is_Monotone_Tree t1 *)
intros H in_t1.
(* Goal: P (root t1) i *)
inversion_clear in_t1.
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (_ : Is_Monotone_Forest a f) (_ : In_Forest t1 f), Is_Monotone_Tree t1) (_ : Is_Monotone_Forest a (Cons_Forest t f)) (_ : In_Forest t1 (Cons_Forest t f)), Is_Monotone_Tree t1 *)
intros t2 succs ih H in_t1.
(* Goal: P (root t1) i *)
inversion_clear in_t1.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
inversion_clear H; assumption.
(* Goal: P (root t1) i *)
apply ih.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
inversion_clear H; assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
Qed.


Inductive Is_Monotone (t : Tree) : Prop :=
    is_monotone_intro :
      (forall t0 : Tree,
       Successor t0 t ->
       forall i : I,
       P (root t0) i -> forall t1 : Tree, Successor t1 t0 -> P (root t1) i) ->
      Is_Monotone t.



Lemma is_monotone_successor :
 forall T : Tree,
 Is_Monotone T -> forall t : Tree, Successor t T -> Is_Monotone t.
(* Goal: forall (T : Tree) (_ : Is_Monotone T) (t : Tree) (_ : Successor t T), Is_Monotone t *)
intros T mon_T t suc_t.
(* Goal: Is_Monotone t *)
apply is_monotone_intro.
(* Goal: forall (t0 : Tree) (_ : Successor t0 t) (i : I) (_ : P (root t0) i) (t1 : Tree) (_ : Successor t1 t0), P (root t1) i *)
intros t0 suc_t0 i Pa t1 suc_1.
(* Goal: P (root t1) i *)
inversion_clear mon_T.
(* Goal: P (root t1) i *)
apply H with t0.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
apply succs_trans with t; assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
Qed.


Lemma is_monotone_tree_is_monotone :
 forall t : Tree, Is_Monotone_Tree t -> Is_Monotone t.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t), Is_Monotone t *)
intros t H.
(* Goal: Is_Monotone t *)
apply is_monotone_intro.
(* Goal: forall (t0 : Tree) (_ : Successor t0 t) (i : I) (_ : P (root t0) i) (t1 : Tree) (_ : Successor t1 t0), P (root t1) i *)
intros t0 suc_t0.
(* Goal: forall (i : I) (_ : P (root t0) i) (t1 : Tree) (_ : Successor t1 t0), P (root t1) i *)
generalize (is_monotone_tree_successor t H t0 suc_t0); clear H suc_t0 t.
(* Goal: forall (_ : Is_Monotone_Tree t0) (i : I) (_ : P (root t0) i) (t1 : Tree) (_ : Successor t1 t0), P (root t1) i *)
intros H i P0 t1 suc_t1.
(* Goal: P (root t1) i *)
generalize P0; clear P0.
(* Goal: forall _ : P (root t0) i, P (root t1) i *)
generalize H; clear H.
(* Goal: forall (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t1) i *)
elim suc_t1; clear suc_t1 t0 t1.
(* Goal: forall (t : Tree) (_ : Is_Monotone_Tree t) (_ : P (root t) i), P (root t) i *)
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
trivial.
(* Goal: forall (t0 t1 : Tree) (_ : In_Forest t1 (successors t0)) (t2 : Tree) (_ : Successor t2 t1) (_ : forall (_ : Is_Monotone_Tree t1) (_ : P (root t1) i), P (root t2) i) (_ : Is_Monotone_Tree t0) (_ : P (root t0) i), P (root t2) i *)
intros t0 t1 in_t1 t2 suc_t2 ih H P0.
(* Goal: P (root t2) i *)
apply ih; clear ih.
(* Goal: Is_Monotone_Tree t1 *)
(* Goal: P (root t1) i *)
apply is_monotone_tree_successor with t0. 
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: Successor t1 t0 *)
(* Goal: P (root t1) i *)
apply successor_trans with t1.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: Successor t1 t1 *)
(* Goal: P (root t1) i *)
apply successor_refl.
(* Goal: P (root t1) i *)
generalize P0; clear P0.
(* Goal: forall _ : Is_Monotone_Forest a succs, P (root t1) i *)
generalize in_t1; clear in_t1.
(* Goal: forall (_ : In_Forest t1 (successors t0)) (_ : P (root t0) i), P (root t1) i *)
inversion_clear H.
(* Goal: forall (_ : In_Forest t1 (successors (node a succs))) (_ : P (root (node a succs)) i), P (root t1) i *)
simpl in |- *.
(* Goal: forall (_ : In_Forest t1 succs) (_ : P a i), P (root t1) i *)
intros in_t1 Pa.
(* Goal: P (root t1) i *)
generalize H0; clear H0.
(* Goal: forall _ : Is_Monotone_Forest a succs, P (root t1) i *)
generalize in_t1; clear in_t1.
(* Goal: forall (_ : In_Forest t1 succs) (_ : Is_Monotone_Forest a succs), P (root t1) i *)
elim succs; clear succs.
(* Goal: forall (_ : In_Forest t1 Nil_Forest) (_ : Is_Monotone_Forest a Nil_Forest), P (root t1) i *)
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (_ : In_Forest t1 f) (_ : Is_Monotone_Forest a f), P (root t1) i) (_ : In_Forest t1 (Cons_Forest t f)) (_ : Is_Monotone_Forest a (Cons_Forest t f)), P (root t1) i *)
intros in_t1 H0.
(* Goal: P (root t1) i *)
inversion_clear in_t1.
(* Goal: forall (t : Tree) (f : Forest) (_ : forall (_ : In_Forest t1 f) (_ : Is_Monotone_Forest a f), P (root t1) i) (_ : In_Forest t1 (Cons_Forest t f)) (_ : Is_Monotone_Forest a (Cons_Forest t f)), P (root t1) i *)
intros t3 succs ih in_t1 H0.
(* Goal: P (root t1) i *)
inversion_clear in_t1.
(* Goal: P (root t3) i *)
(* Goal: P (root t1) i *)
inversion_clear H0.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
apply H; assumption.
(* Goal: P (root t1) i *)
apply ih.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
assumption.
(* Goal: In_Forest t1 succs *)
(* Goal: Is_Monotone_Forest a succs *)
inversion_clear H0; assumption.
Qed.


End Trees.
