The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Not really what you're asking, but why aren't you just using the
"elim" tactic for that?

On Fri, Mar 24, 2017 at 10:34 AM, Nicolas Magaud 
<magaud AT unistra.fr>
 wrote:
> Hello,
>
> I would like to write a Ltac tactic which, from the type of a variable 
> (obtained using the function "type of”), retrieves and applies the 
> associated induction principle.
>
> If _x is of type nat, it applies nat_rect; if _x is of type t, it applies 
> t_rect (see example below).
>
> So far, I do it using Ltac pattern-matching, which is weird as “t” does not 
> belong to an inductive type and my Ltac function has to be extended 
> manually each time I handle a new inductive type.
>
> I would prefer something like (type of _x)^”_rect” which appends the 
> appropriate extension to the tacexpr1 returned by "type of”.
>
> Is there any way to do that using only Ltac (i.e. without writing any .ml 
> or .ml4 files) ?
>
> Nicolas Magaud
>
> ------
> Inductive t:=A|B|C.
>
> Ltac use_pattern _x:= pattern _x;
>     match goal with |- (?f _x) =>
>                     let t:= (type of _x) in
>                     match t with
>                     | nat => apply nat_rect
>                     | t => apply t_rect
>                     end end.
>
> Parameter P : t -> nat -> Prop.
>
> Lemma l : forall a n, P a n.
> Proof.
> intros.
> use_pattern a.
> Undo.
> use_pattern n.