从属归纳似乎对我来说在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失败：destructdependent 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看起来如此依赖上下文？