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.
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
Arguments. If that’s not enough, they should search in the coq bug tracker.
The manual does say a bit more on
Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by
simpl. For instance a constant defined by
plus' := plusis 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
cbn. The tactic
cbnreduces whenever it will be able to reuse it or not:
succ tis reduced to
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++).
Asking on zulip may be a useful step between trying cbn and searching the bug tracker.