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.

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

1 Answer 1


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.

  • $\begingroup$ That's exactly what I was searching for, thanks a lot. $\endgroup$
    – user1231
    Apr 16 at 19:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy