When you have a goal and a lemma that does not really match the goal, you cannot apply it. Associativity can be a common one, where your goal may be some `Env1 ++ (Env2 ++ Env3) |- ...`

and your lemma might expect `(Env1 ++ Env2) ++ Env3 |- ...`

. If you apply this lemma coq will complain. I'm looking for a tactic that lets me apply this lemma anyways, but also emit an equality constraint/goal whereever it found mismatches, i.e. in this case I would want to apply the goal and emit a goal `Env1 ++ (Env2 ++ Env3) = (Env1 ++ Env2) ++ Env3`

. Does this exists?

I know stuff like `forwards`

exists, but then it is my job to instantiate all the parameters myself. Applying it to the goal has the nice effect that all the parameters that *do* match have already been instantiated to the right ones, if that makes any sense

Of course adding a lemma that does this for a specific case, since it just follows from the original lemma and `subst`

. I have been doing this manually in places where its needed, but since it is so trivial, I figured this should be possible to be implemented as a tactic

I think this question / answer might be what you are looking for.

Thanks, that is exactly what I'm looking for. It doesn't work for me however (I get weird errors), but I will investigate further myself before asking here, if needed :)

Last updated: Jan 31 2023 at 12:01 UTC