## 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: Jun 22 2024 at 16:02 UTC