The Coq mailing list

[Mario Alvarez <mariomcgilvrayalvarez AT gmail.com>]

Hello, Coq Club,

I want to use rewrite_strat to do some rewriting under binders. Upgrading to 8.5 is not currently a realistic option for my project, so I'm using 8.4(pl4).

Ideally I'd like to use a hint database for this rewriting. However, I've had some problems trying to do this:

- The "hints" directive in rewrite_strat seems to be broken; when I use it with my hints database it complains that there's nothing to rewrite, even when there is clearly rewriting to be done.

- Looking at the source code, I saw there's an "old_hints" directive. This one seems to work for most of the rewriting hints I care about.

- However, old_hints doesn't quite take care of everything. Some of my hints don't generate side-conditions and are simple rewriting lemmas. These seem to be applied correctly. However, I have some lemmas which produce side-conditions; these need to be discharged using a separate Resolve hint-database. In particular, I have

-----------------------------------------------------------------------
Hint Rewrite
     embed_push_TRUE embed_push_FALSE
     embed_push_And embed_push_Or embed_push_Imp
     embed_push_Exists embed_push_Forall
     embed_push_Const
  : embed_push.

(*

(* these ones produce side-conditions *)

Hint Rewrite
     embed_push_Eq embed_push_Gt embed_push_Le
     using solve [eauto 20 with arith_push]
                         : embed_push.
*)

Hint Resolve
     arith_push_plus arith_push_VarNow arith_push_VarNext arith_push_Nat_zero arith_push_Nat_one arith_push_Nat arith_push_Real
  : arith_push.
-------------------------------------------------------------------------

I apply these hints using

rewrite_strat (topdown (old_hints embed_push)).

With the second "Hint Rewrite" command commented out, this works correctly (except that it doesn't do the rewriting specified in the second "Hint Rewrite" command, which I need).

When I uncomment the second batch of hints, no rewriting is performed at all. Instead I get the following error message:

Error: Application of lemmas whose beta-iota normal form contains
metavariables deep inside the term is not supported; try "refine" instead.

Do you know if there is a way to get this behavior (using rewrite_strat to rewrite under binders, with the ability to discharge side-conditions using a Resolve database) in 8.4?

Thanks,

Mario