The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/18/2014 09:08 PM, Vadim Zaliva wrote:
> ...
>
> Still as in your example the problem remains. It looks like we are stuck here.

I don't know if this is related, but there are some existing bugs with 
setoid rewrite even in rather trivial cases that produce an "Unable to 
satisfy the rewriting constraints" error.  For instance:

Require Setoid.
Goal forall P, (P <-> True) -> {P}+{False}.
intros P H.
rewrite H.

produces:

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the rewriting 
constraints.
Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?7==[P H |- CRelationClasses.crelation Prop] (internal placeholder) {c}
 ?8==[P H (do_subrelation:=CMorphisms.do_subrelation)
       |- CMorphisms.Proper
            (CMorphisms.respectful iff
               (CMorphisms.respectful ?X7@{A:=P; A:=H} 
(CRelationClasses.flip CRelationClasses.arrow)))
            sumbool] (internal placeholder) {p}
 ?9==[P H |- CMorphisms.ProperProxy ?X7@{A:=P; A:=H} False] (internal 
placeholder) {p0}
.

I filed bug 3417 for something similar - but the cases I mentioned in 
that bug report seem to have been fixed (at least when using the rewrite 
tactic, not when directly using setoid_rewrite).

This is in the trunk, version 9ce0bfcd59c52955361a0d2b726f980168659542, 
which is only a few days old.

-- Jonathan