(* =========================================================================== *)
(* == Vérification formelle du tri fonctionnel par tas                      == *)
(* == Etude opérationnelle                                                  == *)
(* ==                                                                       == *)
(* == Pascal Manoury -- PPS, CNRS UMR 7126                                  == *)
(* ==                                                                       == *)
(* =========================================================================== *)


(* == Parametrized binary trees data type *)
v"
type 'a btree = Lf  | Br of 'a * ('a btree) * ('a btree)
" ;;

(* == Inserting function *)
v"
let rec ins_heap c a h =
  match h with
      Lf -> Br(a, Lf, Lf) 
    | Br(a0, h1, h2) ->  
	if (c a a0) then 
	  Br(a, h2, (ins_heap c a0 h1)) 
	else 
	  Br(a0, h2, (ins_heap c a h1)) 
";;
v"Total ins_heap";;
p"Induction h";;

 p"Auto";;

 p"Intros";;
 p"SymEval ins_heap";;
 p"TypeIf";;
  p"Auto";;
  p"Auto";;

(* == Maximal and minimal depth *)
v "
let rec hmax b =
  match b with
     Lf -> 0
  |  Br(a, b1, b2) -> S(max (hmax b1) (hmax b2))
";;
v"Total hmax";;
p"XTerm1 hmax";;

v "
let rec hmin b =
  match b with
     Lf -> 0
  |  Br(_, b1, b2) -> S(min (hmin b1) (hmin b2))
";;
v"Total hmin";;
p"XTerm1 hmin";;

(* == "Predecessor or equal" relation *)
v"
let pred_or_eq n m =
  ((n = m) || ((S n)=m))
";;
v"Total pred_or_eq";;
p"Auto";;

v"
Theorem pred_or_eq_idem :
  Forall n:nat. `(pred_or_eq n n)
";;
p"Intro";
p"SymEval pred_or_eq";;
p"RightOr 1";;
p"Auto";;

v"
Theorem pred_or_eq_S :
  Forall n:nat. `(pred_or_eq n (S n))
";;
p"Intro";
p"SymEval pred_or_eq";;
p"RightOr 2";;
p"Auto";;

v"
Theorem pred_or_eq_SS :
  Forall n:nat. Forall m:nat.
    `(pred_or_eq n m) -> `(pred_or_eq (S n) (S m))
";;
p"Intros";;
p"SymEvalHyp H3; pred_or_eq";;
p"SymEval pred_or_eq";;
p"LeftOr H4";;

 p"RightOr 1";;
 p"Rewrite H5";;
 p"Auto";;

 p"RightOr 2";;
 p"Rewrite H5";;
 p"Auto";;

v"
Theorem pred_or_eq_le :
  Forall n:nat. Forall m:nat. `(pred_or_eq n m) -> `(n <= m)
";;
p"Intros";;
p"SymEvalHyp H3; pred_or_eq";;
p"LeftOr H4";;

 p"Rewrite H5";;
 p"Apply le_refl";;

 p"RewriteRev H5";;
 p"Apply le_S";;

(* == Independance of depth to inserted variable 
   and minimal and maximal depth pseudo equations *)
*)
v"
Theorem hmin_ins_heap_x :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall b:'a btree.
  Forall x1:'a. Forall x2:'a. 
    `((hmin (ins_heap c x1 b)) = (hmin (ins_heap c x2 b)))
";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval ins_heap";;
 p"IntroIf";;

  p"SymEval hmin";;
  p"SymEval ins_heap; 2";;
  p"IntroIf";;

   p"SymEval hmin; 3";;
   p"Auto";;

   p"SymEval hmin; 3";;
   p"LeftForalls H4; c; x2; a6";;
   p"Rewrite H11";;
   p"Auto";;

  p"SymEval hmin";;
  p"SymEval ins_heap; 2";;
  p"IntroIf";;
   
   p"SymEval hmin; 3";;
   p"LeftForalls H4; c; x1; a6";;
   p"Rewrite H11";;
   p"Auto";;
   
   p"SymEval hmin; 3";;
   p"LeftForalls H4; c; x1; x2";;
   p"Rewrite H11";;
   p"Auto";;   

v"
Theorem hmin_ins_heap_eq :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall x:'a.
  Forall b1:'a btree. Forall b2:'a btree. Forall y:'a. 
    `((hmin (ins_heap c y (Br(x,b1,b2)))) 
     = (S(min (hmin b2) (hmin (ins_heap c x b1)))))
";;
p"Intros";;
p"SymEval ins_heap";;
p"IntroIf";;

 p"SymEval hmin";;
 p"Auto";;

 p"SymEval hmin";;
 p"Use hmin_ins_heap_x";;
 p"LeftForalls H7; 'a0; c; b1; y; x";;
 p"Rewrite H8";;
 p"Auto";;

v"
Theorem hmax_ins_heap_x :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall b:'a btree.
  Forall x1:'a. Forall x2:'a. 
    `((hmax (ins_heap c x1 b)) = (hmax (ins_heap c x2 b)))
";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval ins_heap";;
 p"IntroIf";;

  p"SymEval hmax";;
  p"SymEval ins_heap; 2";;
  p"IntroIf";;

   p"SymEval hmax; 3";;
   p"Auto";;

   p"SymEval hmax; 3";;
   p"LeftForalls H4; c; x2; a6";;
   p"Rewrite H11";;
   p"Auto";;

  p"SymEval hmax";;
  p"SymEval ins_heap; 2";;
  p"IntroIf";;

   p"SymEval hmax; 3";;
   p"LeftForalls H4; c; x1; a6";;
   p"Rewrite H11";;
   p"Auto";;
   
   p"SymEval hmax; 3";;
   p"LeftForalls H4; c; x1; x2";;
   p"Rewrite H11";;
   p"Auto";;   

v"
Theorem hmax_ins_heap_eq :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall x:'a.
  Forall b1:'a btree. Forall b2:'a btree. Forall y:'a. 
    `((hmax (ins_heap c y (Br(x,b1,b2)))) 
     = (S(max (hmax b2) (hmax (ins_heap c x b1)))))
";;
p"Intros";;
p"SymEval ins_heap";;
p"IntroIf";;

 p"SymEval hmax";;
 p"Auto";;

 p"SymEval hmax";;
 p"Use hmax_ins_heap_x";;
 p"LeftForalls H7; 'a0; c; b1; y; x";;
 p"Rewrite H8";;
 p"Auto";;

(* == Lemma 1, for 'hmin' and 'hmax' *)
v"
Theorem pred_or_eq_hmin_ins_heap :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall x:'a. Forall b:'a btree.
    `(pred_or_eq (hmin b) (hmin (ins_heap c x b)))
";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval hmin";; 
 p"Rewrite hmin_ins_heap_eq";; 
 p"Cut `(pred_or_eq (hmin b4) (hmin (ins_heap c a6 b4)))";;

  p"Auto";;

  p"SymEvalHyp H8; pred_or_eq";;
  p"LeftOr H9";;
 
   p"RewriteRev H10";;
   p"Rewrite min_com";;
   p"Apply pred_or_eq_idem";;

   p"RewriteRev H10";; 
   p"Rewrite min_com; 2";;
   p"SymEval min; 2";;
   p"IntroIf";;

    p"Rewrite le1_min_eq";;

     p"Apply lt_le";;  
     p"Use lt_trans";;
     p"LeftForalls H12; (hmin b4); (S(hmin b4))";;
     p"Apply H13";;
      p"ByHyp";;
      p"Apply lt_S";;

     p"Apply pred_or_eq_S";;

    p"Cut `((hmin b5) < (S(hmin b4))) Or `((hmin b5) = (S(hmin b4)))";;

     p"Apply le_lt_or_eq";;
     p"Apply not_lt_le";;
     p"ByHyp";;

     p"LeftOr H12";;

      p"Cut `((hmin b5) <= (hmin b4))";;

       p"Apply lt_S_le";;
       p"ByHyp";;

       p"Rewrite le2_min_eq";;
        p"ByHyp";;
        p"Apply pred_or_eq_idem";;

      p"Rewrite H13";;
      p"Rewrite H13";;
      p"Rewrite le1_min_eq";;
       p"Apply le_S";;
       p"Apply pred_or_eq_S";;

v"
Theorem pred_or_eq_hmax_ins_heap :
  Forall 'a:type. Forall c:'a -> 'a -> bool. Forall x:'a. Forall b:'a btree.
    `(pred_or_eq (hmax b) (hmax (ins_heap c x b)))
";;
p"Intro-n 2";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval hmax";; 
 p"Rewrite hmax_ins_heap_eq";; 
 p"LeftForall H5; a6";;
 p"SymEvalHyp H8; pred_or_eq";;
 p"LeftOr H9";;

   p"RewriteRev H10";;
   p"Rewrite max_com";;
   p"Apply pred_or_eq_idem";;

   p"RewriteRev H10";; 
   p"Rewrite max_com; 2";;
   p"SymEval max; 2";;
   p"IntroIf";;

    p"Rewrite le1_max_eq";;

     p"Use le_trans";;
     p"LeftForalls H12; (hmax b4); (S(hmax b4))";;
     p"Apply H13";;
      p"ByHyp";;
      p"Apply le_S";;

     p"Apply pred_or_eq_idem";;

    p"Rewrite le2_max_eq";;

     p"Apply lt_S_le";;
     p"Apply not_le_lt";;
     p"ByHyp";;

     p"Apply pred_or_eq_S";;

(* == "Well balanced" property *)
v"
let is_wb b =
   (pred_or_eq (hmin b) (hmax b))
" ;;
v"Total is_wb";;
p"Auto" ;;

(* == Binary trees structural isomorphism *)
v"
let rec biso b1 b2 =
  match b1, b2 with
    (Lf, Lf) -> true
  | ((Br(x1, b11, b12)), (Br(x2, b21, b22))) ->
      (biso b11 b21) && (biso b12 b22)
  | (b1, b2) -> false
";;
v"Total biso";;
p"Induction b1";;

 p"ByInduction b2";;

 p"Intros";;
 p"Case b2";;

  p"ByHyp";;

  p"Auto";;

  p"Intros";;
  p"SymEval biso";;
  p"Auto";;

v"
Theorem biso_refl :
  Forall 'a:type. Forall b: 'a btree. `(biso b b)
";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval biso";;
 p"IntroAnd";;
  p"ByHyp";;
  p"ByHyp";;

v"
Theorem biso_sym :
  Forall 'a:type. Forall b1: 'a btree. Forall b2: 'a btree.
   `(biso b1 b2) -> `(biso b2 b1)
";;
p"Induction b1";;

 p"Intro";;
 p"ByCase b2";;

 p"Intro-n 6";;
 p"Case b2";;

  p"ByHyp";;

  p"Auto";;

  p"Intros";;
  p"SymEvalHyp H10; biso";;
  p"LeftAnd H11";;
  p"SymEval biso";;
  p"IntroAnd";;
   p"Apply H4";;
   p"ByHyp";;
   p"Apply H5";;
   p"ByHyp";;

v"
Theorem biso_trans :
  Forall 'a:type. 
  Forall b1: 'a btree. Forall b2: 'a btree. Forall b3: 'a btree.
   `(biso b1 b2) -> `(biso b2 b3) -> `(biso b1 b3)
";;
p"Induction b1";;

 p"Intro";;
 p"Case b2";;

  p"ByHyp";;

  p"Intro";;
  p"ByCase b3";;

  p"Intros";;
  p"SymEvalHyp H6; biso";;
  p"Trivial";;

 p"Intro-n 6";;  
 p"Case b2";;

  p"ByHyp";;

  p"Intros";;
  p"SymEvalHyp H8; biso";;
  p"Trivial";;

  p"Intro-n 5";;
  p"Case b3";;

   p"ByHyp";;

   p"Intros";;
   p"SymEvalHyp H12; biso";;
   p"Trivial";;

   p"Intros";;
   p"SymEval biso";;
   p"SymEvalHyp H15; biso";;
   p"LeftAnd H16";;
   p"SymEvalHyp H11; biso";;
   p"LeftAnd H19";;
   p"IntroAnd";;

    p"LeftForalls H4; b7; b13";;
    p"Apply H22";;
     p"Apply H17";;
     p"Apply H20";;

    p"LeftForalls H5; b8; b14";;
    p"Apply H22";;
     p"Apply H18";;
     p"Apply H21";;

(* == Lemma 2 *)  
v"
Theorem biso_hmax :
  Forall 'a: type. Forall b1: 'a btree. Forall b2: 'a btree.
    `(biso b1 b2) -> `((hmax b1) = (hmax b2))
";;
p"Induction b1";;

 p"Intro";;
 p"ByCase b2";;

 p"Intro-n 6";;
 p"Case b2";;

  p"ByHyp";;

  p"Auto";;

  p"Intros";;
  p"SymEval hmax";;
  p"SymEval hmax; 3";;
  p"SymEvalHyp H10; biso";;
  p"LeftAnd H11";;
  p"LeftForall H4; b7";;
  p"Rewrite H14";;
   p"ByHyp";;
  p"LeftForall H5; b8";;
  p"Rewrite H15";;
   p"ByHyp";;
  p"Auto";;

v"
Theorem biso_hmin :
  Forall 'a: type. Forall b1: 'a btree. Forall b2: 'a btree.
    `(biso b1 b2) -> `((hmin b1) = (hmin b2))
";;
p"Induction b1";;

 p"Intro";;
 p"ByCase b2";;

 p"Intro-n 6";;
 p"Case b2";;

  p"ByHyp";;

  p"Auto";;

  p"Intros";;
  p"SymEval hmin";;
  p"SymEval hmin; 3";;
  p"SymEvalHyp H10; biso";;
  p"LeftAnd H11";;
  p"LeftForall H4; b7";;
  p"Rewrite H14";;
   p"ByHyp";;
  p"LeftForall H5; b8";;
  p"Rewrite H15";;
   p"ByHyp";;
  p"Auto";;

(* == Lemma 3 and indepence corolary *)
v"
Theorem biso_ins_heap :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. 
  Forall x1:'a. Forall x2:'a.
  Forall b1: 'a btree. Forall b2: 'a btree.
   `(biso b1 b2) -> `(biso (ins_heap c x1 b1) (ins_heap c x2 b2))
";;
p"Intro-n 2";;
p"Induction b1";;

 p"Intro-n 3";;
 p"ByCase b2";;

 p"Intro-n 8";;
 p"Case b2";;

  p"ByHyp";;

  p"Auto";;

  p"Intros";;
  p"SymEvalHyp H13; biso";;
  p"LeftAnd H14";;
  p"SymEval ins_heap";;
  p"IntroIf";;

   p"SymEval ins_heap; 2";;
   p"IntroIf";;

    p"SymEval biso";;
    p"IntroAnd";;
     p"ByHyp";;
     p"Apply H5";;
     p"ByHyp";;

    p"SymEval biso";;
    p"IntroAnd";;
     p"ByHyp";;
     p"Apply H5";;
     p"ByHyp";;

   p"SymEval ins_heap; 2";;
   p"IntroIf";;

    p"SymEval biso";;
    p"IntroAnd";;
     p"ByHyp";;
     p"Apply H5";;
     p"ByHyp";;

    p"SymEval biso";;
    p"IntroAnd";;
     p"ByHyp";;
     p"Apply H5";;
     p"ByHyp";;

v"
Theorem biso_ins_heap_x :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. Forall x1:'a. Forall x2:'a.
  Forall b: 'a btree.
   `(biso (ins_heap c x1 b) (ins_heap c x2 b))
";;
p"Intros";;
p"Apply biso_ins_heap";;
p"Apply biso_refl";;

(* == "Adequat trees" property *)
v"
let rec ins_heap_wb c x b =
  match b with
    Lf -> true
  | Br(y,b1,b2) -> 
     (ins_heap_wb c x b1) && 
     ((biso b2 b1) || (biso b2 (ins_heap c x b1))) 
";;
v"Total ins_heap_wb";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEval ins_heap_wb";;
 p"Auto";;

(* == Lemma 4 *)
v"
Theorem biso_ins_heap_wb :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. Forall x:'a. 
  Forall b1: 'a btree. Forall b2: 'a btree.
    `(biso b1 b2) -> `(ins_heap_wb c x b1) -> `(ins_heap_wb c x b2)
";;
p"Intro-n 2";;
p"Induction b1";; 

 p"Intro-n 2";;
 p"ByCase b2";;

 p"Intro-n 7";;
 p"Case b2";;

  p"ByHyp";;

  p"Intros";;
  p"SymEvalHyp H9; biso";;
  p"Trivial";;

  p"Intros";;
  p"SymEvalHyp H12; biso";;
  p"LeftAnd H14";;
  p"SymEvalHyp H13; ins_heap_wb";;
  p"LeftAnd H17";;
  p"SymEval ins_heap_wb";;
  p"IntroAnd";;

   p"Apply H5";;
    p"ByHyp";;
    p"ByHyp";;

   p"LeftOr H19";;

    p"RightOr 1";;
    p"Use biso_trans";;
    p"LeftForalls H21; 'a0; b8; b4; b13";;
    p"Apply H22";;

     p"ByHyp";;

     p"LeftForalls H21; 'a0; b8; b5; b4";;
     p"Apply H23";;

      p"ByHyp";;

      p"Apply biso_sym";;
      p"ByHyp";;

    p"RightOr 2";;
    p"Use biso_trans";;
    p"LeftForalls H21; 'a0; b8; (ins_heap c x b4)";;
    p"Apply H22";;

     p"Apply biso_ins_heap";;
     p"Apply H15";;

     p"LeftForalls H21; 'a0; b8; b5";;
     p"Apply H23";;

      p"Apply H20";;    

      p"Apply biso_sym";;
      p"Apply H16";;

(* == Technical lemma 5 *)
v"
Theorem hmax_ins_heap_eq_S_hmax__hmin_eq_hmax :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. Forall x:'a. Forall b: 'a btree.
    `(ins_heap_wb c x b) -> `((hmax (ins_heap c x b)) = (S(hmax b)))
     -> `((hmin b) = (hmax b))
";;
p"Intro-n 2";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEvalHyp H8; ins_heap_wb";;
 p"LeftAnd H10";;
 p"LeftOr H12";;

  (* `((biso b5 b4)) *)
  p"SymEval hmin";;
  p"SymEval hmax";;
  p"SymEval =";;
  p"Use biso_hmin";;
  p"LeftForalls H14; 'a0; b5; b4";;
  p"LeftArrow H15";;
   p"ByHyp";;
  p"Rewrite H16";;
  p"Rewrite min_idem";;
  p"Use biso_hmax";;
  p"LeftForalls H17; 'a0; b5; b4";;
  p"LeftArrow H18";;
   p"ByHyp";;
  p"Rewrite H19";;
  p"Rewrite max_idem";;
  p"LeftForall H5; x";;
  p"Rewrite H20";;

   p"LeftRewrite H9; hmax_ins_heap_eq";;
   p"SymEvalHyp H21; =";;
   p"LeftRewrite H22; H19";;
   p"LeftRewrite H23; le1_max_eq";;
    p"Apply pred_or_eq_le";;
    p"Apply pred_or_eq_hmax_ins_heap";;
   p"SymEvalHyp H24; hmax; 2";;
   p"LeftRewrite H25; H19";;
   p"LeftRewrite H26; max_idem";;
   p"Use hmax_ins_heap_x";;
   p"LeftForalls H28; 'a0; c; b4; x; a6";;  
   p"Rewrite H29";;
   p"Apply H27";;

   p"ByHyp";;

   p"Auto";;

  (* `((biso b5 (ins_heap c x b4))) *)
  p"RightNotRule `((hmax (ins_heap c a6 b4)) = (S(hmax (ins_heap c a6 b4))))";;
   p"Apply not_eq_S";;

   p"LeftRewrite H9; hmax_ins_heap_eq";;
   p"SymEvalHyp H14; =";;
   p"SymEvalHyp H15; hmax; 3";;
   p"Use biso_hmax";;
   p"LeftForalls H17; 'a0; b5; (ins_heap c a6 b4)";;
   p"LeftArrow H18";;

    p"Use biso_trans";;  
    p"LeftForalls H19; 'a0; b5; (ins_heap c x b4)";;
    p"Apply H20";;
     p"Apply biso_ins_heap_x";;
     p"Apply H13";;

    p"LeftRewrite H16; H19";;
    p"LeftRewrite H20; max_idem";;
    p"LeftRewrite H21; H19";;
    p"Use le1_max_eq";;
    p"LeftForalls H23; (hmax b4); (hmax (ins_heap c a6 b4))";;
    p"LeftRewrite H22; H24";;
  
     p"Apply pred_or_eq_le";;
     p"Apply pred_or_eq_hmax_ins_heap";;

     p"ByHyp";;     

(* == Theorem 1 *)
v"
Theorem ins_heap_wb_ins_heap :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. Forall x:'a. Forall b: 'a btree.
    `(ins_heap_wb c x b) -> `(ins_heap_wb c x (ins_heap c x b))
";;
p"Intro-n 2";;
p"Induction b";; 

 p"Auto";;

 p"Intros";;
 p"SymEvalHyp H8; ins_heap_wb";;
 p"LeftAnd H9";;
 p"SymEval ins_heap";;

 p"IntroIf";;

  p"SymEval ins_heap_wb";;
  p"LeftOr H11";;

   p"IntroAnd";;

    p"Use biso_ins_heap_wb";;
    p"LeftForalls H14; 'a0; c; x; b4";;
    p"Apply H15";;
     p"Apply H10";;
     p"Apply biso_sym";;
     p"ByHyp";;

    p"RightOr 2";;
    p"Use biso_trans";;
    p"LeftForalls H14; 'a0; (ins_heap c a6 b4);(ins_heap c x b4)";;
    p"Apply H15";;

     p"Apply biso_ins_heap";;
     p"Apply biso_sym";;
     p"Apply H13";;

     p"Apply biso_ins_heap_x";;

   p"IntroAnd";;

    p"Use biso_ins_heap_wb";;
    p"LeftForalls H14; 'a0; c; x; (ins_heap c x b4); b5";;
    p"Apply H15";;

     p"Apply H5";;
     p"ByHyp";;

     p"Apply biso_sym";;
     p"Apply H13";;

    p"RightOr 1";;
    p"Use biso_trans";;
    p"LeftForalls H14; 'a0; (ins_heap c a6 b4); (ins_heap c x b4)";;
    p"Apply H15";;

     p"Apply biso_sym";;
     p"Apply H13";;

     p"Apply biso_ins_heap_x";;

  p"SymEval ins_heap_wb";;
  p"LeftOr H11";;

   p"IntroAnd";;

    p"Use biso_ins_heap_wb";;
    p"LeftForalls H14; 'a0; c; x; b4";;
    p"Apply H15";;
     p"Apply H10";;
     p"Apply biso_sym";;
     p"ByHyp";;

    p"RightOr 2";;
    p"Apply biso_ins_heap";;
    p"Apply biso_sym";;
    p"ByHyp";;

   p"IntroAnd";;

    p"Use biso_ins_heap_wb";;
    p"LeftForalls H14; 'a0; c; x; (ins_heap c x b4); b5";;
    p"Apply H15";;

     p"Apply H5";;
     p"Apply H10";;

     p"Apply biso_sym";;
     p"Apply H13";;

    p"RightOr 1";;
    p"Apply biso_sym";;
    p"ByHyp";;

(* == Theorem 2 *)
v"
Theorem ins_heap_wb_is_wb :
  Forall 'a:type. Forall c: 'a -> 'a -> bool. Forall x:'a. Forall b: 'a btree.
    `(ins_heap_wb c x b) -> `(is_wb b)
";;
p"Intro-n 2";;
p"Induction b";;

 p"Auto";;

 p"Intros";;
 p"SymEvalHyp H8; ins_heap_wb";;
 p"LeftAnd H9";;
 p"SymEval is_wb";;
 p"SymEval hmin";;
 p"SymEval hmax";;
 p"Apply pred_or_eq_SS";;
 p"LeftOr H11";;

  p"Use biso_hmin";;
  p"LeftForalls H13; 'a0; b5; b4";;
  p"Rewrite H14";;
   p"ByHyp";;
  p"Rewrite min_idem";;
  p"Use biso_hmax";;
  p"LeftForalls H15; 'a0; b5; b4";;
  p"Rewrite H16";;
   p"ByHyp";;
  p"Rewrite max_idem";;
  p"LeftForall H5; x";;
  p"SymEvalHyp H17; is_wb";; 
  p"Auto";;

  p"Use biso_hmin";;
  p"LeftForalls H13; 'a0; b5; (ins_heap c x b4)";;
  p"Rewrite H14";;
   p"ByHyp";;
  p"Use biso_hmax";;
  p"LeftForalls H15; 'a0; b5; (ins_heap c x b4)";;
  p"Rewrite H16";;
   p"ByHyp";;
  p"Rewrite le1_min_eq";;
   p"Apply pred_or_eq_le";;
   p"Apply pred_or_eq_hmin_ins_heap";;
  p"Rewrite le1_max_eq";;
   p"Apply pred_or_eq_le";;
   p"Apply pred_or_eq_hmax_ins_heap";;
  p"LeftForall H5; x";;
  p"LeftArrow H17; H10";;

   p"ByHyp";;

   p"SymEvalHyp H18; is_wb";;
   p"SymEvalHyp H19; pred_or_eq";;
   p"LeftOr H20";;

    p"Rewrite H21";;
    p"Apply pred_or_eq_hmax_ins_heap";;

    p"Use pred_or_eq_hmax_ins_heap";; 
    p"LeftForalls H22; 'a0; c; x; b4";;
    p"SymEvalHyp H23; pred_or_eq";;
    p"LeftOr H24";;

     p"RewriteRev H25";;
     p"RewriteRev H21";;
     p"Apply pred_or_eq_S";;
 
     p"RightNotRule `(((S((hmin b4))) = (hmax b4)))";;   

      p"Use hmax_ins_heap_eq_S_hmax__hmin_eq_hmax";;
      p"LeftForalls H26; 'a0; c; x; b4";;
      p"Rewrite H27";;

       p"Rewrite H25";;
       p"Auto";;

       p"ByHyp";;

       p"Apply not_S_eq";;

      p"ByHyp";;

(* == Heap sort 
v"
let c x1 x2 = (x2 <= x2)
";;
v"Total c";;
p"Auto";;

v"
let rec list_to_btree xs =
  match xs with
    [] -> Lf
  | x::xs -> (ins_heap c x (list_to_btree xs))
";;
v"Total list_to_btree";;
p"Induction xs";;

 p"Auto";;

 p"Intros";;
 p"SymEval list_to_btree";;
 p"Auto";;

v "
let rec btree_to_list t = 
  match t with
      Lf -> []
    | Br(a,Lf,t2) -> a::(btree_to_list t2)
    | Br(a1, (Br(a2, t1, t2)), t3)
       -> (btree_to_list (Br(a1, t1, (Br(a2, t2, t3)))))
" ;;
v"Total btree_to_list" ;;
p "Induction t" ;;

 p"Auto" ;;

 p"Intro-n 4" ;;
 p"Generalize b5" ;;
 p"Generalize a6" ;;
 p"Generalize b4" ;;
 p"ByInduction b4" ;;

v"
let heap_sort xs =
  (btree_to_list (list_to_btree xs))
";;

v"
let rec btree_mem = fun x t ->
  match t with 
      Lf -> false
    | Br(y, t1, t2) -> (x = y) || (btree_mem x t1) || (btree_mem x t2)
" ;;
v"Total btree_mem" ;;
p "Intro-n 2" ;;
p "XTerm1 btree_mem" ;;

(* A faire avec rewrite_AC *)
v"
Theorem btree_mem_assoc:
  Forall 'a:type. Forall x:'a. Forall x1:'a. Forall x2:'a.
  Forall t1:'a btree. Forall t2:'a btree. Forall t3:'a btree.
    `((btree_mem x (Br(x1,(Br(x2,t1,t2)),t3)))
     =(btree_mem x (Br(x1,t1,(Br(x2,t2,t3))))))
";;
p "Intros" ;;
p "SymEval btree_mem" ;;
p "SymEval btree_mem; 3" ;;
p "Apply eq_fun" ;;
p "SymEval btree_mem" ;;
p "Rewrite or_com; 4" ;;
p "SymEval btree_mem; 4" ;;
p "Rewrite or_assoc; 1" ;;
p "Rewrite or_assoc; 2" ;;
p "Apply eq_fun" ;;
p "Rewrite or_com; 2";;
p "Rewrite or_assoc; 1" ;;
p "Rewrite or_assoc; 1" ;;
p "Apply eq_fun" ;;
p "Rewrite or_com; 1";;
p "Auto" ;;

v"
Theorem mem_btree_mem_list:
  Forall 'a:type. Forall x:'a. Forall t:'a btree.
   `((btree_mem x t) = (list_mem x (btree_to_list t)))
" ;;
p"Intro-n 2" ;;
p"ByInduction" ;;  

 p"Auto" ;;

 p"Intro-n 4" ;;
 p"Generalize b5" ;;
 p"Generalize a4" ;;
 p"Generalize b4" ;;
 p"Rec" ;;

  p"Intros";;
  p"SymEval btree_mem" ;;
  p"SymEval btree_to_list" ;;
  p"SymEval list_mem" ;;
  p"SymEval btree_mem; 1" ;;
  p"SymEval ||; 2" ;;
  p"Rewrite H8; 1" ;;
  p"Auto" ;;

  p"Intros" ;;
  p"SymEval btree_to_list" ;;
  p"Rewrite btree_mem_assoc; 1" ;;
  p"Rewrite H9; 1" ;;
   p"Auto" ;;
   p"Auto" ;;
== *)