The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

That seems to be the case in this instance; if I use [set] to remove all the evars from the goal, then it magically works again without the [at 1].  However, I still can't get setoid_rewrite to work on the underlying problem (even with [at 1]), which is at https://coq.inria.fr/bugs/show_bug.cgi?id=3254 and also https://gist.github.com/JasonGross/9491068.

The error message is

Error:

Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.

Unable to satisfy the following constraints:

EVARS:

 ?267==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n H

         |- ProperProxy ?265 ?224] (internal placeholder)

 ?266==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n H

         (do_subrelation:=do_subrelation)

         |- Proper (?263 ==> ?265 ==> flip impl) refine]

         (internal placeholder)

 ?265==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n H

         |- relation (Comp (Rep0 * cod idx))] (internal placeholder)

 ?264==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n H

         (do_subrelation:=do_subrelation)

         |- Proper (pointwise_relation (Rep0 * cod idx) refine ==> ?263)

              (Bind (UnbundledMethods0 idx r_n n))] (internal placeholder)

 ?263==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n H

         |- relation (Comp (Rep0 * cod idx))] (internal placeholder)

 ?224==[Rep0 MethodNames0 UnbundledMethods0 idx r_n n

         |- Comp (Rep0 * cod idx)] (underscore)

At a glance, it seems like it might be failing because it's inferred [flip impl] where it should have inferred [impl], but I'm not really sure.

-Jason

On Mon, Mar 10, 2014 at 10:37 AM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

Hi,

  As suggested by Cedric it might fail because just the first occurrence can be rewritten,

otherwise it’s probably a bug indeed. Note that rewrite at has a different semantic (it’s counting

occurrences of the first complete unification appearing in the goal). The bug tracker is 

inaccessible right now…

— Matthieu

Le 10 mars 2014 à 09:34, Jason Gross <jasongross9 AT gmail.com> a écrit :

Hi,

Can someone explain to me the difference between [setoid_rewrite ... at 1] and [setoid_rewrite ...]?  In particular, why might the first succeed when the second fails?  (This seems to me to be a bug, so I reported it, with a test case, at https://coq.inria.fr/bugs/show_bug.cgi?id=3253.)

Thanks,

Jason