# Cbn vs simpl?

**URL:** <https://discourse.rocq-prover.org/t/cbn-vs-simpl/959>\
**Category:** Using Rocq\
**Created:** [July 22, 2020, 7:07am UTC](https://discourse.rocq-prover.org/t/cbn-vs-simpl/959 "2020-07-22T07:07:51Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jco](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jco/32/368_2.png) [@jco](https://discourse.rocq-prover.org/u/jco)\
**Post date:** [July 22, 2020, 7:07am UTC](https://discourse.rocq-prover.org/t/cbn-vs-simpl/959/1 "2020-07-22T07:07:51Z")

</div>

Pardon the dumb question, I was curious if the difference between these two tactics is elaborated somewhere? The manual just says that cbn is considered a “better” version, and it looks like they’re both opaque from within coq.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [July 23, 2020, 1:02pm UTC](https://discourse.rocq-prover.org/t/cbn-vs-simpl/959/2 "2020-07-23T13:02:16Z")

</div>

Oversimplified TLDR: Beginners should just use `simpl`. If the output is not what they’d want, they should try if `cbn` is better and/or learn about controlling `simpl` via `Arguments`. If that’s not enough, they should search in the coq bug tracker.

The manual does say a bit more on `cbn`:

> Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by [`simpl`](https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacn.simpl). For instance a constant defined by `plus' := plus` is possibly unfolded and reused in the recursive calls, but a constant such as `succ := plus (S O)` is never unfolded. This is the main difference between [`simpl`](https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacn.simpl) and [`cbn`](https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacn.cbn). The tactic [`cbn`](https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacn.cbn) reduces whenever it will be able to reuse it or not: `succ t` is reduced to `S t` .

In practice, one common reason for using `cbn` is when you are dealing with operational typeclasses — that is, typeclasses with only one method, used to overload operations; if you don’t know what they are, and the libraries you use don’t use them either, you can defer learning about this. I’m not aware of any operational typeclasses used in the Coq stdlib (but I might forget some), but such typeclasses are common in other libraries (e.g. math-classes and std++).

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [July 23, 2020, 1:17pm UTC](https://discourse.rocq-prover.org/t/cbn-vs-simpl/959/3 "2020-07-23T13:17:28Z")

</div>

> [@Blaisorblade](#):
>
> Oversimplified TLDR: Beginners should just use `simpl` . If the output is not what they’d want, they should try if `cbn` is better and/or learn about controlling `simpl` via `Arguments` . If that’s not enough, they should search in the coq bug tracker.

Asking on zulip may be a useful step between trying cbn and searching the bug tracker.