Stream: Coq users

Topic: getting around limitations of simple apply


view this post on Zulip 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'].

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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'.

view this post on Zulip 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....

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC