[Agda] finite map

[Sergei Meshveliani]

On Thu, 2013-12-19 at 14:13 +0100, Nils Anders Danielsson wrote:
> On 2013-12-17 09:53, Sergei Meshveliani wrote:
> > I consider implementing  AssociationList,
> > like AssocList in the Haskell library, only with some proofs.
> >
> > Has the Agda standard library such?
> 
> Perhaps you can use Data.List.Any.any.
> 

1) AssocList  is a list of pairs  (key , value),  with keys compared by 
_≈_. But I think that there is also needed the condition of that the
keys do not repeat. This makes it a certain record. And then,
                                                    insert k v assocList
needs to include a proof for the condition.
Then, I am going to use this to define  Multiset.
Generally, it is probably natural to have such  AssocList  in Standard
library -- because  AVL.Tree  is only for syntactic equality.

2) Suppose that  AVL.Tree  is generalized to  Key  being of
   StrictTotalOrder _≈_ _<_  (rather than _≡_).

This requires certain difficult proofs.
And suppose that these proofs are `postulate'-d.
Probably, it will be useful even in this version
(?) 
For example, one can define  Multiset  as  Tree A ℕ,  and it is also
O(n*(log n)) is lookup/insert.

Regards,

------
Sergei