Require Import nat_trees.
Require Import search_trees.
Require Import Arith.

Inductive RMAX (t t' : nat_tree) (n : nat) : Prop :=
    rmax_intro :
      occ t n →
      (∀ p : nat, occ t p → p ≤ n) →
      (∀ q : nat, occ t' q → occ t q) →
      (∀ q : nat, occ t q → occ t' q ∨ n = q) →
      ¬ occ t' n → search t' → RMAX t t' n.

Hint Resolve rmax_intro: searchtrees.


Lemma rmax_nil_nil : ∀ n : nat, RMAX (bin n NIL NIL) NIL n.
Proof.
 intro n; split; auto with searchtrees v62.
 intros p H; inversion_clear H; auto with searchtrees v62.
 absurd (occ NIL p); auto with searchtrees v62.
 absurd (occ NIL p); auto with searchtrees v62.
 intros q H; inversion_clear H; auto with searchtrees v62.
Defined.

Lemma rmax_t_NIL :
 ∀ (t : nat_tree) (n : nat),
 search (bin n t NIL) → RMAX (bin n t NIL) t n.
Proof.
 intros t n H; split; auto with searchtrees v62.
 intros p H0.
 elim (occ_inv n p t NIL H0); intro H1.
 elim H1; auto with searchtrees v62.
 elim H1; intro H2.
 apply lt_le_weak.
 elim (maj_l n t NIL H); auto with searchtrees v62.
 absurd (occ NIL p); auto with searchtrees v62.
 intros q H1; elim (occ_inv n q t NIL H1); intros; auto with searchtrees v62.
 elim H0.
 auto with searchtrees v62.
 intro H'; absurd (occ NIL q); auto with searchtrees v62.
 apply not_left with n NIL; auto with searchtrees v62.
 apply search_l with n NIL; auto with searchtrees v62.
Defined.

Hint Resolve rmax_t_NIL: searchtrees.


Section RMAX_np.
     Variable n p q : nat.
     Variable t1 t2 t3 t' : nat_tree.
     Hypothesis S1 : search (bin n t1 (bin p t2 t3)).
     Hypothesis R1 : RMAX (bin p t2 t3) t' q.
     Hint Resolve S1 R1: searchtrees.

     Remark rmax_1 : occ (bin n t1 (bin p t2 t3)) q.
     Proof.
      elim R1; auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_1: searchtrees.

     Remark rmax_2 : n < p.
     Proof.
      elim (min_r _ _ _ S1); auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_2: searchtrees.

     Remark rmax_3 : min n t'.
     Proof.
      apply min_intro.
      intros q' H.
      elim R1; intros.
      elim (min_r _ _ _ S1); auto with searchtrees v62.
     Qed.
     Hint Resolve rmax_3: searchtrees.

     Remark rmax_4 : search (bin n t1 t').
     Proof.
      apply bin_search.
      apply search_l with n (bin p t2 t3); auto with searchtrees v62.
      elim R1; auto with searchtrees v62.
      apply maj_l with (bin p t2 t3); auto with searchtrees v62.
      auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_4: searchtrees.

     Remark rmax_5 : n < q.
     Proof.
      elim R1; intros; apply lt_le_trans with p; auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_5: searchtrees.

     Remark rmax_6 :
      ∀ p0 : nat, occ (bin n t1 (bin p t2 t3)) p0 → p0 ≤ q.
     Proof.
      intros p0 H.
      elim R1.
      intros H0 H1 H2 H3 H4 H5.
      elim (occ_inv _ _ _ _ H); intro H6.
      elim H6; auto with searchtrees v62.
      elim H6; intro H7.
      elim (maj_l _ _ _ S1).
      intro H8.
      cut (p0 < n); auto with searchtrees v62.
      intro; apply lt_le_weak.
      apply lt_trans with n; auto with searchtrees v62.
      elim (min_r _ _ _ S1); auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_6: searchtrees.

     Remark rmax_7 :
      ∀ q' : nat,
      occ (bin n t1 t') q' → occ (bin n t1 (bin p t2 t3)) q'.
     Proof.
      intros q' H; elim (occ_inv _ _ _ _ H); intro H0.
      elim H0; auto with searchtrees v62.
      elim H0; auto with searchtrees v62.
      intro H1; elim R1; auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_7: searchtrees.

     Remark rmax_8 : ¬ occ (bin n t1 t') q.
     Proof.
      unfold not in |- *; intro F.
      elim (occ_inv _ _ _ _ F).
      intro eg; absurd (n < q); auto with searchtrees v62.
      elim eg; auto with searchtrees v62.
      simple induction 1; intro H1.
      absurd (occ t1 q); auto with searchtrees v62.
      apply not_left with n (bin p t2 t3); auto with searchtrees v62.
      elim R1; auto with searchtrees v62.
     Qed.

     Hint Resolve rmax_8: searchtrees.

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

     Hint Resolve rmax_9: searchtrees.

     Lemma rmax_t1_t2t3 : RMAX (bin n t1 (bin p t2 t3)) (bin n t1 t') q.
     Proof.
      apply rmax_intro; auto with searchtrees v62.
     Qed.

End RMAX_np.

Hint Resolve rmax_t1_t2t3: searchtrees.

Lemma rmax :
 ∀ t : nat_tree,
 search t → binp t → {q : nat & {t' : nat_tree | RMAX t t' q}}.
Proof.

simple induction t;
 [ intros s b; ∃ 0; ∃ NIL
 | intros n t1 hr1 t2; case t2;
    [ intros hr2 s b; ∃ n; ∃ t1
    | intros n' t1' t2' hr2 s b; elim hr2;
       [ intros num ex; elim ex; intros tr htr; ∃ num;
          ∃ (bin n t1 tr)
       | idtac
       | idtac ] ] ]; auto with searchtrees v62.
absurd (binp NIL); auto with searchtrees v62.
eapply search_r; eauto with searchtrees v62.

Defined.