依存性誘導は、私にとっては違った働きをするようです。 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 一見そうコンテキスト依存？
回答：
回答№1は1これは確かにバグであり、2015年3月に修正されました。