In the middle of my proof, this works
induction H1 as [ | | | | | | | | | ].
But, when I exchange it for
dependent induction H1 as [ | | | | | | | | | ].
I get "Error: Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]). "
Can you seriously not choose the names of your variables when doing dependent induction? That would be crazy; I really hope I just have the syntax wrong somehow.
Thank you.
After reading the code of Equality.v, here is an attempt to define a notation for dependent induction supporting the as clause.
From Coq Require Import Program.
Ltac elim_ind_as p pat := elim_tac ltac:(fun p el => induction p as pat using el) p.
Ltac do_ind_as p pat := introduce p ; (induction p as pat || elim_ind_as p pat).
Tactic Notation "dependent" "induction" ident(H) "as" simple_intropattern(pat) :=
do_depind ltac:(fun hyp => do_ind_as hyp pat) H.
(*Example:*)
From Coq Require Vector.
Definition head : forall {A} (n:nat), Vector.t A (S n) -> A.
Proof.
intros A n v.
(* induction v. Would not discard the case t A 0 *)
dependent induction v as [|a z v IH]. (* For some reason the `z` is renamed to `n`... *)
exact a.
Defined.
Note that it suffers some caveat: this notation use a simple_intropattern whereas the standard induction tactic use an or_and_intropattern_loc that does not seem accessible from Ltac.
I filed an issue at #12840.