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)
Definition of trees over an ordered set
a is lower than a Tree T if T is a Leaf
or T is a Node holding b>a
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.
equivalence of two trees is equality of corresponding multisets
From lists to sorted lists
Specification of heap insertion
Building a heap from a list
Specification of treesort