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: Oct 13 2024 at 01:02 UTC