用COQ申请和申请

Question

对不起，这个问题含糊不清，但我很难理解apply和apply with之间的区别。

假设我有一个目标，什么时候应该使用apply，什么时候应该使用apply with？我的目标是形式:p，a，b，而我试图应用的引理，对于所有的a，b，如果我使用，它只是a-b常量。如果我用的是apply，它概括了a和b。

Answer 1

当你看一个定理陈述时，你可以检查普遍量化的变量是否出现在陈述的最后结论中。我所有的都会出现，你可以使用apply。如果其中之一没有，那么使用apply ... with ...通常更实用。

以下是两个例子。

Require Import Arith.
Check le_trans.
(* This says : 
  Nat.le_trans
   : forall n m p : nat, n <= m -> m <= p -> n <= p. *)
Check le_S.
(* This says :
 le_S
  : forall n m : nat, n <= m -> n <= S m *)
Check le_n.
(* This says :
 le_n
  : forall n: nat, n <= n *)m -> n <= S m

我正在从已经存在的Arith库中学习示例。这两个检查命令可以验证我们在同一个页面上。第一个关于le_trans的例子表明，在这个定理中有一个变量，在我的例子中名为y，它没有出现在最后的语句中。因此，在执行apply命令时，与手头的目标相比，这个y是不可猜测的。因此，这个定理是apply ... with ...的一个很好的候选定理。

下面是一个例子：

Lemma test_drive : forall x, x <= S (S x).
Proof.
intros x.
apply le_trans with (S x).
apply le_S.
apply le_n.
apply le_S.
apply le_n.
end.

当应用定理le_trans时，Coq系统可以通过简单地比较当时的目标：n应该是x，p应该是S (S x)，来猜测用于实例化变量n和p的值。对于m，应该给出一个值，apply希望用户给它，这就是我们使用with子句的地方。在这种情况下，我们可以简单地给出值(使用变量出现的顺序)。我们选择给S x。因此，我们得到了两个目标，一个是语句x <= S x，另一个是语句S x <= S (S x)。这两个目标都是le_S最后声明的实例。反过来，这个引理具有两个通用量化变量都出现在最后语句中的性质，因此可以使用不带with子句的with。

当我们想要使用引理le_n时，也会发生同样的情况。