Require Import nat_trees.
Require Import More_on_Lists.
Require Import search_trees.
Require Import Adding.


Theorem list2trees :
 ∀ l : list nat,
 {t : nat_tree | search t ∧ (∀ p : nat, In p l ↔ occ t p)}.

Proof.

 Lemma list2trees_aux :
  ∀ (l : list nat) (t : nat_tree),
  search t →
  {t' : nat_tree |
  search t' ∧ (∀ p : nat, In p l ∨ occ t p ↔ occ t' p)}.
 Proof.
simple induction l;
 [ intros t s; ∃ t
 | intros hd tl hr t H; elim (insert hd t H); intros x i; elim (hr x);
    [ intros n a; ∃ n | idtac ] ].


  split; auto with searchtrees v62.
  intro p; unfold iff in |- *; split; intros H0.
  elim H0; auto with searchtrees v62.
  intro; absurd (In p nil); auto with searchtrees v62.
  auto with searchtrees v62.

2: elim i; auto with searchtrees v62.

  split; elim a; auto with searchtrees v62.
  intros; unfold iff in |- *; split; intros.
  elim H2; intros.
  inversion_clear H3.
  rewrite <- H4.
  elim (H1 hd); intros.
  apply H3.
  right; elim i; auto with searchtrees v62.
  elim (H1 p); auto with searchtrees v62.
  elim (H1 p); intros.
  apply H4.
  right; elim i; auto with searchtrees v62.
  elim (H1 p); intros.
  elim (H4 H2); intros.
  auto with searchtrees v62.
  elim i; intros.
  elim (H8 p).
  auto with searchtrees v62.
  simple induction 1; auto with searchtrees v62.
  auto with searchtrees v62.
 Defined.

 intros l; elim (list2trees_aux l NIL); [ intros x a; ∃ x | idtac ].

 elim a; split; [ auto with searchtrees v62 | idtac ].
 intro p0; unfold iff in |- *; split; intros.
 elim (H0 p0); intros.
 auto with searchtrees v62.
 elim (H0 p0); intros.
 elim (H3 H1); auto with searchtrees v62.
 intro; absurd (occ NIL p0); auto with searchtrees v62.
 auto with searchtrees v62.
Defined.