The Coq mailing list

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

From: "Andrew Appel" <appel AT CS.Princeton.EDU>

I agree, an injectivity axiom for int2Z is necessary.

No, that's not true after all!  Injectivity of int2Z is not necessary!

I was right the first time.  But, in our community, being right without

a proof is almost like being wrong.  I have now filled in the proof

of elements_relate, in the Redblack chapter of Verified Function Algorithms.

I have just uploaded to the VFA site,

http://www.cs.princeton.edu/~appel/vfa/

version 0.4, which is the second beta release.

The only difference from version 0.3 is that "elements_relate" exercise

in the Redblack chapter is (1) explained more, and (2) guaranteed provable.

(You won't see the proof in the public distribution, but it is available

in the instructor's solution manual.)

Here's the start of the new explanation:

(** **** Exercise: 4 stars, optional (elements)  *)
(** Prove [elements_relate], that is, the correctness of the [elements] function.
    Because [elements] does not pay attention to colors, and does not
    rebalance the tree, then its proof is closely related to the [elements_relate]
    proof in SearchTree.v.  But that proof uses a different [key] type,  it needs
    to be adapted, lemma by lemma.
    Although this proof is only 4 stars of difficulty, it is plenty of work to do.*)

Sincerely, 

Andrew Appel 

P.S. At this point, there are only three exercises in all of VFA for which
I have not done the Coq proofs.  All three are in the Binom chapter: 
delete_max_Some_priq,  delete_max_None_relate, delete_max_Some_relate.