The Coq mailing list

[Andrew Appel <appel AT CS.Princeton.EDU>]

I agree, an injectivity axiom for int2Z is necessary.

In this beta release, there are a few places (such as RedBlack.elements_relate)

where I had not yet written the solution.  Indeed, the instruction for

proving this one,

  "its proof should be a simple copy-paste from SearchTree.v,
    with only minor edits."

is an oversimplification.  The proof does follow the corresponding

theorem from SearchTree.v, but it's not quite as simple as a copy-paste.

I apologize for this incompleteness.

I'll fix this in the next release of Verified Functional Algorithms.

REQUEST:  If you're an expert and you're tempted to post your

adjustments and "better solutions" to this mailing list, 

why not instead ask to participate in the subversion repository

where you can work with the authors on this construction?

For Software Foundations, you can request this from Benjamin Pierce.

For VFA, you can request this from Andrew Appel.

Sincerely,

Andrew Appel