A Document-Oriented Coq Plugin for TEXmacs
Abstract:
This article discusses the integration of the authoring of a mathematical document
with the formalisation of the mathematics contained in that document. To
achieve this we have started the development of a Coq plugin for the TEXmacs
scientific editor, called tmEgg. TEXmacs allows the wysiwyg editing of mathematical
documents, much in the style of LATEX. Our plugin allows to integrate into a
TEXmacs document mathematics formalised in the Coq proof assistant: formal definitions,
lemmas and proofs. The plugin is still under development. Its main current
hallmark is a document-consistent interaction model, instead of the calculator-like
approach usual for TEXmacs plugins. This means that the Coq code in the TEXmacs
document is interpreted as one (consistent) Coq file: executing a Coq command in
the document means to execute it in the context (state) of all the Coq commands
before it.