coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mario Alvarez <mmalvare AT eng.ucsd.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Problems with rewrite_strat in 8.4pl4
- Date: Fri, 5 Jun 2015 13:44:20 -0700
Hello, Coq Club,
(Hopefully this is not a double post; I tried to send this before but it did not go through).
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.
-------------------------------------------------------------------------
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.
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,
- [Coq-Club] Problems with rewrite_strat in 8.4pl4, Mario Alvarez, 06/05/2015
Archive powered by MHonArc 2.6.18.