Coq:Ltac 内部的 "dependent induction"

Question

在 Ltac 中，依赖归纳对我来说似乎不同。并不是。

以下工作正常:

Require Import Coq.Program.Equality.

Goal forall (x:unit) (y:unit), x = y.
intros.
dependent induction x.
dependent induction y.
trivial.
Qed.

dependent induction这里是矫枉过正，因为 destruct工作得很好。此外，没有必要将事物命名为 destruct如果 Ltac 在证明脚本中编辑用于帮助:

Ltac ok :=
  match goal with
    | [H : unit |- _] => destruct H
  end.

Goal forall (x:unit) (y:unit), x = y.
intros.
ok.
ok.
trivial.
Qed.

然而，同样的 Ltac失败时 destruct被 dependent induction 取代:

Ltac wat :=
  match goal with
    | [H : unit |- _] => dependent induction H
  end.

Goal forall (x:unit) (y:unit), x = y.
intros.
wat.

(*
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).
*)

Set Ltac Debug除了 dependent induction 之外，没有提供其他有用的信息事实上，在 x 上都尝试过和 y .

奇怪的是，如果我结束了 dependent induction在另一个 Ltac没有匹配，并将其应用于与我实际想要进行归纳的术语相同的术语，一切都会顺利进行:

Ltac go H := let z := fresh in remember H as z; dependent induction z; subst H.

Ltac why :=
  match goal with
    | [H : unit |- _] => go H
  end.

Goal forall (x:unit) (y:unit), x = y.
intros.
why.
why.
trivial.
Qed.

这里发生了什么，为什么是 dependent induction看起来如此依赖上下文？

Answer 1

这确实是一个错误，已于 2015 年 3 月修复。