Cbn vs simpl?

Using Coq
1

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.

2 Likes
2

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 . 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 and cbn . The tactic 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++).

2 Likes
3

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

1 Like