Efficient algorithms using tree

Using Coq
1

Dear friends,
I want to write an efficient algorithm for some task in hand. Currently, I am doing it using lists. The main operations I need to use are remove minimum/maximum and insert. For this, currently I am keeping a sorted list but the issue is this takes O(n) comparisons for insert. Hence, I am planning to use tree to make it work O(logn) on extracted programs.

One way I can see , this is possible is using binary search tree (or red-black tree).

Please suggest some Coq implementations and use cases for remove_min and insert trees.

Thanks in advance.

-Suneel Sraswat

2

Do you want to learn how to write binary search trees or do you want to just use any implementation?

If you want to learn how to write a binary search tree, Software Foundations Vol. 3 has chapters on binary search trees and red-black trees.

If you want to just use any implementation, the standard library has FMapAVL.

3

Dear Lyxia,
Thanks for the references. Basically I am looking something in line with Andrew Appel’s implementation of red-black tree. https://www.cs.princeton.edu/~appel/papers/redblack.pdf. I couldn’t find this paper’s repository online.

Also, Can you help in this test on FmapAVL.

From Coq Require Import FMapAVL.
From Coq Require Import Init.Nat.
From Coq Require Import Lia.
Set Implicit Arguments.

Section try.

Search “tree”.
Check Coq.FMapAVL.height.

End.

The answer for Search command is nil and the second line is “The reference Coq.FMapAVL.height was not found in the current environment.” Do I need to download/update something. My coq version is 8.12.2.

Thanks again for your reply.
-Suneel

4

The Software Foundations volume I linked earlier was also written by Andrew Appel and has a chapter about red black trees.

The way to use FMapAVL is that to instantiate it with a module implementing the OrderedType interface to use for the keys of the maps. There are examples of such modules in OrderedTypeEx, notably Nat_as_OT for nat. Once you have applied the Make module, the low-level functions like height can be found in the Raw submodule:

From Coq Require Import FMapAVL.
From Coq Require Import OrderedTypeEx.

Module NatFMap := FMapAVL.Make Nat_as_OT.

About NatFMap.Raw.height.
5

Thanks Lyxia,
This is very useful. Is there any document/manual or web-link on more on this. Some work implemented using AVL tree?
Thanks again,
Suneel

6

Sure! Here is an example of use in the CompCert verified compiler: https://github.com/AbsInt/CompCert/blob/master/backend/CleanupLabels.v . Basically, it instantiates FSetAVL with the type of positive integers and a suitable ordering, as defined here: https://github.com/AbsInt/CompCert/blob/c9f8b8e598808775bf4e5072aa47c94625677f7c/lib/Ordered.v#L29-L55 . Hope this helps.

7

Dear Xavier,
Thanks a lot. I am implementing my existing programs involving sorted lists (delete max in O(1) but insert is in O(n) time) using trees so that both the insertion and delete_max can be performed in O(logn) time. Hence, looking for right resource with minimum proof obligation.
This is helpful.
Regards,
Suneel