我试图以非 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
。事实上,如果我删除 :
,它就可以正常工作。为什么会有所不同?
最佳答案
确实,apply: H1 ... Hn
对于所有效果等同于 move: H1 .. Hn;应用
。 apply 的一个更有趣的用法是 apply/H
及其变体,它们可以解释 View 。
关于coq - ssreflect/Coq 中何时需要 `:`(冒号)?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34500893/