The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Nicolas,

  you could associate a typeclass instance to each induction principle and key the class by the associated inductive type.

-- Matthieu

On Tue, Apr 11, 2017 at 2:47 PM Dan Frumin <dfrumin AT cs.ru.nl> wrote:

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.