The Coq mailing list

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

Thanks!  That was an elegant counter-example that showed that the theorem is not always true.

I really liked your approach (which I parrot here, to clarify it for myself): 

- Create a new type 'int1:=bool * int', that otherwise behave just as 'int' when mapped to Z. 

  Then, For all k:int,  (true, k) <> (false,k), but they behave just as k when mapped to Z.

- Instantiate 'int' in the module with 'int1'.

- Create a singleton tree that contains ((false,k), v)

- Lookup (true,k) which will return v.

   This is a contradiction, because (true,k) is decidably not in the tree.

On Thu, Aug 25, 2016 at 11:18 PM, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> wrote:

I think you do need an axiom saying that int2Z is injective or something like it. If you don't have that you can do the following:

In Extraction.v, rename int, ltb, int2Z and ltb_lt to int0, ltb0, int2Z0 and ltb_lt0. Then define int as (bool * int0)%type, and ltb (resp int2Z) from ltb0 (resp int2Z0) ignoring the bool. ltb_lt can be proved trivially.

This gives us an int type with int2Z not injective and still satisfying the required axioms according to VFA.

Then in Redblack.v we can prove that, if there is at least some value k0 of type int0, and some value v of type V not equal to default, then

exists t cts, SearchTree t /\ Abs t cts /\ ~ elements_property t cts.

Specifically [t := T Black E (false,k0) v E] (the singleton tree) and [cts :=(t_update (combine (int2Z0 k0) (t_empty default) (t_empty default)) (int2Z0 k0) v)] (v on (int2Z0 k0) and default everywhere else).

This is because (true,k0) is not in (elements t) but does verify [cts (int2Z (true,k0)) <> default].


See attached files which contain the int0 modification and the proof above.

Gaëtan Gilbert

On 25/08/2016 21:41, Lars Rasmusson wrote:

I am reading Andrew Appel's VFA electronic book "Verified Functional Algorithms"
http://www.cs.princeton.edu/~appel/vfa/ <http://www.cs.princeton.edu/%7Eappel/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 <http://www.cs.princeton.edu/%7Eappel/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.