Skip to Content.
Sympa Menu

coq-club - [Coq-Club] generate a lemma from a definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] generate a lemma from a definition


chronological Thread 
  • From: "Devisschere Yann" <devissch AT enseirb.fr>
  • To: <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] generate a lemma from a definition
  • Date: Tue, 29 Mar 2005 12:31:08 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I've got several definitions
(ex :
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)))).
)
and I want to automaticaly generate corresponding lemmas which have simple
corresponding structures
(ex :
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)).
)
(note here the product becomes an equality, Pvar i becomes ti, pdiam becomes
TDiamond, ...)

I succeed getting the corresponding kind_of_term by temporarily declaring a
second definition
(ex :
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,
...)



Yann Devisschere





Archive powered by MhonArc 2.6.16.

Top of Page