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?
-
$\begingroup$ Hello, welcome to PASE! 👋 $\endgroup$– ice1000Apr 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$– Qinshi WangApr 30 at 4:40
1 Answer
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
.