The Coq mailing list

[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