# Applying a theorem that doesn't match exactly

**URL:** <https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552>\
**Category:** Using Rocq\
**Created:** [February 6, 2022, 3:18am UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552 "2022-02-06T03:18:58Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![sudgy](https://avatars.discourse-cdn.com/v4/letter/s/58f4c7/32.png) [@sudgy](https://discourse.rocq-prover.org/u/sudgy)\
**Post date:** [February 6, 2022, 3:18am UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552/1 "2022-02-06T03:18:58Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![sudgy](https://avatars.discourse-cdn.com/v4/letter/s/58f4c7/32.png) [@sudgy](https://discourse.rocq-prover.org/u/sudgy)\
**Post date:** [February 6, 2022, 3:20am UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552/2 "2022-02-06T03:20:33Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![olaure01](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/olaure01/32/733_2.png) [@olaure01](https://discourse.rocq-prover.org/u/olaure01)\
**Post date:** [February 6, 2022, 8:32am UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552/3 "2022-02-06T08:32:16Z")

</div>

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:

```coq
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:

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

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [February 6, 2022, 6:15pm UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552/4 "2022-02-06T18:15:52Z")

</div>

This reminds me of Charguéraud’s [`applys_eq`](https://www.seas.upenn.edu/~cis500/cis500-f16/sf/UseTactics.html)…

---

<div class="post-metadata">

**Author:** ![sudgy](https://avatars.discourse-cdn.com/v4/letter/s/58f4c7/32.png) [@sudgy](https://discourse.rocq-prover.org/u/sudgy)\
**Post date:** [February 6, 2022, 9:44pm UTC](https://discourse.rocq-prover.org/t/applying-a-theorem-that-doesnt-match-exactly/1552/5 "2022-02-06T21:44:06Z")

</div>

Thanks. eq\_ind\_r didn’t work, but applys\_eq worked perfectly.