The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi! You may be interested by this message:

https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00013.html

Le 09/06/2014 17:17, Jonathan a écrit :
> A funny thing happened on the way to a counterexample...
>
> I seem to have discovered, with Coq's help, a new type of balanced 
> binary search tree, closely related to red-black and AVL trees. I'm 
> calling them "gap trees".
>
> See the file gaptree.txt in 
> https://github.com/jonleivent/mindless-coding for details.  The 
> extracted OCaml code is in gaptree.ml and gaptree.mli - which were 
> extracted from the proofs in gaptree.v.  As mentioned in gaptree.txt, 
> I was trying to see how the treatment I had given red-black and AVL 
> trees in that git repository would fare on a structure that doesn't 
> work properly.  So I devised a related structure that didn't obviously 
> not work, and churned away at it in Coq.  And, much to my surprise, it 
> didn't not work.
>
> If gap trees are new - it's a bit of a wonder how they managed to 
> avoid being discovered until now.  Which makes me suspect that either 
> they don't work or were discovered before - but I can't find anything 
> similar when searching for binary search tree structures on the 
> internet (there's certainly lots of stuff on red-black and AVL trees, 
> though), and I don't see any holes in the Coq proofs.
>
> Does anyone know if gap trees were discovered previously?  Would 
> anyone like to examine this result to check if there are any flaws in 
> the gap tree algorithms?  Or, does anyone on this list know of someone 
> who might want to try that?
>
> -- Jonathan