Red-black tree benchmark problem

[Adam Chlipala]

Here's a benchmark problem that might seem too obvious to mention:
Implement insertion into red-black trees (representing finite sets of
some arbitrary carried type with comparison) and verify that every
red-black tree is balanced and that insertion has the expected effect on
the set of keys.

My Coq solution appears in the book that I'm working on:
http://adam.chlipala.net/cpdt/html/MoreDep.html#lab49

[Hongwei Xi]

I have taken a look at the solution. It is great!

I understand the part on being balanced. Could you be more specific on
the claim that insertion has the expected effect on the set of keys?
I have difficulty getting it out of your code.

Thanks,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hw...@cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

[Adam Chlipala]

Hongwei Xi wrote:
> On Thu, 5 Feb 2009, Adam Chlipala wrote:
>
>
>>> Here's a benchmark problem that might seem too obvious to mention:
>>> Implement insertion into red-black trees (representing finite sets of
>>> some arbitrary carried type with comparison) and verify that every
>>> red-black tree is balanced and that insertion has the expected effect on
>>> the set of keys.
>>>
>>> My Coq solution appears in the book that I'm working on:
>>> http://adam.chlipala.net/cpdt/html/MoreDep.html#lab49
>>>
>>>
>>>
>>>
> I have taken a look at the solution. It is great!
>
> I understand the part on being balanced. Could you be more specific on
> the claim that insertion has the expected effect on the set of keys?
> I have difficulty getting it out of your code.
>

You can define a test for whether a key is in a tree ("present" in my
solution), and the property to prove is that any value x is in the
result of inserting y into a tree T iff x = y or x is in T.

[Hongwei Xi]

On Fri, 6 Feb 2009, Adam Chlipala wrote:

>>You can define a test for whether a key is in a tree ("present" in my
>>solution), and the property to prove is that any value x is in the
>>result of inserting y into a tree T iff x = y or x is in T.

I see. I assume that this does not imply that a binary search always
finds x in T if x is in T, right?

[Adam Chlipala]

Hongwei Xi wrote:
> On Fri, 6 Feb 2009, Adam Chlipala wrote:
>
>
>>> You can define a test for whether a key is in a tree ("present" in my
>>> solution), and the property to prove is that any value x is in the
>>> result of inserting y into a tree T iff x = y or x is in T.
>>>
>
> I see. I assume that this does not imply that a binary search always
> finds x in T if x is in T, right?
>

I'm not sure what you mean. My solution doesn't even have a lookup
function defined.

[Hongwei Xi]

I am trying to see if the code still typechecks if I change

le_lt_dec x y

into

le_lt_dec y x

[Adam Chlipala]

Hongwei Xi wrote:
> On Fri, 6 Feb 2009, Adam Chlipala wrote:
>
>
>>> Hongwei Xi wrote:
>>>
>>>> On Fri, 6 Feb 2009, Adam Chlipala wrote:
>>>>
>>>>
>>>>
>>>>>> You can define a test for whether a key is in a tree ("present" in my
>>>>>> solution), and the property to prove is that any value x is in the
>>>>>> result of inserting y into a tree T iff x = y or x is in T.
>>>>>>
>>>>>>
>>>> I see. I assume that this does not imply that a binary search always
>>>> finds x in T if x is in T, right?
>>>>
>>>>
>>> I'm not sure what you mean. My solution doesn't even have a lookup
>>> function defined.
>>>
>
> I am trying to see if the code still typechecks if I change
>
> le_lt_dec x y
>
> into
>
> le_lt_dec y x
>

The insert function still type-checks. My solution doesn't verify that
the trees being constructed are binary search trees. That would be easy
to prove as an additional after-the-fact theorem.