1
$\begingroup$

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.
Improve this question
$\endgroup$
2
  • $\begingroup$ One simple workaround is to add your definitions as propositional equalities to the database, ie prove bar : c = a by reflexivity, and add bar to the database. Although this is rather unsatisfying, because there should be no need to use propositional equality when the definitional one does the job. So let us see if someone has a better solution. $\endgroup$
    – Meven Lennon-Bertrand
    Nov 21 at 9:56
  • 1
    $\begingroup$ @MevenLennon-Bertrand, yeah, I thought about that, but I'd have to add an additional step to fold everything back again in order to get the intended presentation for values, and be careful about cases where I can't rewrite anything (other than unfolding and folding back again). I do think autosubst uses a similar trick, but I really hope there's a better way... $\endgroup$
    – paulotorrens
    Nov 21 at 12:33

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.