为什么去除假设会改变归纳策略的行为？

Question

我试图证明 various definitions of the reflexive-transitive closure 是等价的。这是有效的代码：

Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Relations.Relation_Operators.

Hint Constructors clos_refl_trans.
Hint Constructors clos_refl_trans_1n.

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A), 
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z _ IH1 _ IH2]; eauto.
  induction IH1; eauto.
Qed.

注意下划线表示丢弃的变量。如果我给这些变量命名，自动化就会失败：

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1; eauto. (* three subgoals left *)
Fail Qed.

经检验，我们发现第二个例子的内归纳假设较弱。看起来归纳策略正在检测有问题的假设与内部归纳对象之间的幕后依赖关系。

这在任何地方都有记录吗？原理是什么，我如何预测它会发生？

Answer 1

我认为基本上它会让你的归纳假设依赖于与你归纳的事物相关的所有假设。如果你在有 h : Q n 和 y : h = h' 的上下文中对 x : P n m 进行归纳，它可能会将它们包含在组合中。在很多情况下，这并不符合您的要求，事先做一些 clean 可能会使您的归纳突然通过。

induction 还有一个非常有用的变体，induction ... in 允许您指定在进行归纳时要保留的上下文部分。

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1 in z, IH2 |- *. all: eauto.
Qed.

这里你得到一个警告，老实说我不太明白（Cannot remove x和Cannot remove y）但是你得到了预期的结果。这还有一个好处，就是它可以让您指定应该概括的内容。

也许有人有更好的解释。

为什么去除假设会改变归纳策略的行为？

Why does removing assumptions change the behaviour of the induction tactic?

coq

coq-tactic