The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Edsko de Vries wrote:
> Hi,
>
> Coq is giving me an error, and I'm not sure what it means. A tiny bit 
> of context: in the proof of a simple lemma, I need to prove that
>
> Hin : z === x
> ______________________________________(1/2)
> List.In (x, c) ((z, c) :: l)
>
> which surely should be easy (rewrite using Hin, since I cannot do 
> "subst"), and then apply In_head (or whatever that lemma is called). 
> However, calling "rewrite Hin" gives the following error:
>
> Error: Tactic failure: setoid rewrite failed: unable to satisfy the 
> rewriting constraints.
> Unable to satisfy the following constraints:
> In environment:
> A : Type
> B : Type
> key : Type
> x : key
> a : A
> E : list (key * A)
> F : list (key * A)
> G : list (key * A)
> R : relation key
> Equiv : Equivalence R
> Eqdec : EqDec key R
> Fset : FSet key Eqdec
> z : key
> c : A
> l : list (key * A)
> IHl : x `in` dom l -> exists b : A, binds x b l
> Hin : z === x
>
> ?10768 == (Morphism (?10764 ==> flip impl) (eq (x, c)))
> ?10767 == (MorphismProxy ?10765 c)
> ?10766 == (Morphism (equiv ==> ?10765 ==> ?10764) pair)
> ?10765 == (relation A)
> ?10764 == (relation (key * A)).
>
> I'm not sure what that means. Any pointers would be appreciated,
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
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.
Allowing what you want to perform would tantamount to proving z === x -> 
z = x.

List.in (x,c) ((z,c)::l) converts to (x,c) = (z,c) \/ (x,c) in l.   
Rewriting with Hin would require rewriting
inside a pair or inside an eq...  These informations appear inside you 
error report.

If you want more, you need to give more details.  What is behind the 
notation "_ === _"?

Yves