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.