(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                Avl_prog.v                                *)
(****************************************************************************)

Require Export Le.

Section trees.

(*************************************************)
(*		Variables		  	 *)
(*************************************************)

Axiom a : Set.
Axiom inf : a -> a -> Prop.

Axiom inf_dec : (x,y:a) {inf x y}+{inf y x}.
Axiom inf_trans : (x,y,z:a) (inf x y) -> (inf y z) -> (inf x z).

(*********************************************************)
(*		Definitions and5, and3		         *)
(*********************************************************)

Inductive and5 [a1,a2,a3,a4,a5:Prop] : Prop
	:= conj5 : a1 -> a2 -> a3 -> a4 -> a5 -> (and5 a1 a2 a3 a4 a5).

Hints Resolve conj5 : avl.

(******
Lemma and5_rec : (A1,A2,A3,A4,A5:Prop)
     (C:Set)(A1->A2->A3->A4->A5->C)->(and5 A1 A2 A3 A4 A5)->C.
Intros A1 A2 A3 A4 A5 C F A.
Apply F; Elim A; Auto with avl.
Save.
********)

Inductive and3 [a1,a2,a3:Prop] : Prop
	:= conj3 : a1 -> a2 -> a3  -> (and3 a1 a2 a3).

Hints Resolve conj3 : avl.

(*******
Lemma and3_rec : (A1,A2,A3:Prop)
     (C:Set)(A1->A2->A3->C)->(and3 A1 A2 A3)->C.
Intros A1 A2 A3 C F A.
Apply F; Elim A; Auto with avl.
Save.
********)

(*************************************************)
(*		Definition max		  	 *)
(*************************************************)

Fixpoint max [n:nat] : nat -> nat :=
 [m:nat]Case n of
     (* O *) m
   (* S p *) [p:nat]Case m of
                 (* O *) (S p) 
               (* S q *) [q:nat](S (max p q)) 
		    end
	end.

(*************************************************)
(*		Definition equil		 *)
(*************************************************)

Inductive equil : Set
	:= ga : equil
	| mi : equil
	| dr : equil.

(*************************************************)
(*		Definition abe		  	 *)
(*************************************************)

Inductive abe : Set
	:= nil : abe
	| node : a -> abe -> abe -> equil -> abe.

(*************************************************)
(*		Definition haut		  	 *)
(*************************************************)

Fixpoint haut [h:abe] : nat :=
 	Case h of
           (* nil *) O
(* node l g d des *) [l:a][g,d:abe][des:equil] 
                       (S (max (haut g) (haut d))) 
	end.

Lemma haut_node : (l:a)(g,d:abe)(e:equil)
     (S (max (haut g) (haut d)))=(haut (node l g d e)).
Auto with avl.
Save.

(*************************************************)
(*		Definition or3		  	 *)
(*************************************************)

Inductive or3 [A,B,C:Prop] : Prop :=
    cas1 : A -> (or3 A B C)
  | cas2 : B -> (or3 A B C)
  | cas3 : C -> (or3 A B C).

Hints Resolve cas1 cas2 cas3 : avl.

(*************************************************)
(*		Definition in		  	 *)
(*************************************************)

Inductive In [x:a] : abe->Prop
 := In_left : (y:a)(g,d:abe)(e:equil)(In x g)->(In x (node y g d e))
 | In_right : (y:a)(g,d:abe)(e:equil)(In x d)->(In x (node y g d e))
 | In_node :  (g,d:abe)(e:equil)(In x (node x g d e)).

Hints Resolve In_node In_left In_right : avl.

Lemma In_node_eq : (x,l:a)(g,d:abe)(e:equil)(l=x)->(In x (node l g d e)).
Induction 1; Auto with avl.
Save.
Hints Resolve In_node_eq : avl.

Local in_inverse :=
   [x:a][h:abe]
     Case h of
      (* nil *)     False  
(* node l g d eq *) [l:a][g,d:abe][des:equil]
                            (or3 (In x g) (In x d) (l=x))
	end.

Lemma In_nil : (x:a)~(In x nil).
Red; Intros x H; Change (in_inverse x nil).
Elim H; Simpl; Auto with avl.
Save.
Hints Resolve In_nil : avl.

Lemma In_node_inv : (x:a)(l:a)(g,d:abe)(e:equil)
     (In x (node l g d e))->(or3 (In x g) (In x d) (l=x)).
Intros x l g d e H; Change (in_inverse x (node l g d e)).
Elim H; Simpl; Auto with avl.
Save.
(*Hints Resolve In_node_inv : avl.*)



(*************************************************)
(*		Definition inft		  	 *)
(*************************************************)

Inductive inft [x:a] : abe -> Prop
  := inft_nil : (inft x nil)
  | inft_node : (l:a)(g,d:abe)(des:equil)
                (inf x l)->(inft x g)->(inft x d)->(inft x (node l g d des)).

Hints Resolve inft_nil inft_node : avl.

Local inft_inverse :=
   [x:a][t:abe]Case t of
                (* nil *) True
     (* node l g d des *) [l:a][g,d:abe][des:equil]
	                         (and3 (inf x l) (inft x g) (inft x d))
		end.

Lemma inft_node_inv : (x,l:a)(g,d:abe)(des:equil)
     (inft x (node l g d des))->(and3 (inf x l) (inft x g) (inft x d)).
Intros x l g d des H; Change (inft_inverse x (node l g d des)); Elim H; Simpl;Auto with avl.
Save.

Lemma inft_in_inf : (x:a)(t:abe)(inft x t)->(y:a)(In y t)->(inf x y).
Induction 1; Intros.
Absurd (In y nil); Auto with avl.
Elim (In_node_inv y l g d des); Auto with avl.
Induction 1; Auto with avl.
Save.

Lemma in_inf_inft : (x:a)(t:abe)((y:a)(In y t)->(inf x y))->(inft x t).
Induction t; Auto with avl.
Save.

(*************************************************)
(*		Definition supt		  	 *)
(*************************************************)

Inductive supt [x:a] : abe -> Prop
  := supt_nil : (supt x nil)
  | supt_node : (l:a)(g,d:abe)(des:equil)
                (inf l x)->(supt x g)->(supt x d)->(supt x (node l g d des)).

Hints Resolve supt_nil supt_node : avl.

Local supt_inverse :=
   [x:a][t:abe]Case t of
                (* nil *) True
     (* node l g d des *) [l:a][g,d:abe][des:equil]
                          (and3 (inf l x) (supt x g) (supt x d))
		end.

Lemma supt_node_inv : (x,l:a)(g,d:abe)(des:equil)
     (supt x (node l g d des))->(and3 (inf l x) (supt x g) (supt x d)).
Intros x l g d des H; Change (supt_inverse x (node l g d des)); Elim H; Simpl;Auto with avl.
Save.

Lemma supt_in_inf : (x:a)(t:abe)(supt x t)->(y:a)(In y t)->(inf y x).
Induction 1; Intros.
Absurd (In y nil); Auto with avl.
Elim (In_node_inv y l g d des); Auto with avl.
Induction 1; Auto with avl.
Save.

Lemma in_inf_supt : (x:a)(t:abe)((y:a)(In y t)->(inf y x))->(supt x t).
Induction t; Auto with avl.
Save.


(*************************************************)
(*		Definition bal		  	 *)
(*************************************************)

Inductive bal [g,d:abe] : equil->Prop
   := bal_ga : ((haut g)=(S(haut d))) -> (bal g d ga)
   | bal_mi : ((haut g)=(haut d)) -> (bal g d mi)
   | bal_dr : ((S (haut g))=(haut d)) -> (bal g d dr).

Hints Resolve bal_ga bal_mi bal_dr : avl.

Local bal_inverse := [g,d:abe][e:equil]
     Case e of
         (* ga *)  ((haut g)=(S(haut d)))
         (* mi *)  ((haut g)=(haut d))
	 (* dr *)  ((S(haut g))=(haut d))
     end.

Lemma bal_ga_inv : (g,d:abe)(bal g d ga)->(haut g)=(S(haut d)).
Intros g d H; Change (bal_inverse g d ga); Elim H; Simpl; Auto with avl.
Save.
Hints Immediate bal_ga_inv : avl.

Lemma bal_mi_inv : (g,d:abe)(bal g d mi)->(haut g)=(haut d).
Intros g d H; Change (bal_inverse g d mi); Elim H; Simpl; Auto with avl.
Save.
Hints Immediate bal_mi_inv : avl.


Lemma bal_dr_inv : (g,d:abe)(bal g d dr)->(S (haut g))=(haut d).
Intros g d H; Change (bal_inverse g d dr); Elim H; Simpl; Auto with avl.
Save.
Hints Immediate bal_dr_inv : avl.

Lemma bal_rec : (g,d:abe)(P:equil->Set)
          (((haut g)=(S (haut d)))->(P ga))->
          (((haut g)=(haut d))->(P mi))->
          (((S (haut g))=(haut d))->(P dr))->
          (e:equil)(bal g d e)->(P e).
Realizer [g,d:abe][P:Set][H,H0,H1:P][e:equil]
		Cases e of
		    ga => H 
	          | mi => H0 
		  | dr => H1
		end.
Program_all.
Save.


(*************************************************)
(*		Definition avl		  	 *)
(*************************************************)

Inductive avl : abe -> Prop
:= avl_nil : (avl nil)
| avl_node : (l:a)(g,d:abe)(des:equil)
             (avl g)->(avl d)->(bal g d des)->(supt l g)->(inft l d)
             ->(avl (node l g d des)).

Hints Resolve avl_nil avl_node : avl.

Definition avl_inverse := 
[u:abe]Case u of
           (* nil *) True
(* node l g d des *) [l:a][g,d:abe][des:equil]
    	             (and5 (avl g) (avl d) (supt l g) (inft l d) (bal g d des))
	end.

Lemma avl_inv : (l:a)(g,d:abe)(des:equil)(avl (node l g d des))
     ->(and5 (avl g) (avl d) (supt l g) (inft l d) (bal g d des)).
Intros l g d des H; Change (avl_inverse (node l g d des)).
Elim H; Simpl; Auto with avl.
Save.

Lemma avl_rec : 
     (t:abe)(P:abe->Set)
     (P nil)
     ->((l:a)(g,d:abe)(des:equil)(avl g)->(P g)->(avl d)->(P d)
         ->(supt l g)->(inft l d) ->(bal g d des)->(P (node l g d des)))
     ->(avl t)->(P t).
Realizer [t:abe][P:Set][H0:P][H1:a->abe->abe->equil->P->P->P]
                Match t with
		  H0
                  [l,g,Pg,d,Pd,des](H1 l g d des Pg Pd)
		end.
Program_all.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Elim (avl_inv a1 a2 a3 e); Auto with avl.
Save.

(*************************************************************)
(*    	  A special kind of avl obtained after an insertion  *)
(*        that modifies the heigth                           *)
(*************************************************************)

Inductive avl_ins : abe -> Prop
  := ins_ga : (l:a)(g,d:abe)(avl g)->(avl d)->
              ((haut g)=(S (haut d)))->
              (supt l g)->(inft l d)->(avl_ins (node l g d ga))
  | ins_mil : (l:a)(avl_ins (node l nil nil mi))
  | ins_dr : (l:a)(g,d:abe)(avl g)->(avl d)->
              ((S (haut g))=(haut d))->
              (supt l g)->(inft l d)->(avl_ins (node l g d dr)).

Hints Resolve ins_ga ins_mil ins_dr : avl.
        
Definition avl_ins_inverse := 
[t:abe]Case t of
           (* nil *) False
(* node l g d des *) [l:a][g,d:abe][des:equil] 
                       Case des of
                       (* ga *) (and5 (avl g) (avl d) 
                                      ((haut g)=(S (haut d)))
                                      (supt l g) (inft l d))
                       (* mi *) ((nil=g)/\ (nil=d))
                       (* dr *) (and5 (avl g) (avl d) 
                                      ((S (haut g))=(haut d))
                                      (supt l g) (inft l d))
			end 
	end.

Lemma avl_ins_nil_inv : ~(avl_ins nil).
Red; Intro H; Change (avl_ins_inverse nil); Elim H; Simpl; Auto with avl.
Save.

Lemma avl_ins_ga_inv : (l:a)(g,d:abe)
     (avl_ins (node l g d ga))->
     (and5 (avl g) (avl d) ((haut g)=(S (haut d))) (supt l g) (inft l d)).
Intros l g d H; Change (avl_ins_inverse  (node l g d ga)); Elim H; Simpl;Auto with avl.
Save.

Lemma avl_ins_mi_inv : (l:a)(g,d:abe)
     (avl_ins (node l g d mi))->((nil=g)/\ (nil=d)).
Intros l g d H; Change (avl_ins_inverse  (node l g d mi)); Elim H; Simpl;Auto with avl.
Save.

Lemma avl_ins_dr_inv : (l:a)(g,d:abe)
     (avl_ins (node l g d dr))->
     (and5 (avl g) (avl d) ((S (haut g))=(haut d)) (supt l g) (inft l d)).
Intros l g d H; Change (avl_ins_inverse  (node l g d dr)); Elim H; Simpl;Auto with avl.
Save.

Lemma avl_ins_avl : (t:abe)(avl_ins t)->(avl t).
Induction 1; Auto with avl.
Save.
Hints Immediate avl_ins_avl : avl.

Lemma avl_ins_rec : (P:abe->Set)
        ((l:a)(g,d:abe)(avl g)->(avl d)->
               ((haut g)=(S (haut d)))->
               (supt l g)->(inft l d)->(P (node l g d ga)))
        ->((l:a)(P (node l nil nil mi)))->
        ((l:a)(g,d:abe)(avl g)->(avl d)->
               ((S (haut g))=(haut d))->
               (supt l g)->(inft l d)->(P (node l g d dr)))
        ->(a:abe)(avl_ins a)->(P a).

Realizer [P:Set][H:a->abe->abe->P][H0:a->P][H1:a->abe->abe->P][a0:abe]
             Cases a0 of
		nil => (False_rec P)
              | (node l g d ga) => (H l g d)
	      | (node l _ _ mi) => (H0 l)
              | (node l g d dr) => (H1 l g d)
	     end.


Program_all.
Elim avl_ins_nil_inv; Auto with avl.
Elim (avl_ins_ga_inv l g d); Auto with avl.
Elim (avl_ins_ga_inv l g d); Auto with avl.
Elim (avl_ins_ga_inv l g d); Auto with avl.
Elim (avl_ins_ga_inv l g d); Auto with avl.
Elim (avl_ins_ga_inv l g d); Auto with avl.
Elim (avl_ins_mi_inv l g d); Auto with avl.
Destruct 1; Destruct 1; Auto with avl.
Elim (avl_ins_dr_inv l g d); Auto with avl.
Elim (avl_ins_dr_inv l g d); Auto with avl.
Elim (avl_ins_dr_inv l g d); Auto with avl.
Elim (avl_ins_dr_inv l g d); Auto with avl.
Elim (avl_ins_dr_inv l g d); Auto with avl.
Save.

(*************************************************)
(*		Definition equiv		 *)
(*************************************************)

Definition equiv_abe :=
  [t,t':abe](((x:a)(In x t)->(In x t'))/\ ((x:a)(In x t')->(In x t))).

Inductive equiv [y:a;t,t':abe] : Prop :=
  equiv_intro : 
   ((x:a)(In x t)->(In x t'))->
   (In y t')->((x:a)(In x t')->((In x t)\/y=x))
   -> (equiv y t t').
Hints Resolve equiv_intro : avl.

(*************************************************)
(*    Lemmas                                     *)
(*************************************************)

Lemma equiv_equiv_abe : (x:a)(t,u,v:abe)(equiv x t u)->(equiv_abe u v)->(equiv x t v).
Intros x t u v H H0; Elim H; Intros H1 H2 H3; Elim H0; Intros H4 H5; Auto with avl.
Save.

Lemma equiv_gauche : (y,l:a)(g,g',d:abe)(des,des':equil)
     (equiv y g g')->(equiv y (node l g d des) (node l g' d des')).
Intros.
Elim H ; Intros.
Apply equiv_intro; Auto with avl.
Intros x H3; Elim (In_node_inv x l g d des) ; Auto with avl.
Intros x H3; Elim (In_node_inv x l g' d des') ; Auto with avl.
Intro H4; Elim (H2 x); Auto with avl.
Save.

Lemma equiv_droite : (y,l:a)(g,d,d':abe)(des,des':equil)
     (equiv y d d')->(equiv y (node l g d des) (node l g d' des')).
Intros.
Elim H ; Intros.
Apply equiv_intro; Auto with avl.
Intros x H3; Elim (In_node_inv x l g d des) ; Auto with avl.
Intros x H3; Elim (In_node_inv x l g d' des') ; Auto with avl.
Intro H4; Elim (H2 x); Auto with avl.
Save.

Hints Resolve equiv_gauche equiv_droite : avl.



(*************************************************)
(*		Definition avl_spec	  	 *)
(*************************************************)

Inductive avl_spec [x:a;t:abe] : Set
	:= h_eq : (h:abe)(avl h)->(equiv x t h)->((haut h)=(haut t)) 
                 -> (avl_spec x t)
	| h_plus : (h:abe)(avl_ins h)->(equiv x t h)
                 -> ((haut h)=(S(haut t))) ->(avl_spec x t).

Definition h_eqc := [x:a][t:abe][h:abe](h_eq x t h).
Definition h_plusc := [x:a][t:abe][h:abe](h_plus x t h).

(*************************************************)
(*		Definition abe_match	  	 *)
(*************************************************)
Lemma abe_match : (P:abe->Set)
       (P nil)
     ->((l:a)(g:abe)(d:abe)(des:equil) (P (node l g d des)))
     ->(t:abe)(P t).
Realizer [P:Set][H:P][H0:a->abe->abe->equil->P][t:abe]
                 Cases t of
		    nil => H
                 | (node a0 y y0 e) => (H0 a0 y y0 e)
		  end.
Program_all.
Save.

(*************************************************)
(*		Definition abe_case	  	 *)
(*************************************************)

Lemma abe_case : (t:abe)(P:abe->Prop)
       ((nil=t)->(P nil))
     ->((l:a)(g:abe)(d:abe)(des:equil)
         ((node l g d des)=t)->(P (node l g d des)))
     ->(P t).

Intro t.
Elim t ; Intros ; Auto with avl.
Save.

Lemma equiv_sup_g : (g,g':abe)(l,x:a)
     (equiv x g g')-> (supt l g)-> (inf x l) -> (supt l g').
Induction 1; Intros H1 H2 H3 S I.
Apply in_inf_supt.
Intros y H4; Elim (H3 y); Trivial with avl.
Intro H5; Apply supt_in_inf with g; Auto with avl.
Induction 1; Auto with avl.
Save.

Lemma bal_haut : (g,g',d,d':abe)(des:equil)
     ((haut g')=(haut g))->((haut d')=(haut d))
      ->(bal g d des)->(bal g' d' des).
Intros g g' d d' des Hg Hd B;
Elim B; Elim Hg; Elim Hd; Auto with avl.
Save.

Lemma equiv_inf_g : (g,g':abe)(l,x:a)
     (equiv x g g') -> (inft l g) -> (inf l x) -> (inft l g').
Induction 1; Intros H1 H2 H3 S I.
Apply in_inf_inft.
Intros y H4; Elim (H3 y); Trivial with avl.
Intro H5; Apply inft_in_inf with g; Auto with avl.
Induction 1; Auto with avl.
Save.

Lemma inft_trans : (l,l':a)(t:abe)(inf l l')->(inft l' t)->(inft l t).
Induction 2; Auto with avl.
Intros l0 g d des I' ITg' ITg ITd' ITd.
Cut (inf l l0); Auto with avl.
Apply inf_trans with l'; Auto with avl.
Save.

Lemma supt_trans : (l,l':a)(t:abe)(inf l' l)->(supt l' t)->(supt l t).
Induction 2; Auto with avl.
Intros l0 g d des I' ITg' ITg ITd' ITd.
Cut (inf l0 l); Auto with avl.
Apply inf_trans with l'; Auto with avl.
Save.

Lemma haut_plus : (g,g':abe)(des:equil)(d:abe)(l:a)
     ((haut g)=(haut g'))->
     ((haut (node l g' d des))=(haut (node l g d des))).
Intros g g' des d l H; Simpl; Elim H; Auto with avl.
Save.
Hints Resolve haut_plus : avl.

Lemma max_n_n : (n:nat)(n=(max n n)).
Induction n ; Simpl ; Auto with avl.
Save.
Hints Resolve max_n_n : avl.

Lemma max_Sn_n : (n:nat)((S n)=(max (S n) n)).
Induction n ; Simpl ; Auto with avl.
Save.
Hints Resolve max_Sn_n : avl.

Lemma max_n_Sn : (n:nat)((S n)=(max n (S n))).
Induction n ; Simpl ; Auto with avl.
Save.
Hints Resolve max_n_Sn : avl.

Lemma le_max : (m,n:nat)(le n m)->(m=(max m n)).
Intros m n Le; Pattern n m; Apply le_elim_rel; Simpl; Auto with avl.
Induction p; Simpl; Auto with avl.
Save.
Hints Resolve le_max : avl.

Lemma max_case : (n,m:nat)((n=(max n m))\/(m=(max n m))).
Induction n.
Simpl; Auto with avl.
Induction m.
Simpl; Auto with avl.
Intros p H0; Simpl; Elim (H p); Auto with avl.
Save.

Lemma max_sym : (n,m:nat)(max m n)=(max n m).
Induction n;Induction m; Simpl; Auto with avl.
Save.

(*************************************************)
(*						 *)
(*   Rotations                             	 *)
(*						 *)
(*************************************************)

Chapter rotations.

Variables l, m :a.
Variables t,v : abe.

Hypothesis avlv : (avl v).
Hypothesis avlt : (avl t).

Hypothesis inflv : (inft l v).
Hypothesis supmt : (supt m t).

Hints Resolve inflv supmt avlt avlv : avl.

Section simple_rotations.

Variable u : abe.
Hypothesis avlu : (avl u).
Hints Resolve avlu : avl.

Section right_rotation.

Hypothesis suplmtu : (supt l (node m t u ga)).
Hypothesis infmu : (inft m u).

Hints Resolve suplmtu infmu : avl.

Lemma infml : (inf m l).
Elim (supt_node_inv l m t u ga); Auto with avl.
Save.
Hints Resolve infml : avl.

Lemma suptlu : (supt l u).
Elim (supt_node_inv l m t u ga); Auto with avl.
Save.
Hints Resolve suptlu : avl.

Hypothesis Htu : (haut t)=(S (haut u)).
Hypothesis Huv : (haut u)=(haut v).

Hints Resolve Huv Htu : avl.

Definition rot_d := (node m t (node l u v mi) mi).

Lemma avl_rotd : (avl rot_d).
Unfold rot_d.
Apply avl_node; Auto with avl.
Apply bal_mi; Simpl.
Elim Huv.
Elim max_n_n; Auto with avl.
Apply inft_node; Auto with avl.
Apply inft_trans with l; Auto with avl.
Save.

Lemma equiv_rotd : (eql:equil)(equiv_abe (node l (node m t u ga) v eql) rot_d).
Intro eql; Unfold equiv_abe rot_d; Split.
Intros x H; Elim (In_node_inv x l (node m t u ga) v eql); Auto with avl.
Intro H0; Elim (In_node_inv x m t u ga); Auto with avl.
Intros x H; Elim (In_node_inv x m t (node l u v mi) mi); Auto with avl.
Intro H0; Elim (In_node_inv x l u v mi); Auto with avl.
Save.

Lemma haut_rotd : (S (haut t))=(haut rot_d).
Simpl.
Elim Huv.
Elim max_n_n.
Elim Htu; Auto with avl.
Save.

Opaque rot_d.

End right_rotation.

Section left_rotation.

Hypothesis inftmuv : (inft m (node l u v dr)).
Hypothesis suplu : (supt l u).

Hints Resolve inftmuv suplu : avl.

Lemma infml' : (inf m l).
Elim (inft_node_inv m l u v dr); Auto with avl.
Save.
Hints Resolve infml' : avl.

Lemma inftmu : (inft m u).
Elim (inft_node_inv m l u v dr); Auto with avl.
Save.
Hints Resolve inftmu : avl.

Hypothesis Hut : (haut u)=(haut t).
Hypothesis Huv : (haut v)=(S (haut u)).

Hints Resolve Huv Hut : avl.

Definition rot_g := (node l (node m t u mi) v mi).

Lemma avl_rotg : (avl rot_g).
Unfold rot_g.
Apply avl_node; Auto with avl.
Apply bal_mi; Simpl.
Elim Hut.
Elim max_n_n; Auto with avl.
Apply supt_node; Auto with avl.
Apply supt_trans with m; Auto with avl.
Save.

Lemma equiv_rotg : (eqm:equil)(equiv_abe (node m t (node l u v dr) eqm) rot_g).
Intros eqm; Unfold equiv_abe rot_g; Split.
Intros x H; Elim (In_node_inv x m t (node l u v dr) eqm); Auto with avl.
Intro H0; Elim (In_node_inv x l u v dr); Auto with avl.
Intros x H; Elim (In_node_inv x l (node m t u mi) v mi); Auto with avl.
Intro H0; Elim (In_node_inv x m t u mi); Auto with avl.
Save.

Lemma haut_rotg : (S (haut v))=(haut rot_g).
Unfold rot_g; Elim haut_node.
Elim haut_node.
Elim Hut.
Elim max_n_n.
Elim Huv; Auto with avl.
Save.

Opaque rot_g.

End left_rotation.

End simple_rotations.

Section double_rotations.

Variable n:a.
Variables u1,u2:abe.
Variable eqn : equil.

Local u :=  (node n u1 u2 eqn).
Hypothesis avlu : (avl u).

Hypothesis infmu : (inft m u).
Hypothesis suplu : (supt l u).
Hypothesis infml : (inf m l).

Hints Resolve avlu infmu suplu infml : avl.

Lemma infmu1 : (inft m u1).
Elim (inft_node_inv m n u1 u2 eqn); Auto with avl.
Save.

Lemma suplu2 : (supt l u2).
Elim (supt_node_inv l n u1 u2 eqn); Auto with avl.
Save.

Lemma infnl : (inf n l).
Elim (supt_node_inv l n u1 u2 eqn); Auto with avl.
Save.

Lemma infmn : (inf m n).
Elim (inft_node_inv m n u1 u2 eqn); Auto with avl.
Save.

Hints Resolve infmu1 suplu2 infnl infmn : avl.

Lemma supnt : (supt n t).
Apply supt_trans with m; Auto with avl.
Save.

Lemma infnv : (inft n v).
Apply inft_trans with l; Auto with avl.
Save.

Hints Resolve supnt infnv : avl.

Hypothesis Htu : (S (haut t))=(haut u).
Hypothesis Htv : (haut t)=(haut v).

Hints Resolve Htu Htv : avl.

Local eqm := Case eqn of (* ga *) mi (* mi *) mi (* dr *) ga end.
Local eql := Case eqn of (* ga *) dr (* mi *) mi (* dr *) mi end.

Definition rot_gd := (node n (node m t u1 eqm) (node l u2 v eql) mi).

Lemma equiv_rotgd : (eql':equil)(equiv_abe (node l (node m t u dr) v eql') rot_gd).
Intros eql'; Unfold equiv_abe rot_gd; Split.
Intros x H; Elim (In_node_inv x l (node m t u dr) v eql'); Auto with avl.
Intros H0; Elim (In_node_inv x m t u dr); Auto with avl.
Intros H1; Elim (In_node_inv x n u1 u2 eqn); Auto with avl.
Unfold u; Intros x H; 
       Elim (In_node_inv x n (node m t u1 eqm) (node l u2 v eql) mi);Trivial with avl.
Intros H0; Elim (In_node_inv x  m t u1 eqm); Auto with avl.
Intros H0; Elim (In_node_inv x l u2 v eql); Auto with avl.
Auto with avl.
Save.

Lemma equiv_rotdg : (eql':equil)(equiv_abe (node m t (node l u v ga) eql') rot_gd).
Intros eql'; Unfold equiv_abe rot_gd; Split.
Intros x H; Elim (In_node_inv x m t (node l u v ga) eql'); Auto with avl.
Intros H0; Elim (In_node_inv x l u v ga); Auto with avl.
Intros H1; Elim (In_node_inv x n u1 u2 eqn); Auto with avl.
Unfold u; Intros x H; 
       Elim (In_node_inv x n (node m t u1 eqm) (node l u2 v eql) mi);Trivial with avl.
Intros H0; Elim (In_node_inv x  m t u1 eqm); Auto with avl.
Intros H0; Elim (In_node_inv x l u2 v eql); Auto with avl.
Auto with avl.
Save.

Lemma avl_rotgd : (avl rot_gd).
Unfold rot_gd.
Elim (avl_inv n u1 u2 eqn); Trivial with avl.
Intros avlu1 avlu2 supnu1 infnu2 balu1u2.
Unfold eqm eql; Elim balu1u2.
Intro Hu1u2; Cut (haut t)=(haut u1).
Intro Htu1; Cut (S (haut u2))=(haut v).
Intro Hu2v; Apply avl_node; Auto with avl.
Apply bal_mi; Simpl.
Elim Htu1; Elim max_n_n; Elim Hu2v; Elim max_n_Sn; Elim Hu1u2; Auto with avl.
Elim Htv; Elim Hu1u2; Auto with avl.
Apply eq_add_S; Replace (S (haut u1)) with (haut u); Auto with avl.
Simpl; Rewrite -> Hu1u2; Auto with avl.
Intro Hu1u2; Cut (haut t)=(haut u1).
Intro Htu1; Cut (haut u2)=(haut v).
Intro Hu2v; Apply avl_node; Auto with avl.
Apply bal_mi; Simpl.
Elim Htu1; Elim max_n_n; Elim Hu2v; Elim max_n_n; Elim Hu1u2; Auto with avl.
Elim Htv; Elim Hu1u2; Auto with avl.
Apply eq_add_S; Replace (S (haut u1)) with (haut u); Auto with avl. 
Simpl; Elim Hu1u2; Auto with avl.
Intro Hu1u2; Cut (haut t)=(S (haut u1)).
Intro Htu1; Cut (haut u2)=(haut v).
Intro Hu2v; Apply avl_node; Auto with avl.
Apply bal_mi; Simpl.
Rewrite -> Htu1.
Elim max_Sn_n; Elim Hu2v; Elim max_n_n; Auto with avl.
Elim Htv; Rewrite -> Htu1; Auto with avl.
Apply eq_add_S; Rewrite -> Htu; Simpl.
Elim Hu1u2; Auto with avl.
Save.

Lemma haut_rotgd : (S (S (haut v)))=(haut rot_gd).
Unfold rot_gd.
Elim haut_node.
Elim haut_node.
Elim haut_node.
Elim Htv.
Replace (haut t) with (max (haut u1) (haut u2)).
Elim (max_sym (haut u2)).
Elim (max_case (haut u1) (haut u2)); Intro H.
Elim H.
Elim H.
Elim max_n_n; Auto with avl.
Elim H.
Elim max_n_n.
Elim (max_sym (haut u2)); Elim H; Auto with avl.
Apply eq_add_S; Auto with avl.
Save.

Opaque rot_gd.

End double_rotations.

End rotations.
Hints Resolve equiv_rotd equiv_rotg equiv_rotgd equiv_rotdg haut_rotd haut_rotg haut_rotgd : avl.

Theorem insert : (x:a)(t:abe)(avl t)->(avl_spec x t).
Realizer 
[x:a][t:abe][{Hyp:(avl t)}]
  (avl_rec t avl_spec 
      (h_plusc x nil (node x nil nil mi))
      [l:a][g,d:abe][des:equil][avlsg,avlsd:avl_spec]
        Case (inf_dec x l) of
            Case avlsg of
                [g'](h_eqc x (node l g d des) (node l g' d des))
                (bal_rec g d abe->avl_spec
                    [g':abe][{H:(avl_ins g')}]
                       (avl_ins_rec avl_spec
                           [m:a][g'g,g'd:abe]
		       	     (h_eqc x (node l g d ga) (rot_d l m g'g d g'd))
                           [l0:a](False_rec avl_spec)
                           [m:a][g'g,g'd:abe]
                             Case g'd of
                                 (False_rec avl_spec)
                                 [n,g'd1,g'd2,eqn]
                                   (h_eqc x (node l g d ga)
                                            (rot_gd l m g'g d n g'd1 g'd2 eqn))
			     end
                        g')
                    [g':abe](h_plusc x (node l g d mi) (node l g' d ga))
                    [g':abe](h_eqc x (node l g d dr) (node l g' d mi))
                 des)
	    end
            Case avlsd of
                 [d'](h_eqc x (node l g d des) (node l g d' des))
                 (bal_rec g d abe->avl_spec
                     [d':abe](h_eqc x (node l g d ga) (node l g d' mi))
                     [d':abe](h_plusc x (node l g d mi) (node l g d' dr))
                     [d':abe][{H:(avl_ins d')}]
                        (avl_ins_rec avl_spec
                            [m:a][d'g,d'd:abe]
                              Case d'g of
                                  (False_rec avl_spec)
                                  [n,d'g1,d'g2,eqn]
                                    (h_eqc x (node l g d dr)
                                             (rot_gd m l g d'd n d'g1 d'g2 eqn))
                              end
                            [m:a](False_rec avl_spec)
                            [m:a][d'g,d'd:abe]
                              (h_eqc x (node l g d dr) (rot_g m l g d'd d'g))
                         d')
                  des)
	     end
        end).

Program_all.
(* (equiv x nil (node x nil nil mi)) *)
Apply equiv_intro ; Intros ; Auto with avl.
Elim  (In_node_inv x0 x nil nil mi) ; Auto with avl.
(* (avl (node l h d des)) *)
Apply avl_node ; Auto with avl.
Apply bal_haut with g d ; Trivial with avl.
Apply equiv_sup_g with g x ; Auto with avl.
(* (avl (rot_d l m g'g d g'd)) *)
Apply avl_rotd ; Auto with avl.
Apply equiv_sup_g with g x; Auto with avl.
Apply eq_add_S ; Elim H8 ; Apply eq_add_S ; Elim H4 . 
Elim e0 ; Elim haut_node.
Rewrite -> H8; Auto with avl.
(* (equiv x (node l g d ga) (rot_d l m g'g d g'd))  *)
Apply equiv_equiv_abe with (node l (node m g'g g'd ga) d ga) ; Auto with avl.
(* (haut (rot_d l m g'g d g'd))=(haut (node l g d ga)) *)
Elim haut_node.
Rewrite -> H4.
Elim max_Sn_n.
Elim haut_rotd ; Auto with avl.
Elim H4 ; Elim e0.
Elim haut_node.
Rewrite -> H8.
Elim max_Sn_n ; Auto with avl.
Apply eq_add_S ; Elim H8 ; Apply eq_add_S ; Elim H4. 
Elim e0 ; Elim haut_node.
Rewrite -> H8; Auto with avl.
(* False *)
Absurd O=(haut g); Auto with avl.
Rewrite -> H4 ; Auto with avl.
(* False *)
Absurd (S (haut g'g))=O ; Auto with avl.
(* (avl (rot_gd l m g'g d n g'd1 g'd2 eqn)) *)
Apply avl_rotgd; Auto with avl.
Elim (supt_node_inv l m g'g (node n g'd1 g'd2 eqn) dr); Auto with avl.
Apply equiv_sup_g with g x ; Auto with avl.
Apply eq_add_S ; Elim H8 ; Apply eq_add_S ; Elim H4.
Elim e0; Elim haut_node.
Elim H8; Auto with avl.
(* (equiv x (node l g d ga) (rot_gd l m g'g d n g'd1 g'd2 eqn)) *)
Apply equiv_equiv_abe with (node l (node m g'g (node n g'd1 g'd2 eqn) dr) d ga) ; Auto with avl.
(* (haut (rot_gd l m g'g d n g'd1 g'd2 eqn))=(haut (node l g d ga)) *)
Elim haut_rotgd ; Auto with avl.
Elim haut_node.
Rewrite -> H4 ; Auto with avl.
Apply eq_add_S ; Elim H8 ; Apply eq_add_S ; Elim H4.
Elim e0 ; Elim haut_node.
Elim H8 ; Auto with avl.
(* (avl_ins (node l g' d ga)) *)
Apply ins_ga ; Auto with avl.
Elim H4 ; Auto with avl.
Apply equiv_sup_g with g x ; Auto with avl.
(* (haut (node l g' d ga))=(S (haut (node l g d mi))) *)
Elim haut_node; Elim haut_node; Elim H4; Elim max_n_n.
Rewrite -> e0; Auto with avl.
(* (avl (node l g' d mi)) *)
Apply avl_node ; Auto with avl.
Apply bal_mi ; Auto with avl.
Elim H4; Auto with avl.
Apply equiv_sup_g with g x ; Auto with avl.
(* (haut (node l g' d mi))=(haut (node l g d dr)) *)
Elim haut_node; Elim haut_node; Elim H4; Elim max_n_Sn.
Elim e0 ; Auto with avl.
(* (avl (node l g d' des)) *)
Apply avl_node ; Auto with avl.
Apply bal_haut with g d ; Trivial with avl.
Apply equiv_inf_g with d x ; Auto with avl.
(* (haut (node l g d' des))=(haut (node l g d des)) *)
Simpl; Elim e0; Auto with avl.
(* (avl (node l g d' mi)) *)
Apply avl_node ; Auto with avl.
Apply bal_mi ; Auto with avl.
Rewrite -> H4; Auto with avl.
Apply equiv_inf_g with d x ; Auto with avl.
(* (haut (node l g d' mi))=(haut (node l g d ga)) *)
Simpl; Rewrite -> e0.
Rewrite -> H4.
Elim max_Sn_n; Auto with avl.
(* (avl_ins (node l g d' dr)) *)
Apply ins_dr ; Auto with avl.
Apply trans_equal with (S (haut d)); Auto with avl.
Apply equiv_inf_g with d x ; Auto with avl.
(* (haut (node l g d' dr))=(S (haut (node l g d mi))) *)
Elim haut_node; Elim haut_node; Rewrite -> H4.
Elim max_n_n; Rewrite e0; Auto with avl.
(* False *)
Absurd O=(S (haut d'd)); Auto with avl.
(* (avl (rot_gd m l g d'd n d'g1 d'g2 eqn)) *)
Apply avl_rotgd ; Auto with avl.
Elim (inft_node_inv l m (node n d'g1 d'g2 eqn) d'd ga); Auto with avl.
Apply equiv_inf_g with d x ; Auto with avl.
Simpl.
Rewrite -> H4.
Apply eq_add_S; Elim e0.
Elim haut_node.
Replace (S (max (haut (node n d'g1 d'g2 eqn)) (haut d'd))) with (max (S (haut (node n d'g1 d'g2 eqn))) (S (haut d'd))).
Elim H8.
Cut ((haut (node n d'g1 d'g2 eqn))=(S (max (haut d'g1) (haut d'g2)))); Auto with avl.
Auto with avl.
Apply eq_add_S; Rewrite -> H4.
Elim H8.
Apply eq_add_S; Elim e0.
Elim haut_node.
Replace (S (max (haut (node n d'g1 d'g2 eqn)) (haut d'd))) with (max (S (haut (node n d'g1 d'g2 eqn))) (S (haut d'd))).
Elim H8; Auto with avl.
Auto with avl.
(* (equiv x (node l g d dr) (rot_gd m l g d'd n d'g1 d'g2 eqn)) *)
Apply equiv_equiv_abe with (node l g (node m (node n d'g1 d'g2 eqn) d'd ga) dr) ; Auto with avl.
(* (haut (rot_gd m l g d'd n d'g1 d'g2 eqn))=(haut (node l g d dr)) *)
Elim haut_node; Elim haut_rotgd; Auto with avl.
Elim H4; Elim max_n_Sn.
Rewrite -> H4.
Elim e0.
(* Rewrite -> H8; Auto with avl. *)
Elim haut_node.
Replace (S (max (haut (node n d'g1 d'g2 eqn)) (haut d'd))) with (max (S (haut (node n d'g1 d'g2 eqn))) (S (haut d'd))); Auto with avl.
Elim H8; Auto with avl.
Rewrite -> H4.
Apply eq_add_S; Elim e0.
Elim haut_node.
Replace (S (max (haut (node n d'g1 d'g2 eqn)) (haut d'd))) with (max (S (haut (node n d'g1 d'g2 eqn))) (S (haut d'd))); Auto with avl.
Elim H8; Auto with avl.
Apply eq_add_S; Rewrite -> H4.
Apply eq_add_S; Elim e0.
Elim H8.
Elim haut_node.
Replace (S (max (haut (node n d'g1 d'g2 eqn)) (haut d'd))) with (max (S (haut (node n d'g1 d'g2 eqn))) (S (haut d'd))); Auto with avl.
Elim H8; Auto with avl.
(* False *)
Absurd O=(haut d); Auto with avl.
Elim H4; Auto with avl.
(* (avl (rot_g m l g d'd d'g)) *)
Apply avl_rotg ; Auto with avl.
Apply equiv_inf_g with d x ; Auto with avl.
Apply eq_add_S; Rewrite -> H4.
Apply eq_add_S; Elim e0; Simpl; Elim H8; Auto with avl.
(* (equiv x (node l g d dr) (rot_g m l g d'd d'g)) *)
Apply equiv_equiv_abe with (node l g (node m d'g d'd dr) dr) ; Auto with avl.
(* (haut (rot_g m l g d'd d'g))=(haut (node l g d dr)) *)
Elim haut_rotg.
Elim haut_node.
Elim H4; Elim max_n_Sn.
Rewrite -> H4.
Elim e0; Simpl.
Elim H8; Auto with avl.
Apply eq_add_S; Rewrite -> H4.
Apply eq_add_S; Elim e0; Simpl; Elim H8; Auto with avl.
Auto with avl.
Save.

End trees.

(* $Id: Avl_prog.v,v 1.6 1999/06/29 07:48:42 loiseleu Exp $ *)
