The Coq mailing list

[Dan Frumin <dfrumin AT cs.ru.nl>]

Hi Nicolas,

It seems that the problem boils down to "how to concatenate an identifier 
name and a string in Ltac". I had a similar problem and basically I didn't 
find any solutions for this.

Do you know how to do this using an .ml module?

Best
Dan 

> On 24 Mar 2017, at 14:34, 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.