Coq: Unify with a pattern and get the result

Question

I want to do change t with (f _), where t is a term and f is a function, but change does not allow placeholders in its second parameter. So I want to write a tactic that unifies t and (f _) and returns the result (f x), so I can change t with (f x). I know that t = f _ can be unified by reflexivity, but this approach adds redundancy to the proof term. Is there a nice way to do this task?

Answer 1

The following tactic unifies term with pattern and returns the result.

Ltac unify_to term pattern :=
  let eq_proof := constr:(eq_refl : term = pattern) in
  match type of eq_proof with
  | _ = ?result => result
  end.

Then we can use

let u := unify_to t uconstr:(f _) in
...

to get u = f x.