Require Import nat_trees.
Require Import search_trees.
Require Import DeleteMax.
Require Import Arith.
Require Import Compare_dec.

Inductive RM (n : nat) (t t' : nat_tree) : Prop :=
    rm_intro :
      ¬ occ t' n →
      (∀ p : nat, occ t' p → occ t p) →
      (∀ p : nat, occ t p → occ t' p ∨ n = p) →
      search t' → RM n t t'.

Hint Resolve rm_intro: searchtrees.


Remark RM_0 : ∀ n : nat, RM n NIL NIL.
Proof.
intro n; apply rm_intro; auto with searchtrees v62.
Defined.

Hint Resolve RM_0: searchtrees.

Remark RM_1 : ∀ n : nat, RM n (bin n NIL NIL) NIL.
Proof.
intros; apply rm_intro; auto with searchtrees v62.
intros p H; elim (occ_inv n _ _ _ H); auto with searchtrees v62.
tauto.
Defined.

Hint Resolve RM_1: searchtrees.


Remark rm_left :
 ∀ (n p : nat) (t1 t2 t' : nat_tree),
 p < n →
 search (bin n t1 t2) → RM p t1 t' → RM p (bin n t1 t2) (bin n t' t2).
Proof.
intros n p t1 t2 t' H H0 H1.
apply rm_intro. unfold not in |- *; intro H2.
elim (occ_inv n p t' t2).
intro eg; absurd (p < p); auto with searchtrees v62.
pattern p at 2 in |- *; elim eg; auto with searchtrees v62.
intro D; elim D; intro H3.
elim H1; auto with searchtrees v62.
absurd (occ t2 p); auto with searchtrees v62.
apply not_right with n t1; auto with searchtrees v62.
auto with searchtrees v62.
intros p0 H2.
elim (occ_inv n p0 t' t2).
simple induction 1; auto with searchtrees v62.
simple induction 1; auto with searchtrees v62.
intro; elim H1; auto with searchtrees v62.
auto with searchtrees v62.
intros.
elim (occ_inv n p0 t1 t2).
simple induction 1; auto with searchtrees v62.
simple induction 1; intro H4.
elim H1.
intros H5 H6 H7 H8.
elim (H7 p0 H4); auto with searchtrees v62.
auto with searchtrees v62.
auto with searchtrees v62.
apply bin_search.
elim H1; auto with searchtrees v62.
apply search_r with n t1; auto with searchtrees v62.
apply maj_intro; intros q H2.
cut (occ t1 q).
intro; elim (maj_l n t1 t2 H0); intros; auto with searchtrees v62.
auto with searchtrees v62.
elim H1; auto with searchtrees v62.
apply min_r with t1; auto with searchtrees v62.
Defined.

Hint Resolve rm_left: searchtrees.


Remark rm_right :
 ∀ (n p : nat) (t1 t2 t' : nat_tree),
 n < p →
 search (bin n t1 t2) → RM p t2 t' → RM p (bin n t1 t2) (bin n t1 t').
Proof.
intros n p t1 t2 t' H H0 H1.
apply rm_intro.
unfold not in |- *; intro H2.
elim (occ_inv n p t1 t').
intro eg; absurd (p < p); auto with searchtrees v62.
pattern p at 1 in |- *; elim eg; auto with searchtrees v62.
intro D; elim D; intro H3.
elim H1; auto with searchtrees v62.
absurd (occ t1 p).
apply not_left with n t2; auto with searchtrees v62.
auto with searchtrees v62.
elim H1; auto with searchtrees v62.
auto with searchtrees v62.
intros p0 H2.
elim (occ_inv n p0 t1 t').
simple induction 1; auto with searchtrees v62.
simple induction 1; auto with searchtrees v62.
intro; elim H1; auto with searchtrees v62.
auto with searchtrees v62.
intros.
elim (occ_inv n p0 t1 t2).
simple induction 1; auto with searchtrees v62.
simple induction 1; auto with searchtrees v62.
intro H4.
elim H1; intros H5 H6 H7 H8.
elim (H7 p0 H4); auto with searchtrees v62.
auto with searchtrees v62.
apply bin_search.
apply search_l with n t2; auto with searchtrees v62.
elim H1; auto with searchtrees v62.
apply maj_l with t2; auto with searchtrees v62.
apply min_intro; intros q H2.
cut (occ t2 q).
intro.
elim (min_r n t1 t2 H0); auto with searchtrees v62.
elim H1; auto with searchtrees v62.
Defined.

Hint Resolve rm_right: searchtrees.


Remark rm_NILt :
 ∀ (n : nat) (t : nat_tree),
 search (bin n NIL t) → RM n (bin n NIL t) t.
Proof.
intros; apply rm_intro.
apply not_right with n NIL; auto with searchtrees v62.
auto with searchtrees v62.
intros p H1; elim (occ_inv n p NIL t H1); intro H2.
right; auto with searchtrees v62.
elim H2; intro.
absurd (occ NIL p); auto with searchtrees v62.
left; auto with searchtrees v62.
apply search_r with n NIL; auto with searchtrees v62.
Defined.

Hint Resolve rm_NILt: searchtrees.


Section rm_root.
     Variable n p : nat.
     Variable t1 t2 t' : nat_tree.
     Hypothesis S : search (bin n (bin p t1 t2) t').
     Variable q : nat.
     Variable t0 : nat_tree.
     Hypothesis R : RMAX (bin p t1 t2) t0 q.
     Hint Resolve S: searchtrees.

     Remark rm_2 : q < n.
     Proof.
     elim R.
     intros.
     elim (maj_l n (bin p t1 t2) t').
     auto with searchtrees v62.
     auto with searchtrees v62.
     Qed.

     Hint Resolve rm_2: searchtrees.

     Remark rm_3 : ¬ occ (bin q t0 t') n.
     Proof.
     unfold not in |- *; intro H.
     elim (occ_inv q n t0 t').
     intro eg; absurd (q < q); auto with searchtrees v62.
     pattern q at 2 in |- *; rewrite eg; auto with searchtrees v62.
     intro D; elim D; intro H'.
     elim R; intros H0 H1 H2 H3 H4 H5.
     absurd (occ (bin p t1 t2) n); auto with searchtrees v62.
     apply not_left with n t'; auto with searchtrees v62.
     absurd (occ t' n); auto with searchtrees v62.
     apply not_right with n (bin p t1 t2); auto with searchtrees v62.
     auto with searchtrees v62.
     Qed.

     Hint Resolve rm_3: searchtrees.

     Remark rm_4 :
      ∀ p0 : nat,
      occ (bin q t0 t') p0 → occ (bin n (bin p t1 t2) t') p0.
     Proof.
     intros p0 H.
     elim (occ_inv q p0 t0 t' H).
     intro eg.
     elim R; rewrite eg; auto with searchtrees v62.
     simple induction 1; auto with searchtrees v62.
     intro H'. elim R; auto with searchtrees v62.
     Qed.

     Hint Resolve rm_4: searchtrees.

     Remark rm_5 :
      ∀ p0 : nat,
      occ (bin n (bin p t1 t2) t') p0 → occ (bin q t0 t') p0 ∨ n = p0.
     Proof.
     intros p0 H.
     elim (occ_inv n p0 (bin p t1 t2) t').
     simple induction 1; auto with searchtrees v62.
     simple induction 1.
     intro H1.
     elim R; intros H2 H3 H4 H5 H6 H7.
     elim (H5 p0 H1). intro; left; auto with searchtrees v62.
     simple induction 1; left; auto with searchtrees v62.
     intro; left; auto with searchtrees v62.
     auto with searchtrees v62.
     Qed.

     Hint Resolve rm_5: searchtrees.

     Remark rm_6 : search (bin q t0 t').
     Proof.
     apply bin_search.
     elim R; auto with searchtrees v62.
     apply search_r with n (bin p t1 t2); auto with searchtrees v62.
     elim R; intros H H0 H1 H2 H3 H4.
     apply maj_intro.
     intros q0 H5; elim (le_lt_or_eq q0 q (H0 q0 (H1 q0 H5))).
     auto with searchtrees v62.
     intro eg; absurd (occ t0 q0).
     rewrite eg; auto with searchtrees v62.
     auto with searchtrees v62.
     apply min_intro.
     intros q0 H.
     apply lt_trans with n.
     elim R; auto with searchtrees v62.
     elim (min_r n (bin p t1 t2) t').
     auto with searchtrees v62.
     auto with searchtrees v62.
     Qed.

     Hint Resolve rm_6: searchtrees.

     Lemma rm_root_lemma : RM n (bin n (bin p t1 t2) t') (bin q t0 t').
     Proof.
     apply rm_intro; auto with searchtrees v62.
     Qed.

End rm_root.


Theorem rm :
 ∀ (n : nat) (t : nat_tree), search t → {t' : nat_tree | RM n t t'}.
Proof.
 simple induction t;
  [ intros s; ∃ NIL
  | intros p; elim (le_gt_dec n p); intros h;
     [ elim (le_lt_eq_dec n p h); intros h';
        [ intros t1 hr1 t2 hr2 s; elim hr1;
           [ intros t3 h3; ∃ (bin p t3 t2) | idtac ]
        | intros t1; case t1;
           [ intros hr1 t2 hr2 s; ∃ t2
           | intros p' t1' t2' hr1 t2 hr2 s; elim (rmax (bin p' t1' t2'));
              [ intros q ex; elim ex; intros t' H; ∃ (bin q t' t2)
              | idtac
              | idtac ] ] ]
     | intros t1 hr1 t2 hr2 s; elim hr2;
        [ intros t3 h3; ∃ (bin p t1 t3) | idtac ] ] ];
  auto with searchtrees v62.

 eapply search_l; eauto with searchtrees v62.
 rewrite h'; apply rm_NILt; auto with searchtrees v62.
 rewrite h'; apply rm_root_lemma; auto with searchtrees v62.
 eapply search_l; eauto with searchtrees v62.
 eapply search_r; eauto with searchtrees v62.

Defined.