The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Apr 01, 2009 at 12:38:40PM +0100, Edsko de Vries wrote:
> Hi Yves,
> 
> >You really sent us very little context, but assuming you are using a  
> >defined equality because it is
> >more strictly more liberal than Leibniz equality (i.e. there are a  
> >and b such that a === b and a <> b),
> >I think that what you are trying to prove is not true!  List.in  
> >explicitly relies on Leibniz equality.
> 
> Aah, I see. That makes perfect sense, thank you.
> 
> (The === relation came from the Metatheory library bundled with Brian  
> Aydemir's LNgen tool; quite frankly, I didn't really understand it and  
> I was trying to copy the style of an existing lemma. "Proof by  
> incantation" as my previous advisor would say ;)
> 
> Changing the relation R to be simply eq solves it.
> 
> Thanks,
> 
> Edsko
> 

By the way, there is now a file SetoidList.v in the standard library,
where you can find a definition for the fact of belonging to a list
modulo some setoid equality.

Best,

Pierre Letouzey