The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can also do [Hint Rewrite @my_rw_rule : rw_rules.], but this won't solve the constraints in the goal, it'll just leave them unsolved as further goals.

-Jason

On Fri, May 16, 2014 at 8:16 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 05/16/2014 12:14 PM, jonikelee wrote:

I'm not sure if I'm hitting a bug or being told something is not legal Coq.

I have a Section with Contexts, a rewrite rule defined there, and an attempt to add a hint for that rewrite after the section.  Like this:

   Section defs.
      Context {A : Type}.
      Context {ordA : Ordered A}.
      ...
      Lemma my_rw_rule : ...
   End defs.

   Hint Rewrite my_rw_rule : rw_rules.

The above Hint Rewrite produces the following error:

   Toplevel input, characters 0-34:
   Error:
   Unable to satisfy the following constraints:

   ?1 : "Type"
   ?2 : "Ordered ?1"


Obviously, those constraints can't be solved outside that Section - but they can be solve elsewhere (other similarly contextualized sections, etc.).  And, Hints added in the section don't survive the end of the section.  Also note that Hint Resolve after the section for things defined in that section doesn't produce any such error. If Hint Resolve knows enough to delay attempting to satisfy those constraints until the rule is applied, why doesn't Hint Rewrite?

Do I need to handle rewrite rules defined under Contexts differently?

-- Jonathan

Just noticed that there is a simple if somewhat inconvenient workaround - trivially redefining the rule outside the section:

Definition rw_rule(A : Type)(ordA : Ordered A) := my_rw_rule.
Hint Rewrite rw_rule : rw_rules.

But, this only works if A and ordA are not implicit in the new definition.

So, I think the above error is probably a bug having to do with implicit arguments and rewrite rules.  I'll file it...

-- Jonathan