6
$\begingroup$

I have this function:

Definition bexp x y := bexp_r x y [true].

And I have this goal:

value (bexp [] y) = 0 ^ value y

I want to replace the call to bexp with the underlying bexp_r. I tried to use the simpl tactic but it did not replace it.

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Please do not start your question with Coq:. You can use tags to express your intended topic etc. $\endgroup$
    – Trebor ♦
    Commented Apr 18, 2022 at 10:05

1 Answer 1

Reset to default
10
$\begingroup$

The tactic you are looking for is probably unfold. If you write unfold bexp it will replace it with its body.

In certain cases, unfolding the definition will unfold too much and if you want more control over it you can prove unfolding lemmas instead and rewrite with them.

Improve this answer
$\endgroup$
2
  • $\begingroup$ That's exactly what I was searching for, thanks a lot. $\endgroup$
    – user1231
    Commented Apr 16, 2022 at 19:55
  • $\begingroup$ For anyone who stumbled across this thread: "unfolding too much" can be reversed with fold. I often define Ltac refold f := unfold f; fold f and this often does what you want. $\endgroup$
    – shooqie
    Commented Jun 10, 2023 at 9:20

Your Answer

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