Stream: Coq users

Topic: Apply mismatched lemma, emit equality constraint/goal


view this post on Zulip Roger Bosman (Oct 15 2021 at 09:07):

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?

view this post on Zulip Roger Bosman (Oct 15 2021 at 09:08):

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

view this post on Zulip Roger Bosman (Oct 15 2021 at 09:10):

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

view this post on Zulip Ana de Almeida Borges (Oct 15 2021 at 09:46):

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

view this post on Zulip Roger Bosman (Oct 15 2021 at 11:52):

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