The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

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
>
>
>