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

【问题标题】：Why does removing assumptions change the behaviour of the induction tactic?为什么去除假设会改变归纳策略的行为？
【发布时间】：2020-02-13 18:15:54
【问题描述】：

我试图证明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.

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

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

【问题讨论】：

标签： coq coq-tactic

【解决方案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），但您会得到预期的结果。这还有一个好处是它可以让您指定应该概括的内容。

也许有人有更好的解释。

【讨论】：