更多关于符号 （可选） More on Notation

（一般来说，标有可选部分的章节不需要遵循书的其余部分，但可能的其他可选部分除外。一读时，您可能需要浏览这些部分，以便您知道哪些内容供将来参考。 回想一下中缀加号和时间的符号定义：

Notation "x + y"

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.

Notation "x * y"

Notation "x * y" := (mult x y)
                      (at level 40, left associativity)
                      : nat_scope.

对于 Coq 中的每个符号，我们可以指定其 precedence level 及其 associativity 。优先级 n 通过 at level n 写入来指定：这有助于 Coq 解析复合表达。关联设置有助于消除包含相同符号多次发生的表达式。例如，上面指定的 + 和×的参数说，表达式 1 + 2 * 3 * 4 是速记（1+（2*3）*4）。Coq 使用从 0 到 100 的优先级，以及左、右或无关联性。稍后我们将在 Lists 章节中看到更多这方面的例子。

每个符号还与一个符号作用域相关联Coq试图从上下文中猜测范围是什么意思，所以当它看到S（O×O）时，它猜 nat_scope ，但是当它看到产品类型 bool×bool （我们将在以后的章节中看到），它猜测type_scope。有时，有必要通过书写(x × y) % nat来帮助它解决百分比符号问题，有时在 Coq 打印的内容中，它会使用 %nat 来指示符号的范围。 符号范围也适用于数字符号（3，4，5，42等），所以你有时可能会看到 0%nat ，这意味着O（我们在本章中使用的自然数字 0 ），或 0%Z ，这意味着整数零（它来自标准库的不同部分）。 专业提示：Coq 的记号机制不是特别强大。不要期望太高。

固定点和结构递归（可选） Fixpoints and Structural Recursion

Fixpoint plus'

Fixpoint plus' (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus' n' m)
  end.

当 Coq 检查此定义时， 它注意到 Plus' "在第一个参数上正在减少" 。这意味着，我们正在对论点进行结构性递归，即我们只对严格较小的 n 值进行递归性调用。这意味着所有 plus' 的调用最终将终止。Coq 要求每个修复点定义的一些论点正在 "减少" 。

此要求是 Coq 设计的一个基本特征：特别是，它保证 Coq 中可以定义的所有功能都会在所有输入中终止。但是，由于 Coq 的"递减分析"不是很复杂，有时有必要以稍微不自然的方式编写函数。

练习 Exercise

9: 2 stars, standard, optional (decreasing)

要具体了解这一点，请找到一种方法来编写一个明智的 Fixpoint 定义（比如数字上的简单函数），该定义确实会终止所有输入，但 Coq 会因为这一限制而拒绝。（如果您选择将此可选练习作为家庭作业的一部分，请确保您评论您的解决方案，以免导致 Coq 拒绝整个文件！