coq - ssreflect/Coq 中何时需要 `:`(冒号)？

Question

我试图以非 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。事实上，如果我删除 :，它就可以正常工作。为什么会有所不同？

Answer 1

确实，apply: H1 ... Hn 对于所有效果等同于 move: H1 .. Hn；应用。 apply 的一个更有趣的用法是 apply/H 及其变体，它们可以解释 View 。