The Coq mailing list

["Devisschere Yann" <devissch AT enseirb.fr>]

Hi.

 

Let's assume I have such a definition :

 

Definition K2Diam (i:I) (j:J) : strucrule I J :=

((pdiam j (pcomma i (pvar 1) (pvar 2))),

 (pcomma i (pvar 1) (pdiam j (pvar 2)))).

 

I want to write a function in ML allowing me to write in coq :

add_lemma_rw K2Diam.

to automaticaly generate the lemma :

 

Lemma K2DIAM_rw: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)).

 

(perhaps eventually also defining its proof automaticaly)

quite like do add_morphism in setoid_replace (and like what Antonia Balaa did in term_const with recursive_definition).

 

In order to do that, I wanted to get internal representation of the definition and modify it according to a defined morphism, to construct the lemma definition and declare it.

I tried using the function parse_vernac but that doesn't really match with kind_of_term which seem to be the good object to use to do such things.

 

Can you confirm kind_of_term is what I need to use ?

And then, tell me what function I can use to get the kind_of_term representation ?

 

Yann Devisschere