# Library Coq.Sorting.Heap

This file is deprecated, for a tree on list, use Mergesort.v.
A development of Treesort on Heap trees. It has an average complexity of O(n.log n) but of O(n²) in the worst case (e.g. if the list is already sorted)

Require Import List Multiset PermutSetoid Relations Sorting.

Section defs.

# Trees and heap trees

## Definition of trees over an ordered set

Variable A : Type.
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 : core.
Hint Immediate eqA_dec leA_dec leA_antisym : core.

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

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.

Lemma leA_Tree_Node :
forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).

## 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).

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.

Lemma is_heap_rect :
forall P:Tree -> Type,
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.

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.

Lemma low_trans :
forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.

## Merging two sorted lists

Import Morphisms.

Instance: Equivalence (@meq A).

Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).

Lemma merge :
forall l1:list A, Sorted leA l1 ->
forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.

## From trees to multisets

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).

# From lists to sorted lists

## Specification of heap insertion

Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.

## Building a heap from a list

Lemma list_to_heap : forall l:list A, build_heap l.

## Building the sorted list

Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.

# Specification of treesort

Theorem treesort :
forall l:list A,
{m : list A | Sorted leA m & permutation _ eqA_dec l m}.

End defs.