Dependent induction seems to work differently for me in an Ltac and not.
The following works just fine:
Require Import Coq.Program.Equality.
Goal forall (x:unit) (y:unit), x = y.
intros.
dependent induction x.
dependent induction y.
trivial.
Qed.
dependent induction is overkill here, since destruct works just fine. Furthermore, it's not necessary to name the thing to be destructed in the proof script if Ltac is used to help:
Ltac ok :=
match goal with
| [H : unit |- _] => destruct H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
ok.
ok.
trivial.
Qed.
However, the same Ltac fails when destruct is replaced by 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 gives no additional useful information, other than that dependent induction is, in fact, attempted on both x and y.
Strangely enough, if I wrap up the dependent induction in another Ltac without a match, and apply it to a term that is equal to the one I actually want to perform induction on, everything goes smoothly:
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.
What is going on here, and why is dependent induction seemingly so context dependent?
wat.fails in a more verbose way: "In nested Ltac calls to "wat", last call failed. Error: Ltac variable H is bound to x which cannot be coerced to a fresh identifier."whyandokboth work just fine. I'm still confused. - jbapple