Merge PR coq#18602: Update of the doc of simpl and cbn, especially wr…

…t "simpl never". Reviewed-by: proux01 Ack-by: jfehrle Ack-by: SkySkimmer Co-authored-by: proux01 <[email protected]>
SkySkimmer · May 31, 2024 · 553f454 · 553f454
2 parents 19de843 + a9f2a31
commit 553f454
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 8 deletions.
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
@@ -334,18 +334,25 @@ Binding arguments to scopes
 Effects of :cmd:`Arguments` on unfolding
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-+ `simpl never` indicates that a :term:`constant` should never be unfolded by :tacn:`cbn` or
-  :tacn:`simpl`:
++ `simpl never` indicates that a :term:`constant` should not be unfolded by :tacn:`cbn` or
+  :tacn:`simpl` when in head position. Note that in the case of :tacn:`simpl`, the
+  modifier does not apply to reduction of the main argument of a `match`, `fix`,
+  primitive projection, or of an unfoldable constant hiding a `match`,
+  `fix` or primitive projection.
 
   .. example::
 
      .. coqtop:: all
 
-        Arguments minus n m : simpl never.
+        Arguments Nat.sub n m : simpl never.
 
-  After that command an expression like :g:`(minus (S x) y)` is left
+  After that command an expression like :g:`(Nat.sub (S x) y)` is left
   untouched by the tactics :tacn:`cbn` and :tacn:`simpl`.
 
+  Otherwise, an expression like :g:`(Nat.sub (S x) 0) + 1`
+  reduces to :g:`S (x + 1)` for :tacn:`simpl` because `Nat.sub`
+  is the main argument of `+` in this case.
+
 + A :term:`constant` can be marked to be unfolded only if it's applied to at least
   the arguments appearing before the `/` in a :cmd:`Arguments` command.
 

diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst
@@ -621,14 +621,32 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
 
    :tacn:`cbn` was intended to be a more principled, faster and more
    predictable replacement for :tacn:`simpl`.
-
-   The main difference between :tacn:`cbn` and :tacn:`simpl` is that
-   :tacn:`cbn` may unfold constants even when they cannot be reused in recursive calls:
-   in the previous example, :g:`succ t` is reduced to :g:`S t`.
+   The main difference is that :tacn:`cbn` may unfold constants even when they
+   cannot be reused in recursive calls: in the previous example, :g:`succ t` is
+   reduced to :g:`S t`. Modifiers such as `simpl never` are also not treated the same,
+   see :ref:`Args_effect_on_unfolding`.
 
    Setting :opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information.
    ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
 
+   .. example::
+
+      Here are typical examples comparing :tacn:`cbn` and :tacn:`simpl`:
+
+      .. coqtop:: all
+
+         Definition add1 (n:nat) := n + 1.
+         Eval simpl in add1 0.
+         Eval cbn in add1 0.
+
+         Definition pred_add n m := pred (n + m).
+         Eval simpl in pred_add 0 0.
+         Eval cbn in pred_add 0 0.
+
+         Parameter n : nat.
+         Eval simpl in pred_add 0 n.
+         Eval cbn in pred_add 0 n.
+
 .. tacn:: hnf @simple_occurrences
 
    Replaces the current goal with its