# Applying a theorem that doesn't match exactly

Let’s say I’m trying to prove something of the form “P a”. In the context, I have “P b”. Now I know that “a = b”, which I can then use to complete the proof. However, at times “a” and “b” are complicated expressions, and I would like to be able to tell Coq to use “P b” and generate the goal “a = b” itself rather than me having to type the complicated expressions in.

That being said, my question is this: Is there some tactic that, given a goal like “P a” and a hypothesis “P b”, will change the goal to “a = b”? It seems like it would be similar to “apply”, but I couldn’t find anything like it in the documentation.

Another thing I forgot to mention: I technically could prove the theorem “∀ a b, P a → a = b → P b” and then use it later. However, this requires a new theorem for every P that I want to use this for, and I run into this situation enough that I would like to find an alternative.

Your theorem `∀ a b, P a → a = b → P b` can be parametrized over `P`, and this is almost what `eq_ind_r` from the standard library is:

``````eq_ind_r :
forall [A : Type] [x : A] (P : A -> Prop),
P x -> forall y : A, y = x -> P y
``````

This means you can try:

``````Lemma my_goal (A : Type) (P : A -> Prop) a b (Hb : P b) : P a.
Proof.
apply (eq_ind_r _ Hb).
``````

It might be the case that, in more complex situations, you could have to give `P` explicitly in `apply (eq_ind_r P Hb)`.
If the output of `P` is not `Prop` but for example `Type`, you could rely on `eq_rect` instead of `eq_ind_r` but with slightly different implicit parameters (and equality in the opposite direction, as with `eq_ind`).

This reminds me of Charguéraud’s `applys_eq`

2 Likes

Thanks. eq_ind_r didn’t work, but applys_eq worked perfectly.