The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

I am reading Andrew Appel's VFA electronic book "Verified Functional Algorithms"

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

It is a very nice addition to Benjamin Pierce's wonderful Software Foundations.

I hope it is ok to ask questions about it here on the list, because I have not found any particular forum dedicated to this course.  The reader is asked not to reveal answers that can be found by Google et al., so I'll keep it condensed.

I am stuck at a proof about redblack trees, the (elements_relate) theorem at

http://www.cs.princeton.edu/~appel/vfa/Redblack.html#lab110

I wonder if anyone here has solved it, and if so if they can give a fellow reader a hint on how proceed.  Strengthening/changing the induction? Proving injectivity?

Thanks for any suggestions,

/Lars

=======================

This is the theorem.

Theorem elements_relate:

  ∀ t cts,

  SearchTree t →

  Abs t cts →

  elements_property t cts.

Proof.

To get to the remaining case where I'm stuck, do

  induction t; intros cts HS HA.

  Focus 2.

  split; intros.

  Focus 2.

  assert (Hk: int2Z k0 = int2Z k) by admit.  (* the other cases go away fine *)

Here the goal is 

  ================

    In (k0, cts (int2Z k0)) (elements (T c t1 k v t2))

"cts" is a function mapping keys to values in the same way as the redblack tree does, and "elements" converts the tree into a list of key-value pairs, the same as in the tree.

One knows some things about the bounds on the keys, so it is easy to prove that the key k0 is not in the left or right branches of the tree,  and that cts (int2Z k0) = v, so the remaining cases simplify a lot, so here just do

  cut (In (k0, v) [(k, v)]).

  Focus 2.

The goal remaining goal is

  ================

    In (k0, v) [(k, v)]

Now, k and k0 are of an abstract type "int", of which we only know "ltb_lt", i.e. that ints can be translated into Coq's integers Z, in a way that respects less-than.

       ltb_lt : forall n m : int, ltb n m = true <-> int2Z n < int2Z m

I do not see how to proceed on this line without having injectivity, i.e. that int2Z also respects equality. So,

* either one can somehow prove injectivity (or something else) using only ltb_lt, or

* some other solution is needed.

There is some more information in the context that I haven't used, such as

 cts (int2Z k0) <> default 

which says that the key has to be somewhere in the tree, and one also knows that it is not to the left and not to the right, so it should be in the middle, with the label (int2Z k), but it doesn't get me any further (I already know that (Hk: int2Z k0 = int2Z k)).

Also, the function "cts" is related to another function "lookup" which does comparison with ltb (a binary decision function) on int, instead of Z. However, I have been equally unable to derive k=k0 from that.