Stream: Coq users

Topic: Tactic for generating equalities

spaceloop (Dec 04 2023 at 10:46):

There must be a simple tactic for this, but I couldn't find it: I have a goal P x y z and an assumption H : P x v w. How can I use H and generate goals y = v and z = w?

Michael Soegtrop (Dec 04 2023 at 10:56):

Unless you can prove by whatever means that y=v and z=w, H is useless to prove the goal. As an example assume P x y z means "y is married with z for more than x years". Then H would be that some couple "v w" is married for more than x years and your goal is to prove that couple "y z" is married for more than x years - which is an entirely different thing - unless it happens to be so that v=y and w=z.

Gaëtan Gilbert (Dec 04 2023 at 10:59):

I don't think we have such a tactic in the stdlib.
I guess you can get something similar by defining

Lemma helper {A} (x:A) B : A = B -> B.

then do apply (helper H); f_equal

spaceloop (Dec 04 2023 at 12:53):

Michael Soegtrop said:

Unless you can prove by whatever means that y=v and z=w, H is useless to prove the goal. As an example assume P x y z means "y is married with z for more than x years". Then H would be that some couple "v w" is married for more than x years and your goal is to prove that couple "y z" is married for more than x years - which is an entirely different thing - unless it happens to be so that v=y and w=z.

Yes, I can prove that. I would just like to tell Coq: try to unify these types as best as you can, and leave goals for the equalities that you couldn't find via unification (and I will prove them myself).

spaceloop (Dec 04 2023 at 12:53):

Gaëtan Gilbert said:

I don't think we have such a tactic in the stdlib.
I guess you can get something similar by defining

Lemma helper {A} (x:A) B : A = B -> B.

then do apply (helper H); f_equal

Thanks, I will give that a try!

Paolo Giarrusso (Dec 04 2023 at 12:59):

you seem to be looking for something like applys_eq from Software Foundations https://softwarefoundations.cis.upenn.edu/plf-current/UseTactics.html

spaceloop (Dec 06 2023 at 09:02):

Paolo Giarrusso said:

you seem to be looking for something like applys_eq from Software Foundations https://softwarefoundations.cis.upenn.edu/plf-current/UseTactics.html

Thanks, that is exactly what I was looking for!

Last updated: Oct 13 2024 at 01:02 UTC