[Agda] red black trees with delete

[jleivent at comcast.net]

Attached is an Agda implementation of Red Black trees (the old-fashioned non-leaning variety) with insert, find, and delete functions.  The dependent types show that the trees have the usual red-black level and color invariants, are sorted, and contain the right multiset of elements following each function.  I also tried to keep the types a transparent as possible.

Since I'm a novice at dependent-typed programming, I'm not sure if this is a trivial result or not.  However, one interesting thing is that I didn't previously know or refer to any existing red black tree implementation of delete - I just allowed the combination of the Agda type checker and the exacting dependent type signatures to do their thing (with some simple reasoning about what the delete function must contain - such as a delete minimum function) - making me feel more like a facilitator than a programmer.

Also, I'm not sure of the approach I took for erasability (via parameterized module) - but it was the only thing I could think of, following a failed attempt to use Agda's irrelevance feature.  I wanted to demonstrate erasability of the proof terms because had I not, one could argue that the implementation could be extracting information from the proof terms to cheat somewhere.  Also, those proof terms would be pretty heavy-weight at runtime!

I'd appreciate any comments.

-- Jonathan Leivent
-------------- next part --------------
A non-text attachment was scrubbed...
Name: RB.zip
Type: application/zip
Size: 7300 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120111/2d1160e6/RB.zip