(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: Heap.v,v 1.3.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)

(** A development of Treesort on Heap trees *)

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

Require Import List.
Require Import Multiset.
Require Import Permutation.
Require Import Relations.
Require Import Sorting.


Section defs.

Variable A : Set.
Variable leA : relation A.
Variable eqA : relation A.

Let gtA (x y:A) := ~ leA x y.

Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.

Hint Resolve leA_refl.
Hint Immediate eqA_dec leA_dec leA_antisym.

Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.

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] *)

Definition leA_Tree (a:A) (t:Tree) :=
  match t with
  | Tree_Leaf => True
  | Tree_Node b T1 T2 => leA a b
  end.

Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
Proof.
simpl in |- *; auto with datatypes.
Qed.

Lemma leA_Tree_Node :
 forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
Proof.
simpl in |- *; auto with datatypes.
Qed.

Hint Resolve leA_Tree_Leaf leA_Tree_Node.


(** The heap property *)

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

Hint Constructors is_heap.

Lemma invert_heap :
 forall (a:A) (T1 T2:Tree),
   is_heap (Tree_Node a T1 T2) ->
   leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
Proof.
intros; inversion H; auto with datatypes.
Qed.

(* This lemma ought to be generated automatically by the Inversion tools *)
Lemma is_heap_rec :
 forall P:Tree -> Set,
   P Tree_Leaf ->
   (forall (a:A) (T1 T2:Tree),
      leA_Tree a T1 ->
      leA_Tree a T2 ->
      is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
   forall T:Tree, is_heap T -> P T.
Proof.
simple induction T; auto with datatypes.
intros a G PG D PD PN. 
elim (invert_heap a G D); auto with datatypes.
intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
apply H0; auto with datatypes.
Qed.

Lemma low_trans :
 forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
Proof.
simple induction T; auto with datatypes.
intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
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 A :=
  match t with
  | 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 :
      forall T1:Tree,
        is_heap T1 ->
        meq (contents T1) (munion (contents T) (singletonBag a)) ->
        (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
        insert_spec a T.


Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
Proof.
simple induction 1; intros.
apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
 auto with datatypes.
simpl in |- *; unfold meq, munion in |- *; auto with datatypes.
elim (leA_dec a a0); intros.
elim (H3 a0); intros.
apply insert_exist with (Tree_Node a T2 T0); auto with datatypes.
simpl in |- *; apply treesort_twist1; trivial with datatypes. 
elim (H3 a); intros T3 HeapT3 ConT3 LeA.
apply insert_exist with (Tree_Node a0 T2 T3); auto with datatypes.
apply node_is_heap; auto with datatypes.
apply low_trans with a; auto with datatypes.
apply LeA; auto with datatypes.
apply low_trans with a; auto with datatypes.
simpl in |- *; apply treesort_twist2; trivial with datatypes. 
Qed.

(** building a heap from a list *)

Inductive build_heap (l:list A) : Set :=
    heap_exist :
      forall T:Tree,
        is_heap T ->
        meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.

Lemma list_to_heap : forall l:list A, build_heap l.
Proof.
simple induction l.
apply (heap_exist nil Tree_Leaf); auto with datatypes.
simpl in |- *; unfold meq in |- *; auto with datatypes.
simple induction 1.
intros T i m; elim (insert T i a).
intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
apply meq_trans with (munion (contents T) (singletonBag a)).
apply meq_trans with (munion (singletonBag a) (contents T)).
apply meq_right; trivial with datatypes.
apply munion_comm.
apply meq_sym; trivial with datatypes.
Qed.


(** building the sorted list *)

Inductive flat_spec (T:Tree) : Set :=
    flat_exist :
      forall l:list A,
        sort leA l ->
        (forall a:A, leA_Tree a T -> lelistA leA a l) ->
        meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.

Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
Proof.
  intros T h; elim h; intros.
  apply flat_exist with (nil (A:=A)); auto with datatypes.
  elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
  elim (merge _ leA_dec eqA_dec s1 s2); intros.
  apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
  apply meq_trans with
   (munion (list_contents _ eqA_dec l1)
      (munion (list_contents _ eqA_dec l2) (singletonBag a))).
  apply meq_congr; auto with datatypes.
  apply meq_trans with
   (munion (singletonBag a)
      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
  apply munion_rotate.
  apply meq_right; apply meq_sym; trivial with datatypes.
Qed.

(** specification of treesort *)

Theorem treesort :
 forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
Proof.
  intro l; unfold permutation in |- *.
  elim (list_to_heap l).
  intros.
  elim (heap_to_list T); auto with datatypes.
  intros.
  exists l0; auto with datatypes.
  apply meq_trans with (contents T); trivial with datatypes.
Qed.

End defs.