3
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ Hello, welcome to PASE! 👋 $\endgroup$
    – ice1000
    Apr 29 at 4:59
  • $\begingroup$ @ice1000 I have been here for a long time, but didn't find anything I could contribute until then. $\endgroup$ Apr 30 at 4:40

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.