ssreflect/Coq 中什么时候需要 `:`（冒号）？
when is the `:` (colon) in necessary in ssreflect/Coq?
我试图根据非 ssreflect Coq 理解 Coq/ssreflect 证明中 :（冒号）的确切含义。
我读到它与将事物移向目标（如泛化？？）有关，与 => 相反，后者将事物移向假设。然而，我经常发现它令人困惑，因为无论有无 :，证明都可以工作。以下是教程中的示例：
Lemma tmirror_leaf2 t : tmirror (tmirror t) = Leaf -> t = Leaf.
Proof.
move=> e.
by apply: (tmirror_leaf (tmirror_leaf e)).
Qed.
其中，
tmirror_leaf
: forall t, tmirror t = Leaf -> t = Leaf
是一个引理，表示如果树的镜子是一片叶子，那么这棵树就是一片叶子。
我不明白为什么我们在这里需要 : 而不仅仅是 Coq apply。事实上，如果我删除 :，它就可以正常工作。为什么会有所不同？
我想我在阅读 SSReflect 文档时找到了答案。本质上，ssr 重新定义了 apply 这样的策略，使其对目标的第一个变量而不是上下文中的某些变量进行操作。这就是为什么 : 以 ssr 方式用于 apply: XX. 的原因（相当于 move: XX; apply.），如果省略 : 也有效，因为这是传统的 Coq方法。
引用文档：
Furthermore, SSReflect redefines the basic Coq tactics case, elim, and
apply so that they can take better advantage of ':' and '=>'. These
Coq tactics require an argument from the context but operate on the
goal. Their SSReflect counterparts use the first variable or constant
of the goal instead, so they are "purely deductive":
they do not use or change the proof context. There is no loss since
`:' can readily be used to supply the required variable.
的确，apply: H1 ... Hn 的所有效果等同于 move: H1 .. Hn; apply。 apply 的一个更有趣的用法是 apply/H 及其变体，它可以解释视图。
我试图根据非 ssreflect Coq 理解 Coq/ssreflect 证明中 :（冒号）的确切含义。
我读到它与将事物移向目标（如泛化？？）有关，与 => 相反，后者将事物移向假设。然而，我经常发现它令人困惑，因为无论有无 :，证明都可以工作。以下是教程中的示例：
Lemma tmirror_leaf2 t : tmirror (tmirror t) = Leaf -> t = Leaf.
Proof.
move=> e.
by apply: (tmirror_leaf (tmirror_leaf e)).
Qed.
其中，
tmirror_leaf
: forall t, tmirror t = Leaf -> t = Leaf
是一个引理，表示如果树的镜子是一片叶子，那么这棵树就是一片叶子。
我不明白为什么我们在这里需要 : 而不仅仅是 Coq apply。事实上，如果我删除 :，它就可以正常工作。为什么会有所不同？
我想我在阅读 SSReflect 文档时找到了答案。本质上，ssr 重新定义了 apply 这样的策略，使其对目标的第一个变量而不是上下文中的某些变量进行操作。这就是为什么 : 以 ssr 方式用于 apply: XX. 的原因（相当于 move: XX; apply.），如果省略 : 也有效，因为这是传统的 Coq方法。
引用文档：
Furthermore, SSReflect redefines the basic Coq tactics case, elim, and apply so that they can take better advantage of ':' and '=>'. These Coq tactics require an argument from the context but operate on the goal. Their SSReflect counterparts use the first variable or constant of the goal instead, so they are "purely deductive":
they do not use or change the proof context. There is no loss since `:' can readily be used to supply the required variable.
的确，apply: H1 ... Hn 的所有效果等同于 move: H1 .. Hn; apply。 apply 的一个更有趣的用法是 apply/H 及其变体，它可以解释视图。