如何在不使用 Coq 中的泛化依赖的情况下以不同的顺序进行介绍

Question

鉴于我有forall n m，有没有办法做到这一点：

intros n m. generalize dependent n.

但是一步到位，只需应用intros(或替代策略(即可m？

Answer 1

你可能想要一些类似的东西(但有一个异构的列表，以便能够将这些策略应用于多分类望远镜(：

Require Import ListTactics.
Ltac introNthAcc n acc := match constr:n with
  | 0    => intro ; list_iter ltac:(fun x => generalize dependent x) acc
  | S ?n =>
     let H := fresh "H" in
     intro H ; introNthAcc n (cons H acc)
end.
Ltac introNth n := introNthAcc n (@nil Prop).
Goal forall a b c, a / b / c.
 introNth 1.

Answer 2

不幸的是，基本的Coq策略语言对于这种簿记步骤不是很好。我个人更喜欢使用 SSReflect 的，因为它们更经济。比较

intros n m. generalize dependent n.

与 SSR 等效

move=> n m; move: n.

请注意，如果你的定理是一个普遍量化的事实，你也可以把n和m直接放在冒号之前，从而节省第一个intros步骤，例如

Lemma my_lemma n m : P n m.
Proof.
move: n.
(* Rest of proof *)
Qed.

或者，更好的是，如果你在概括之后立即做induction，

Lemma my_lemma n m : P n m.
Proof.
elim: n.
(* Rest of proof *)
Qed.