2

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

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

我不明白为什么我们需要:here 而不仅仅是做 Coq apply。事实上，如果我删除:，它工作得很好。为什么会有所作为？

4

2 回答 2

3

Indeed, apply: H1 ... Hn is to all effects equivalent to move: H1 .. Hn; apply. A more interesting use of apply is apply/H and its variations, which can interpret views.

于 2016-01-28T00:57:16.087 回答
2

我想我在阅读 SSReflect 文档时找到了答案。从本质上讲，ssr 重新定义了策略，apply例如它对目标的第一个变量而不是上下文中的某个变量进行操作。这就是:in 以 ssr 方式使用的原因apply: XX.（相当于），如果省略move: XX; apply.它也可以使用，因为这是传统的 Coq 方式。:

引用文档：

此外，SSReflect 重新定义了基本的 Coq 策略案例、elim 和 apply，以便他们可以更好地利用 ':' 和 '=>'。这些 Coq 策略需要来自上下文的论据，但要针对目标进行操作。它们的 SSReflect 对应物使用目标的第一个变量或常量，因此它们是“纯粹演绎的”：

they do not use or change the proof context. There is no loss since `:' can readily be used to supply the required variable.

于 2015-12-31T03:49:31.423 回答