[Agda] DTO, STO, AVL.Tree

[Serge D. Mechveliani]

On Sun, Oct 21, 2012 at 12:05:36PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-19 21:49, Serge D. Mechveliani wrote:
[..]
>> I am not sure, but have an impression that
>> 1) STO needs to be removed and to merge to DTO, with _<_ defined via
>>     _<=_  and  \neg (x \~~ y),
>
> See Relation.Binary.Props.StrictTotalOrder and
> Relation.Binary.Props.DecTotalOrder.

Indeed, looks like relevant. Thank you.


>> 2) AVL needs to generalize from \equiv to \~~.
>
> A previous version of Data.AVL allowed arbitrary equivalence relations.
> When I added the search tree invariant to the data structure I switched
> to a less general interface in order to avoid some complications. We
> could switch back, but I believe that both the code and the interface
> would become more complicated.
>

One more note of AVL
--------------------
AVL.Indexed  has the fragment 

  -- Converts the tree to an ordered list. Linear in the size of the tree.
  ...
  toDiffList : Б┬─ {l u h-> Б├▓ Tree l -> h Б├▓ DiffList KV
  toDiffList (leaf _)       = []
  toDiffList (node k l r _) = toDiffList l ++ k ::┬╥ toDiffList r

It is desirable to add a proof for 
(1) StrictlyOrderedList? <parameters> $ toList t 
    for  toList = DiffList.toList \o toDiffList,
    (1) means that the result KV list is ordered by the first coordinate 
        (Key),
(2) fromList $ toList (t : Tree)  \equiv  t

(1) looks easy, and I do not know about (2). 

After this, it will be easy to implement a  sorting function  of  
O(n*(log n))  with all the needs proofs.   
This function will be almost the same as  
                      \lambda pairs -> toList (fromList pairs : Tree)

Regards,
Sergei