The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Hello,

  For comparison, in the Coq’Art book (chap. 11) we specified the remove function on search trees as follows:

Inductive RM (n:A) (t t': btree A) : Prop :=

    rm_intro :

      ~ In n t' ->

      (forall p:A, In p t' -> In p t) ->

      (forall p:A, In p t -> In p t' \/ n = p) ->

      search_tree t' -> RM n t t' .

  Definition rm_spec (n:A) (t:btree A) : Set :=

    search_tree t -> {t' : A_btree | RM n t t’}.

Note that this specification describes a total function: if we try to remove a non-element of t, we obtain an equivalent (same content) search tree.

The file (with search trees on Z instead of A) is available on 

https://github.com/coq-community/coq-art/blob/master/ch11_search_trees/SRC/chap11.v

Pierre

Le 9 oct. 2022 à 07:17, Chris Dams <chris.dams.nl AT gmail.com> a écrit :

Hello Clement,

You are right that the original lemma is true. I actually misread it
the other way around, like
In x t -> In x (remove y t) which does need a x <> y clause.

However, one then has to note that as a specification the lemma In x
(remove y t) -> In x t is
not very good. It is also satisfied by having a remove function that
removes all elements and
returns the empty container.

Kind Regards,
Chris

Op za 8 okt. 2022 om 20:51 schreef Clément Pit-Claudel <cpitclaudel AT gmail.com>:

Hi Chris and Suneel,

The original lemma looks correct to me.  The standard library contains a proof of it for lists, in fact:

  in_remove:
    forall [A] eq_dec (l : list A) (x y : A),
    In x (remove eq_dec y l) -> In x l /\ x <> y

What am I missing?

Clément.

On 10/8/22 09:54, Chris Dams wrote:

Hello Suneel,

To me it looks your removal lemma is not correct. "In x (remove y t) -> In x t"
should not be true if x and y happen to be equal. This needs a precondition
x <> y. And then you also need something for the case where they are equal,
like "~ In x (remove x t)".

Kind Regards,
Chris

Op za 8 okt. 2022 om 09:24 schreef Suneel Sarswat <suneel.sarswat AT gmail.com>:

Dear Friends,
I am working on an application of the red-black tree data structure in implementing an algorithm. In my setting, I am using remove and add. Unfortunately, I could not find out a specification lemma for 'remove' which states the following trivial property.

Lemma remove_spec0 (t:tree)(x y:elt):
In x (remove y t) -> In x t.

Or

Lemma remove_spec0 (t:tree)(x y:elt):
List.In x (elements (remove y t)) -> List.In x (elements t).

The current module has specifications for 'InT', which is a proposition on the membership of keys whereas I am looking for membership of data. Is there any way to have an equivalent lemma without unfolding the definition of remove?

Similarly, for adding specification, the current module has a lemma for 'InT' but not on membership of the whole element.

Thanks,
Suneel