Patrick Nicodemus (Jan 02 2022 at 10:39): Patrick Nicodemus (Jan 02 2022 at 10:39):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'].
Patrick Nicodemus (Jan 02 2022 at 10:41):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
Patrick Nicodemus (Jan 02 2022 at 10:42):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
Pierre Jouvelot (Jan 02 2022 at 10:49):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'.
Paolo Giarrusso (Jan 02 2022 at 10:52):Yep, that's one great technique: Definitions are (light) abstraction barriers, Notations aren't. Not always suitable....
Paolo Giarrusso (Jan 02 2022 at 10:53):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: Oct 13 2024 at 01:02 UTC