coq - ssreflect/Coq中何时需要使用“:”(冒号)？

我试图从非反射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

是一个引理，说如果树的镜子是叶子，那么树就是叶子。

我不明白为什么我们在这里需要apply，而不仅仅是Coq :。实际上，如果我删除ojit_code，它就可以正常工作。为什么会有所作为？

最佳答案

实际上，apply: H1 ... Hn在所有方面都等同于move: H1 .. Hn; apply。 apply的一个更有趣的用法是apply/H及其变体，它可以解释视图。

关于coq - ssreflect/Coq中何时需要使用“:”(冒号)？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/34500893/