From a9f2a31ec1a36d112219ee8b9ebde02f55127aa2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 1 Feb 2024 11:51:34 +0100
Subject: [PATCH] Update of the doc of simpl and cbn, especially wrt "simpl
 never".

---
 .../language/extensions/arguments-command.rst | 15 ++++++++---
 doc/sphinx/proofs/writing-proofs/equality.rst | 26 ++++++++++++++++---
 2 files changed, 33 insertions(+), 8 deletions(-)

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 6fafe26b9e3d..45e38e1e9af5 100644
--- 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
index e70f43777dea..636146d40f0a 100644
--- a/doc/sphinx/proofs/writing-proofs/equality.rst
+++ b/doc/sphinx/proofs/writing-proofs/equality.rst
@@ -630,14 +630,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