应用部分实例化的引理

Question

让我们假设我们想要证明以下（完全人为的）引理。

Lemma lem : (forall n0 : nat, 0 <= n0 -> 0 <= S n0) -> forall n, le 0 n.

我们想申请nat_ind来证明这一点。这是一个可能的证明：

Proof.
  intros H n. apply nat_ind. constructor. exact H.
Qed.

但是为什么不直接在 apply 策略中使用 H，使用 apply (nat_ind _ _ H) 或 eapply (nat_ind _ _ H) 之类的东西呢？但是第一个失败了，第二个将剩余的目标隐藏在一个存在变量中。

是否可以在 apply 或其衍生物中跳过假设以指定其他论点，同时将它们作为证明其余部分的经典目标？

Answer 1

如果你这样做

intros. refine (nat_ind _ _ H _).

那么你只有

0 <= 0

离开了。这对你有用吗？

Answer 2

这部分证明

intros H n.
apply nat_ind, H.

将给你 0 <= 0 作为唯一剩下的子目标。

这种方法使用了 apply 策略，但没有回答问题的一般性，因为只有当你想实例化 last 参数时它才会起作用（问题中的示例就是这种情况）。这是 Coq 参考手册中的引述：

apply term_1 , ... , term_n

This is a shortcut for apply term_1 ; [ .. | ... ; [ .. | apply term_n ]... ], i.e. for the successive applications of term_(i+1) on the last subgoal generated by apply term_i, starting from the application of term_1.

此外，由于它只是语法糖，因此在问题的上下文中，该解决方案可能被认为是作弊（并且我猜是滥用 Coq 策略开发人员的初衷）。

Answer 3

另一种方法（比我的其他答案更通用）是使用 apply ... with ... 构造，如下所示：

intros H n.
apply nat_ind with (2 := H).

这里的2指的是nat_ind的归纳步长参数（参见Coq v8.5参考手册，8.1.3）：

In a bindings list of the form (ref_1 := term_1) ... (ref_n := term_n), ref is either an ident or a num. ... If ref_i is some number n, this number denotes the n-th non dependent premise of the term, as determined by the type of term.

应用部分实例化的引理

Apply partially instantiated lemma

coq