The Coq mailing list

[Nicolas Magaud <magaud AT unistra.fr>]

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.