The Coq mailing list

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

I want to create a lemma and its proof from a definition.

I succeed in constructing a modified lemma from a typical definition. And now I would like to automaticaly associate a proof to complete the lemma definition.

Currently, I've got a general Ltac tactic which allows me to prove all the lemmas corresponding to the awaited definitions.

I'd like to know If there exists a simple way to automaticaly complete the proof in ML, after having declared the lemma with the Command.start_proof.

 

Yann Devisschere