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`

?

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.

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`

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).

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!

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

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