Apply a function to both sides of equality in a Coq hypothesis

Question

The question I have is very similar to the one presented in the link below, but on a hypothesis instead of a goal.

Apply a function to both sides of an equality in Coq?

Say I have the following definition :

Definition make_couple (a:nat) (b:nat) := (a, b).

And the following lemma to prove :

a, b : nat
H : (a, b) = make_couple a b
-------------------------------
(some goal to prove)

I would like to generate the following hypothesis:

new_H : fst (a, b) = fst (make_couple a b)

One way is to write explicitly an assert, then use eapply f_equal :

assert (fst (a, b) = fst (make_couple a b)). eapply f_equal; eauto.

But I would like to avoid, if possible, to write explicitly the assert. I would like to have some tactic or equivalent that would work like this :

apply_in_hypo fst H as new_H

Is there anything in Coq that would come close to that?

Thanks for the answers.

Anton Trunov Anton Trunov · Accepted Answer · 2018-06-21T09:56:46

You can use f_equal lemma to do that.

About f_equal.

f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

Arguments A, B, x, y are implicit
Argument scopes are [type_scope type_scope function_scope _ _ _]
f_equal is transparent
Expands to: Constant Coq.Init.Logic.f_equal

Here is how you can apply it to a hypothesis:

Goal forall a b : nat, (a, b) = (a, b) -> True.
  intros a b H.
  apply (f_equal fst) in H.

The above snippet can be rewritten in a more concise manner using intro-patterns:

  Restart.
  intros a b H%(f_equal fst).
Abort.

Apply a function to both sides of equality in a Coq hypothesis

1 Answers