The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Hi,

maybe it helps you, that Company-Coq has

" C-c C-a C-x extracts the current goal into a separate lemma. "

which might be quite useful in your case:

https://github.com/cpitclaudel/company-coq

-- Jan



On 22.01.19 13:25, Laurent Thery wrote:
> 
> Hi,
> 
> On 1/22/19 6:08 AM, Jeremy Dawson wrote:
>> So my question is, having decided during a proof that a particular lemma 
>> would be useful, how to I prove and use it?
> 
> If it is a local assertion that you will use only inside the proof,
> you can use the tactic have (ssreflect) or the tactic assert (standard
> Coq) to add it to the context.
> 
> If it is a global lemma, good practice is to abort the proof. Prove the
> lemma and then replay the proof.
> 

-- 
Jan Bessai (M.Sc.)
Wissenschaftlicher Mitarbeiter

Technische Universität Dortmund
Fakultät für Informatik - Lehrstuhl 14 Software Engineering
Otto-Hahn Straße 14
D-44227 Dortmund

Tel.: +49 231-755 77 64
Fax: +49 231-755 79 36
jan.bessai AT tu-dortmund.de
www.tu-dortmund.de


Wichtiger Hinweis: Die Information in dieser E-Mail ist vertraulich. Sie
ist ausschließlich für den Adressaten bestimmt. Sollten Sie nicht der
für diese E-Mail bestimmte Adressat sein, unterrichten Sie bitte den
Absender und vernichten Sie diese Mail. Vielen Dank.
Unbeschadet der Korrespondenz per E-Mail, sind unsere Erklärungen
ausschließlich final rechtsverbindlich, wenn sie in herkömmlicher
Schriftform (mit eigenhändiger Unterschrift) oder durch Übermittlung
eines solchen Schriftstücks per Telefax erfolgen.

Important note: The information included in this e-mail is confidential.
It is solely intended for the recipient. If you are not the intended
recipient of this e-mail please contact the sender and delete this
message. Thank you.
Without prejudice of e-mail correspondence, our statements are only
legally binding when they are made in the conventional written form
(with personal signature) or when such documents are sent by fax.