(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                               Heap_prog.v                                *)
(****************************************************************************)

Require Export List.


Inductive Tree : Set :=
      Tree_Leaf : Tree
    | Tree_Node : A -> Tree -> Tree -> Tree.

(*****************************)
(* A decidable relation on A *)
(*****************************)

Axiom   inf : A -> A -> Prop.

Axiom inf_total : (x,y:A){(inf x y)}+{(inf y x)}.
Axiom inf_tran : (x,y,z:A)(inf x y)->(inf y z)->(inf x z).
Axiom inf_refl : (x:A)(inf x x).

Hint inf_refl inf_total.


Definition Tree_Lowert
  [a:A][t:Tree](<Prop>Cases t of
                        Tree_Leaf => True
                    | (Tree_Node b _ _) => (inf a b) end).

Lemma nil_is_low : (a:A)(Tree_Lowert a Tree_Leaf).
Simpl;Auto.
Save.

Lemma node_is_low : (a:A)(b:A)(T1:Tree)(T2:Tree)
     (inf a b)->(Tree_Lowert a (Tree_Node b T1 T2)).
Simpl;Auto.
Save.

Hint nil_is_low node_is_low.

(*******************************)
(* addition of natural numbers *)
(*******************************)

Fixpoint add [n,m:nat] : nat :=
      Cases m of
	O => n
      | (S p) =>(S (add n p))
      end.

Lemma eq_ad_O : (n:nat)((add O n)=n).
Induction n ; Simpl ; Auto.
Save.
Hint eq_ad_O.

Lemma sym_add : (n:nat)(m:nat)((add n m)=(add m n)).
Induction n ; Simpl ; Intros; Auto.
Elim (H m).
Elim m ; Simpl ; Auto.
Save.
Hint sym_add.

Lemma add_ass : (n,m,p:nat)(add n (add m p))=(add (add n m) p).
Induction p; Simpl; Auto.
Save.
Hint add_ass.

Lemma ass_add : (n,m,p:nat)(add (add n m) p)=(add n (add m p)).
Auto.
Save.
Hint ass_add.

Lemma add_simpl_d : (n,m,p:nat)(n=m)->(add n p)=(add m p).
Intros n m p H.
Elim p;Simpl;Auto.
Save.
Hint add_simpl_d.

Lemma add_simpl_g : (n,m,p:nat)(n=m)->(add p n)=(add p m).
Intros.
Elim (sym_add n p).
Elim (sym_add m p).
Auto.
Save.
Hint add_simpl_g.

Lemma add_simpl : (n,m,p,q:nat)
             (n=m)->(p=q)->(add n p)=(add m q).
Intros n m p q H H0.
Elim H.
Elim H0.
Auto.
Save.
Hint add_simpl.

Definition eq_fun := [f1:A->nat][f2:A->nat]((a:A)((f1 a)=(f2 a))).

Definition fun_add := [f1:A->nat][f2:A->nat][a:A](add (f1 a)(f2 a)).

(****************************)
(*    The heap property     *)
(****************************)

Inductive is_heap : Tree -> Prop :=
      nil_is_heap : (is_heap Tree_Leaf)
    | node_is_heap : (a:A)(T1:Tree)(T2:Tree)
                                (Tree_Lowert a T1)->
                                (Tree_Lowert a T2)->
                                (is_heap T1)->(is_heap T2)->
                                        (is_heap (Tree_Node a T1 T2)).

Hint nil_is_heap node_is_heap.

Definition heap_inv
[t:Tree](Cases t of
          Tree_Leaf => True
         | (Tree_Node a G D) => (Tree_Lowert a G)/\(Tree_Lowert a D)
		                      /\(is_heap G)/\(is_heap D) end).


Lemma is_heap_inv : (T:Tree)(is_heap T)->(heap_inv T).
Induction 1;Simpl;Auto.
Save.

Lemma is_heap_rec : (P:Tree->Set)
        (P Tree_Leaf)->
         ((a:A)
           (T1:Tree)
            (T2:Tree)
             (Tree_Lowert a T1)->
              (Tree_Lowert a T2)->
               (is_heap T1)->
                (P T1)->(is_heap T2)->(P T2)->(P (Tree_Node a T1 T2)))
         ->(y:Tree)(is_heap y)->(P y).
Realizer [P:Set][H:P][H0:A->Tree->Tree->P->P->P][y:Tree]
                    Match y with
		       H
                       [a,G,PG,D,PD](H0 a G D PG PD)
		    end.
Program_all.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Induction 2.
Induction 2; Auto.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Induction 2.
Induction 2; Auto.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Induction 2.
Induction 2; Auto.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Induction 2.
Induction 2; Auto.
Elim (is_heap_inv (Tree_Node a t0 t1)); Trivial.
Induction 2.
Induction 2; Auto.
Save.

Lemma low_trans : (T:Tree)(a:A)(b:A)(inf a b)->(Tree_Lowert b T)->(Tree_Lowert a T).
Intro.
Elim T;Intros;Auto.
Simpl.
Apply inf_tran with b;Auto.
Save.
(*Hint low_trans.*)

(**************************)
(* caracteristic function *)
(**************************)

Axiom carac : A->A->nat.

Fixpoint content [t:Tree] : A -> nat :=
      [a:A] Cases t of
              Tree_Leaf =>O
            | (Tree_Node b T1 T2) =>
                            (fun_add (content T1) 
				(fun_add (content T2) (carac b)) a)
            end.

(****************************)
(* equivalence of two trees *)
(****************************)

Definition equiv_Tree := [T1:Tree][T2:Tree]
                        (a:A)((content T1 a)=(content T2 a)).


(**********************************)
(* induction principle over trees *)
(**********************************)

Inductive Lem_spec [a:A;T:Tree] : Set :=
    Lem_exist : (T1:Tree)(is_heap T1)->
                            (eq_fun (content T1)
                                    (fun_add (content T)(carac a)))->
                                ((b:A)(inf b a)->(Tree_Lowert b T)->
                                            (Tree_Lowert b T1))->
                                    (Lem_spec a T).

Lemma insert : (T:Tree)(is_heap T)->(a:A)(Lem_spec a T).
Realizer [T:Tree][{H:(is_heap T)}]
            (is_heap_rec A->Tree
               [a:A](Tree_Node a Tree_Leaf Tree_Leaf)
               [a:A][T1,T2:Tree][H0,H1:A->Tree][a0:A]
                    if (inf_total a a0) then
				 (Tree_Node a T2 (H0 a0))
			   else (Tree_Node a0 T2 (H0 a))
               T).
Program_all.
Simpl;Unfold eq_fun; Unfold fun_add;Auto.
Simpl;Unfold eq_fun; Unfold fun_add;Intros.
Elim ass_add.
Elim (sym_add (content T0 a1)(content T2 a1)).
Elim (add_ass (content T0 a1)(content T2 a1)(carac a a1)).
Elim (sym_add (carac a0 a1)
              (add (content T1 a1) (add (content T2 a1) (carac a a1)))).
Elim (ass_add (carac a0 a1)(content T1 a1)(add (content T2 a1) (carac a a1))).
Apply add_simpl_d.
Elim (sym_add (content T1 a1)(carac a0 a1)).
Exact (e a1).
Apply node_is_heap;Auto.
Apply low_trans with a;Auto.
Apply t;Auto.
Apply low_trans with a;Auto.
Simpl;Unfold eq_fun; Unfold fun_add;Intros.
Elim ass_add.
Apply add_simpl_d.
Elim ass_add.
Elim (sym_add (content T2 a1) (content T1 a1)).
Elim add_ass.
Apply add_simpl_g.
Exact (e a1).
Save.

(**********************)
(* contents of a list *)
(**********************)

Fixpoint list_content [l:list] : A->nat :=
   [a:A] Cases l of
            nil => O
         | (cons b l) =>(fun_add (carac b) (list_content l) a)
        end.

(*******************************)
(* building a heap from a list *)
(*******************************)

Inductive build_heap [l:list] : Set :=
heap_exist : (T:Tree)(is_heap T)->(eq_fun (list_content l)(content T))->
                                             (build_heap l).

Lemma list_to_heap : (l:list)(build_heap l).
Realizer [l:list]Match l with
		     Tree_Leaf
                     [a,y,H](insert H a)
		   end.
Program_all.
Simpl;Unfold eq_fun;Auto.
Simpl;Unfold eq_fun; Unfold fun_add;Intros.
Rewrite -> (e a0).
Elim (sym_add (content T a0)(carac a a0)).
Apply sym_equal.
Exact (e0 a0).
Save.

(*****************)
(* low for lists *)
(*****************)

Inductive list_Lowert [a:A] : list -> Prop :=
      nil_low : (list_Lowert a nil)
    | cons_low : (b:A)(l:list)(inf a b)->(list_Lowert a (cons b l)).
Hint nil_low cons_low.

Definition list_Lowert2 :=
   [a:A][l:list](Cases l of 
                      nil => True 
                  | (cons b _) => (inf a b) end).

Lemma low2_low : (a:A)(l:list)(list_Lowert2 a l)->(list_Lowert a l).
Do 2 Intro.
Elim l;Simpl;Auto.
Save.

Lemma low_low2 : (a:A)(l:list)(list_Lowert a l)->(list_Lowert2 a l).
Intros a l p.
Elim p;Intros;Simpl;Auto.
Save.


(**************************************)
(* definition for a list to be sorted *)
(**************************************)

Inductive sort : list -> Prop :=
      nil_sort : (sort nil)
    | cons_sort : (a:A)(l:list)(sort l)->(list_Lowert a l)->(sort (cons a l)).
Hint nil_sort cons_sort.

Definition sort_inv
[l:list](Cases l of
                 nil => True 
          |  (cons a l) => (sort l)/\(list_Lowert a l) end).


Lemma sort_sort_inv : (l:list)(sort l)->(sort_inv l).
Induction 1;Simpl;Auto.
Save.

Lemma sort_rec : (P:list->Set)
        (P nil)->
         ((a:A)
           (l:list)(sort l)->(P l)->(list_Lowert a l)->(P (cons a l)))
         ->(y:list)(sort y)->(P y).
Realizer [P:Set][H:P][H0:A->list->P->P][y:list]
                 Match y with
		    H
                    [a,l,Pl](H0 a l Pl)
		 end.
Program_all.
Elim (sort_sort_inv (cons a l0)); Auto.
Elim (sort_sort_inv (cons a l0)); Auto.
Elim (sort_sort_inv (cons a l0)); Auto.
Save.

(****************************)
(* merging two sorted lists *)
(****************************)

Inductive merge_lem [l1:list;l2:list] :Set :=
merge_exist : (l:list)(sort l)->
                        (eq_fun(list_content l)
                               (fun_add(list_content l1)
                                       (list_content l2)))->
                            ((a:A)(list_Lowert a l1)->(list_Lowert a l2)->
                                    (list_Lowert a l))->
                                            (merge_lem l1 l2).

Section heapmerge.

Local merge_existc := [l1:list][l2:list][l:list](merge_exist l1 l2 l).

Lemma merge : (l1:list)(sort l1)->(l2:list)(sort l2)->(merge_lem l1 l2).
Realizer [l:list][{H:(sort l)}]
           (sort_rec list->list
	      [l1:list]l1
              [a:A][l1:list][H0:list->list][l2:list][{H':(sort l2)}]
                  (sort_rec list
                     (cons a l1)
                     [a0:A][l3,l4:list]
                         if (inf_total a a0) then
                                    (cons a (H0 (cons a0 l3)))
                               else (cons a0 l4)
                     l2)
              l).
Program_all.
Simpl;Unfold eq_fun fun_add;Auto.
Simpl;Unfold eq_fun fun_add;Auto.
Simpl; Unfold eq_fun fun_add;Intros.
Elim (add_ass (carac a a1)
                 (list_content l1 a1) (add (carac a0 a1) (list_content l3 a1))).
Apply add_simpl_g.
Exact (e0 a1).
Intros.
Apply low2_low.
Simpl.
Cut (list_Lowert2 a1 (cons a l1)).
Simpl; Auto.
Apply low_low2; Assumption.
Simpl;Unfold eq_fun fun_add;Intros.
Elim (sym_add (list_content l3 a1) (carac a0 a1)).
Elim (sym_add (list_content l0 a1) (carac a0 a1)).
Elim (ass_add (add (carac a a1) (list_content l1 a1)) (list_content l3 a1)
                 (carac a0 a1)).
Apply add_simpl_d.
Exact (e a1).
Intros;Apply low2_low.
Simpl.
Cut (list_Lowert2 a1 (cons a0 l3));Auto.
Apply low_low2; Assumption.
Save.

End heapmerge.

(****************************)
(* building the sorted list *)
(****************************)

Inductive flat_lem [T:Tree] : Set :=
flat_exist : (l:list)(sort l)->((a:A)(Tree_Lowert a T)->(list_Lowert a l))->
                                  (eq_fun (content T)(list_content l))->
                                     (flat_lem T).

Section h2l.

Local flat_existc := [T:Tree][l:list](flat_exist T l).

Lemma heap_to_list : (T:Tree)(is_heap T)->(flat_lem T).
Realizer [T:Tree][{H:(is_heap T)}]
		(is_heap_rec list 
		     nil
                     [a:A][T1,T2:Tree][l1,l2:list](cons a (merge l1 l2))
                 T).
Program_all.
Simpl;Unfold eq_fun fun_add;Auto.
Simpl;Unfold eq_fun fun_add;Intro.
Elim (sym_add (list_content l5 a0) (carac a a0)).
Elim (ass_add (content T1 a0) (content T2 a0) (carac a a0)).
Apply add_simpl_d.
Replace (list_content l5 a0) 
    with (add (list_content l0 a0) (list_content l3 a0)).
Apply add_simpl.
Exact (e a0).
Exact (e0 a0).
Apply sym_equal.
Exact (e1 a0).
Save.

End h2l.

Theorem heapsort :
  (l:list){m:list|(sort m)&(eq_fun (list_content l) (list_content m))}.
Realizer [l:list](heap_to_list (list_to_heap l)).
Program_all.
Unfold eq_fun;Intro.
Apply trans_equal with (content T a).
Exact (e a).
Exact (e0 a).
Save.



(* $Id: Heap_prog.v,v 1.3 1998/04/30 16:45:48 mohring Exp $ *)
