Documentation of cbn and simpl is incorrect and behavior of cbn is inconsistent

[JasonGross]

Description of the problem

The documentation says:

These tactics apply to any goal. They try to reduce a term to something still readable instead of fully normalizing it. They perform a sort of strong normalization with two key differences:

• They unfold a constant if and only if it leads to a ι-reduction, i.e. reducing a match or unfolding a fixpoint.

• While reducing a constant unfolding to (co)fixpoints, the tactics use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls.

However, the actual behavior is a bit more insane:

Record foo := { x : nat ; y : nat }.
Definition plus2 := plus.
Definition plus3 := plus.
Arguments plus3 / .
Definition plus4 := plus.
Opaque plus4.
Axiom plus5 : nat -> nat -> nat.
Fixpoint plus6 (n m : nat) {struct n} :=
  match n with
  | O => m
  | S p => S (plus6 p m)
  end.
Opaque plus6.
Definition bar (a : foo) := plus a.(x) 0.
Definition bar2 (a : foo) := plus2 a.(x) 0.
Definition bar3 (a : foo) := plus3 a.(x) 0.
Definition bar4 (a : foo) := plus4 a.(x) 0.
Definition bar5 (a : foo) := plus5 a.(x) 0.
Definition bar6 (a : foo) := plus6 a.(x) 0.
Goal forall a, (bar a, bar2 a, bar3 a, bar4 a, bar5 a, bar6 a) = (0,0,0,0,0,0).
  destruct a; cbn.
  (* 1 subgoal (ID 34)

  x0, y0 : nat
  ============================
  (x0 + 0, plus2 x0 0, x0 + 0, bar4 {| x := x0; y := y0 |}, bar5 {| x := x0; y := y0 |}, bar6 {| x := x0; y := y0 |}) =
  (0, 0, 0, 0, 0, 0)
*)

Issuing

Arguments bar !_ / .
Arguments bar2 !_ / .
Arguments bar3 !_ / .
Arguments bar4 !_ / .
Arguments bar5 !_ / .
Arguments bar6 !_ / .

does not change this behavior. By contrast, simpl unfolds none of the bars without the Arguments directives and unfolds all of them with the Arguments directives.

Possibly related to #4555

Coq Version

8.12

[Zimmi48]

Feel free to review and improve the modified documentation for these tactics at #13707. You probably understand better than us how they work.

cc also @ybertot who has been working on making simpl and cbn more consistent.

[jfehrle]

BTW, it's better to say "is incorrect" rather than "lies". The latter implies an intention to deceive that I'm sure is not appropriate here.