The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Nicolas, here a small hack to do this, not sure this is really robust but hope this helps.

The idea is that "the associated induction principle." means "the constant you will find in your proof term when you do "induction"".

The ltac below performs a "induction" on a dummy proof and extract the head constant.

(* find the hd term of an application *)

Ltac hd_of_app t :=

  match t with

  | (?f _) => hd_of_app f

  | _ => t

  end.

Ltac find_rec h :=

  let typ := type of h in

  let X := constr:(fun x:typ => (ltac:(induction h;exact I)):True) in

  let app := eval lazy beta in (X h) in

  let hd := hd_of_app app in

  hd.

(* example: *)

Inductive t:=A|B|C.

Parameter P : t -> nat -> Prop.

Lemma l : forall a n, P a n.

Proof.

  intros.

  let schem := find_rec a in apply schem.

  Undo.

  let schem := find_rec n in apply schem.

Best,

P.

Le ven. 24 mars 2017 à 14:34, Nicolas Magaud <magaud AT unistra.fr> a écrit :

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.