I'm working with a substitution algebra as described by the Autosubst team, and I'm trying to automate some rewritings. As I'm using more than one calculus in my code, I'm trying to use the rewrite database in order to make it a bit more extensible (namely: I'm defining a homomorphism abstractly, and I want a tactic that simplifies substitutions and properly distributes the substitution over some algebra, e.g.,
s (f a b) = f (s a) (s b), in the process). For readibility, a few of the substitution operations I need are hidden under definitions.
It seems that the rewrite_strat tactic (and the autorewrite tactic as well, for that matter) are not able to automatically unfold definitions when trying to rewrite something that comes from a database. However, if I ask rewrite_strat to use the lemma directly, it works (see minimal example below).
So, my questions are: (1) why? And (2) is there a way to make rewrite_strat work as I need while still using the database?
Require Import Setoid. Axiom a b: nat. Definition c: nat := a. Hypothesis foo: a = b. Create HintDb foo. Local Hint Rewrite foo: foo. Goal c = b. Proof. Print Rewrite HintDb foo. Fail progress autorewrite with foo. Fail progress rewrite_strat outermost (hints foo). rewrite_strat outermost (foo). reflexivity. Qed.