The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Definition K2DIAM_rwtmp:=forall decI decJ A W (t1 t2 : context I J A W)
> (i:I) (j:J),
>    (apply_rule (K2Diam i j) decI decJ (TDiamond j (Comma i t1 t2))) =
>    Some (Comma i t1 (TDiamond j t2)).
> )
> and getting coq's generated kind_of_term from them with Nametab.locate and
> an extraction of the constant from a ConstRef.
> I rather succeed in creating the transformation ML function generating the
> needed kind_of_term from the one of the definition and thanks to
> Command.start_proof, I succeed in automaticaly generate the lemma from the
> new kind_of_term.
> 
> Nevertheless, I still got a little problem : my lemma must contain a
> reference to my definition, with a kind_of_term :
> Const <Top#2>#SomeRules#K2Diam (to keep with the same example)
> (<Top#2> is a Module path with type MPself uid. and I didn't manage to watch
> the dir_path associated to the uniq_ident, "SomeRules" was the section name
> inside which I was working )
> 
> I still don't know how to easily and automaticaly generate this kind_of_term
> from my definition name (which module path generate, how to get the section,
> ...)

  I'm not sure that you need to enter this low-level representation of
names and paths. Nametab.locate gives you a "ConstRef cst" of type
constr that you can reuse as such (without re-building it from its
elementary components) in the statement of the lemma for which you
start a proof.

  Hugo Herbelin