Provide a tactic notation `dependent induction .. as ..`

[kyoDralliam]

Description of the problem

The dependent induction family of tactics provided by Coq.Program.Equality support quite a few variant similar to those of induction but no variant allowing to give names to the hypothesis produced by the elimination principle (the variant with an as clause for induction).

Here is my own naive attempt at providing such a notation:

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.

This attempt is not totally faithful to induction since it takes a simple_intropattern as an Ltac production item instead of a or_and_intropattern_loc (that does not seem accessible from Ltac).

Coq Version

Probably since the introduction of Program.

[herbelin]

This attempt is not totally faithful to induction since it takes a simple_intropattern as an Ltac production item instead of a or_and_intropattern_loc (that does not seem accessible from Ltac).

In the short term, adding or_and_intropattern for tactic notations would be possible. Something like adding let wit_or_and_intropattern = ... in plugins/ltac/tacarg.ml and adding the corresponding register (as shown by grep wit_simple_intropat plugins/ltac/*ml) should canonically do the trick.

I'm otherwise a bit lost about the "big plans" regarding tactics and tactic notations, so hints at least from @ppedrot may help to know how to converge in a common direction.

[Among the big plans, from a user point of view, I would naively say that it would be natural that induction eventually provide dependent induction.]