The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Thanks for all the responses!

I  found that AVL trees in the standard library are pretty good, but I need to compress the proof term. Since the property is decidable it isn't too difficult to replace it with something like `Is_true (check_property ..)`.This means that you you re-check the property every time you do a computation. I'm interested in what impact it would have if proofs were fully transparent, but transitively making all definitions transparent seems like quite a task.

An alternative (which is what I'm doing now) is to provide a "canon : t -> t" function that essentially throws away the current proof term and replaces it with a smaller proof term that is not based on history. For example, I have a proof, `build_ok : Is_true (check k) -> is_bst k` and canon basically converts b into : {| this := b.(this) ; is_bst := build_ok ... |}. In practice this means that the data representation contains the tree twice (maybe hashcons'd?) and checks the property once.

On Thu, May 14, 2020 at 12:46 PM Andrew Appel <appel AT princeton.edu> wrote:

The MSets interface of the Coq standard library factors the program from the proof, and may solve the problem that's being discussed here.

It was intended as a replacement for FSets and FMaps.

There had been a plan to make MMaps also (finite maps instead of sets), but unfortunately I don't think that was ever done.

There are efficient implementations of MSets for AVL trees and Red-Black trees in the standard library.

--

gregory malecha

gmalecha.github.io