The Coq mailing list

[Lars Rasmusson <lars.rasmusson AT gmail.com>]

I am doing Andrew Appel's VST course, that was announced here on the list a month ago.
https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00118.html

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.  

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 this simplifies to

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

    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 solve it somehow, 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.