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

(* A development of Treesort on Heap trees *)

(* G. Huet 1-9-95 uses Multiset *)

Require Generic.
Require A_total_ordering.
Require List_of_A.
Require Multiset_of_A.
Require Permutation.
Require Sorting.

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

(*******************************************)
(* a is lower than a Tree T if T is a Leaf *)
(*      or T is a Node holding b>a         *)
(*******************************************)

Fixpoint inf_Tree [a:A; t:Tree]: Prop :=
 Cases t of 
   Tree_Leaf           => True
 | (Tree_Node b T1 T2) => (inf a b)
 end.

Lemma inf_Tree_Leaf : (a:A)(inf_Tree a Tree_Leaf).
Proof.
Simpl; Auto.
Qed.

Lemma inf_Tree_Node : (a,b:A)(G,D:Tree)(inf a b) ->
                        (inf_Tree a (Tree_Node b G D)).
Proof.
Simpl; Auto.
Qed.

Hint inf_Tree_Leaf inf_Tree_Node.


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

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

Hint nil_is_heap node_is_heap.

Lemma invert_heap : (a:A)(T1,T2:Tree)(is_heap (Tree_Node a T1 T2))->
  (inf_Tree a T1) /\ (inf_Tree a T2) /\
  (is_heap T1) /\ (is_heap T2).
Proof.
Intros; Inversion H; Auto.
Qed.

(* This lemma ought to be generated automatically by the Inversion tools *)
Lemma is_heap_rec : (P:Tree->Set)
        (P Tree_Leaf)->
         ((a:A)
           (T1:Tree)
            (T2:Tree)
             (inf_Tree a T1)->
              (inf_Tree a T2)->
               (is_heap T1)->
                (P T1)->(is_heap T2)->(P T2)->(P (Tree_Node a T1 T2)))
         -> (T:Tree)(is_heap T) -> (P T).
Proof.
Induction T; Auto.
Intros a G PG D PD PN. 
Elim (invert_heap a G D); Auto.
Intros H1 H2; Elim H2; Intros H3 H4; Elim H4; Intros.
Apply H0; Auto.
Qed.

Lemma low_trans : 
  (T:Tree)(a,b:A)(inf a b) -> (inf_Tree b T) -> (inf_Tree a T).
Proof.
Induction T; Auto.
Intros; Simpl; Apply inf_tran with b; Auto.
Qed.

(************************************)
(* contents of a tree as a multiset *)
(************************************)

(* Nota Bene : In what follows the definition of SingletonBag
   in not used. Actually, we could just take as postulate:
   Parameter SingletonBag : A->multiset.  *)

Fixpoint  contents [t:Tree] :multiset :=
 Cases t of
   Tree_Leaf           => EmptyBag
 | (Tree_Node a t1 t2) => (munion (contents t1) 
                          (munion (contents t2) (SingletonBag a)))
end.


(*******************************************************************)
(* equivalence of two trees is equality of corresponding multisets *)
(*******************************************************************)

Definition equiv_Tree := [t1,t2:Tree](meq (contents t1) (contents t2)).


(***********************************)
(* specification of heap insertion *)
(***********************************)

Inductive insert_spec [a:A; T:Tree] : Set :=
   insert_exist : (T1:Tree)(is_heap T1) ->
                  (meq (contents T1) (munion (contents T) (SingletonBag a))) ->
                  ((b:A)(inf b a)->(inf_Tree b T)->(inf_Tree b T1)) ->
                  (insert_spec a T).


Lemma insert : (T:Tree)(is_heap T) -> (a:A)(insert_spec a T).
Proof.
Induction 1; Intros.
Apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); Auto.
Simpl; Unfold meq munion; Auto.
Elim (inf_total a a0); Intros.
Elim (H3 a0); Intros.
Apply insert_exist with (Tree_Node a T2 T0); Auto.
Simpl; Apply treesort_twist1; Trivial. 
Elim (H3 a); Intros T3 HeapT3 ConT3 Inf.
Apply insert_exist with (Tree_Node a0 T2 T3); Auto.
Apply node_is_heap; Auto.
Apply low_trans with a; Auto.
Apply Inf; Auto.
Apply low_trans with a; Auto.
Simpl; Apply treesort_twist2; Trivial. 
Qed.

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

Inductive build_heap [l:list] : Set :=
   heap_exist : (T:Tree)(is_heap T) ->
                (meq (list_contents l)(contents T)) ->
                (build_heap l).

Lemma list_to_heap : (l:list)(build_heap l).
Proof.
Induction l.
Apply (heap_exist nil Tree_Leaf); Auto.
Simpl; Unfold meq; Auto.
Induction 1.
Intros T i m; Elim (insert T i a).
Intros; Apply heap_exist with T1; Simpl; Auto.
Apply meq_trans with (munion (contents T) (SingletonBag a)).
Apply meq_trans with (munion (SingletonBag a) (contents T)).
Apply meq_right; Trivial.
Apply munion_comm.
Apply meq_sym; Trivial.
Qed.


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

Inductive flat_spec [T:Tree] : Set :=
 flat_exist : (l:list)(sort l) ->
              ((a:A)(inf_Tree a T)->(inf_list a l)) ->
              (meq (contents T)(list_contents l)) ->
              (flat_spec T).

Lemma heap_to_list : (T:Tree)(is_heap T) -> (flat_spec T).
Proof.
Intros T h; Elim h; Intros.
Apply flat_exist with nil; Auto.
Elim H2; Intros l1 s1 i1 m1; Elim H4; Intros l2 s2 i2 m2.
Elim (merge l1 s1 l2 s2); Intros.
Apply flat_exist with (cons a l); Simpl; Auto.
Apply meq_trans with 
  (munion (list_contents l1) (munion (list_contents l2) (SingletonBag a))).
Apply meq_congr; Auto.
Apply meq_trans with 
  (munion (SingletonBag a) (munion (list_contents l1) (list_contents l2))).
Apply munion_rotate.
Apply meq_right; Apply meq_sym; Trivial.
Qed.

(*****************************)
(* specification of treesort *)
(*****************************)

Theorem treesort : (l:list)
  {m:list | (sort m) & (permutation l m)}.
Proof.
Intro l; Unfold permutation.
Elim (list_to_heap l).
Intros.
Elim (heap_to_list T); Auto.
Intros.
Exists l0; Auto.
Apply meq_trans with (contents T); Trivial.
Qed.


(* $Id: Heap.v,v 1.6 1998/04/30 16:45:56 mohring Exp $ *)
