I have the following problem: I have some lemma, A, which is stated in terms of an identifier L. I can run "unfold" on the definition of L, and L gets reduced to L', and when i run this command with A as some kind of expressly stated hypothesis "unfold L in A" then i replace A with A' := A[L/L'].

So my problem is that I want to apply A automatically using auto, which uses simple apply. However, the conclusion of A doesn't match the goal correctly - i need to transform it into A' before i can use simple apply on it. Using the stronger "apply" tactic works and simplifies the goal correctly, presumably the unification algorithm in "apply" is strong enough to know to try unfolding certain terms in A to make the unification work

i guess my question is, how can i solve this problem? how can i tell the auto algorithm, or simple apply, to always unfold L in this lemma

I guess that one way to get around this kind of problem could be to replace the `Definition`

of L in terms of L' by instead defining L as a `Notation`

in terms of L'.

Yep, that's one great technique: Definitions are (light) abstraction barriers, Notations aren't. Not always suitable....

You can also replace Hint Resolve via an Hint Extern using apply. But you often want to have some syntactic pattern for your hint (for performance), which might need to mention L or L'?

Last updated: Feb 01 2023 at 13:03 UTC