Library Coq.Sorting.Heap
A development of Treesort on Heap trees
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