Home

as Authoring Tool for Formal Developments - Informatik - FB3

image

Contents

1. A set of SCHEME scripts to accomodate the ETRX and CoQ scripts expor tation filters The last two components are available from the TEX cg user interface Reusing TEX macros in the TEX cg is possible through the import facility Conversely exportation of TEXmacg macros to BTEX macros or environments is not yet offered by TEX acs For documentation purpose our modified COQ distribution provides a new wrapper for the coqtop program named tmdoc A generic utilization consists in running the command tmdoc MyScript v which results in the TEXmacs file MyScript tm Other output formats directly available from tmdoc are TeX SCHEME However as shown in figure these formats together with HTML and POSTSCRIPT are also available by editing MyScript tm Let us illustrate further through two complete examples in the two follow ing sections 3 1 The COQ Standard Library Let us have of look at the very beginning of the theories Init Wf v file from the Coq standard library xi Id Wf tm v 1 1 2003 05 27 11 30 57 paudebau Exp ix This module proves the validity of well founded recursion also called course of values well founded induction from a well founded ordering on a given set Require Logic Require LogicSyntax Well founded induction principle on Prop Variable A Set Variable R A gt A gt Prop The accessibility predicate is defined to be non informative Inductive Acc A g
2. Fig 4 Document Type Definition for the TeXmacs Documents 4 2 COQ script re exportation In the introduction we have explained the need for going back and forth be tween the Coq formal development and the document edited with TEX sacs Hence the re exportation towards a COQ script is required As a matter of consequence we need also keep the documentation or informal part into the exported script in order to recover this part afterwards coming back to the documentation step Assume we are dealing with a TFEXmacg document generated from a de velopment Among all the material present in this document our tool ensures that any vernacular command is perfectly identified with the help of a spe cific macro or environment as already noticed Thus it is an easy task 15 AUDEBAUD RIDEAU thanks to TFXmacg s GUILE facility to recover in the correct order all the vernacular commands among the rest of Coq irrelevant material within the document Once collected and converted into the actual COQ concrete syn tax these pieces of text compose the Coq script s active part that is thus extracted from the TEXmacs document as shown in figure Everything else is considered as documentation To some extent this could be inserted as comments into the script but comments are thrown away by the Coq lexical analyzer In order to collect the documentation provided in the source script we had to change the lexer behavior so that not al
3. x x n c which depends heavily on the Notation enhancement mechanism one prefers to see Lemma 1 1 Set_nrootIR Yn N0 lt n gt Yc R0 lt c Jr R0 lt ENEO C or even better Lemma 1 2 For every positive integer n and non negative real number c there exists a non negative real number x such that x c This last presentation is easier to read hence it provides a better presentation for the formal statement within an article aimed for diffusion This raises several questions about pretty printing existing documents Is the verbatim output as shown in sufficient to make it possible to display or the two lemmas shown above It should be clear that nothing is possible unless the text from is re parsed in order to grab enough information on the actual structure of this code fragment The next question is what is the best internal representation abstract syntax which is capable of providing the information required to make the various displays possible And at what cost Finally what is the best way to generate the various styles and the formats The user expects other features as well For instance he might want to modify imported fragments to make them more readable or easier to under stand Thus variable renaming hypotheses reorganization or other changes at the presentation level should be possible while keeping the formal develop ment correct with respect to t
4. article presenting the formal development was within the capabilities of the scientific editor TEX cg The fact that this editor supports the GUILE SCHEME extension language has also made it possible to handle the second case beyond our initial expec tations We provide Coq and BIFX exportation functions both through the editor interface and as stand alone scripts which offer at the same a certifica tion mechanism on the COQ script and the article production in the format commonly accepted by the scientific community Beyond these tools our experimentation has shown very attractive per spectives We want to achieve the functionality allowing the user to interact with the prover in a mode as transparent as possible That means that the user will be allowed to write definitions lemmas and the other mathematical material in the syntax offered by the editor leaving to the system all the con versions to be done in order to match the actual concrete syntax understood by the prover Our view is that TEXmacsg offers a nice interface for abstraction with respect to the prover The interface can be adapted so that the user s syntax and commands do not depend on the prover As such this interface should offer a convenient support to teach beginners students for instance how to develop formal proofs Even the certification mechanism could allow for machine assisted verification of students examinations We consider our current experiments as an
5. command introduced in the last version of CoQ that permits the kind of enhancement that formula uses for the verbatim output While this is not at all nec essary in our tool see RSA example below at this stage of our development we decide to represent these nodes as special nodes in the generated structure 8 AUDEBAUD RIDEAU 2 2 2 Inductive definitions Cog provides specific outputs in many contexts not only for formulas Let us have a look at the Inductive vernacular command The Coq standard library provides many examples From Datatypes unit the sum of two sets A B is inductively defined as Inductive sum A B Set Set inl A gt sum A B inr B gt sum A B It is worth noting that the concrete syntax is usually chosen on the basis of i its ability to be read easily by the human reader ii and its ability to be read automatically hence understood by the com puter Come to think of it both points would hold if we switched humans and com puters as well The important thing to keep in mind is that for both points it should be possible to infer from the concrete representation that an inductive definition is structurally made of a finite sequence of named items inl inr in this example as constructors with respective type information Also the syntax A B Set means that sets A and B are parameters in the definition the result being a set as the fragment Set shows Therefore an inducti
6. concerned the user expects to be allowed to customize the look on file basis on whole development basis or even de pending on whether the resulting document is about to be browsed or printed on paper TEXmacs fulfills this criterion without requiring any special or additional code Moreover TEX 4cg also supports the GUILE SCHEME extension language 6 AUDEBAUD RIDEAU so that it is easy to customize the interface and write extensions to the ed itor at the user level Browsing is possible between distinct files as well as through the web Automatic content generation includes indices tables fig ures and bibliographies TEXmacg documents are saved as structured text files using a simple notation system which helps automatic machine driven search Therefore as a whole TEXmacg presents many attractive features which make it an interesting candidate in the context of authoring scientific documents 2 1 1 Communication with computer algebra systems Among our motivations interactivity with the theorem prover assistant was also required As such TFEXmacs provides a session mode that also offers the same combination of editing and command execution as EMACS does for many computer algebra systems the operating system shell and a Guile Scheme top level Figure presents a short session with MAPLE I W 1 Maple I l _ Copyright by Waterloo Maple Inc MAPLE All rights reserved Maple is a registered trademark of aag a
7. documentation on the COQ site 3 2 RSA Formalization RSA is an asymmetric public key encryption algorithm which relies on prime number factorization Its correctness has been formalized in various proof assistants including Coq by J C Almeida and more recently by L Th ry The complete formalization consists of half a dozen CoQ scripts available at In Binomials v one finds the well known Pascal statement on binomals Theorem exp_Pascal a b n nat power plus a b n sum_nm On k nat mult binomial n k mult power a minus n k power b k While the fragment does not contain any hint for presentation the structure generated by tmdoc is rich enough to allow for user macro definitions so as to provide the following output Theorem 6 exp_ Pascal Va b n nat a b g Ak nat p a E BF Observe however that the sum does not use the index k as one would expect This is going to be a slight enhancement in the next stage of our development In short this requires that macro definition can inspect the structure of its arguments and in our case grabs the k loop index to put it under the X symbol For a complete presentation of our contribution to this development the required material is available from TMCoOQ web site Besides the same documentation interface as for the standard library our contribution offers also a mechanism for automatically generating an article from the set of f
8. important step in this direction 19 AUDEBAUD RIDEAU References 1 Isabelle Theorem Proving Environment http isabelle in tum de and http www cl cam ac uk Research HVG Isabelle 2 The Maple analytical computation software http www maplesoft com 3 Mathematica The Way the World Calculates http www wolfram com products mathematica 4 Philippe Audebaud and Laurence Rideau Cog integration within TEX acs Home page http www sop inria fr lemme Philippe Audebaud tmcoq 5 Jean Christophe Filliatre Documentation tool for Cog Available at http www lri fr filliatr coqdoc 6 SRI Computer Science Laboratory The PVS Specification and Verification System http pvs csl sri com 7 Lemme Team INRIA Sophia Antipolis Pcog A graphical user interface for Coq Home page http www sop inria fr lemme pcoq 8 Cornell Prl Automated Reasoning Project MetaPRL http cvs metaprl org 12000 metaprl1 default html 9 Coq Team The Coq Theorem Prover Assistant Available at http coq inria fr 10 Laurent Th ry A proof of correctness of RSA algorithm that relies on Fermat s little theorem Browsable online at ftp ftp sop inria fr lemme Laurent Thery Rsa index html 11 MOWGLI Mathematics on the Web Get it by Logic and Interfaces European IST Home page http www mowgli cs unibo it 12 Philippe Audebaud and Luca Padovani D4 c Prototype functionalities for assisted annotation In Mo
9. need to do more work than a simple lexical analysis At least a syntax analysis is required We will show that this is actually sufficient However before this we have to choose between writing another parser for our purposes or benefiting from the existing one present in the Coq source There are two major arguments to take into consideration First COQ is a research tool still subject to changes even with respect to its concrete syntax Second the syntax allowed at the formula level requires a very complex parser Therefore the necessary synchronization would already suggest that we develop our tool as part of the COQ source tree rather than another stand alone program But we can do better than just sharing the parser Our code can also be used to interface COQ with any external tool that requires exchanging data with COQ for example PCoaq 2 2 1 Formulas Consider the following example whichever notation one might choose the internal structure for the above term not_all_ex_not is a tree product binders list arrow type negation EXT application product 2 ss ee binders list Fig 3 Tree representation for not_all_ex_not and the corresponding representation in TEX cg format is V binder_list P U Prop arrowc N _ Wn U appc P n NEXT_ _ _ EXT n U gt Pr The binder_list arrowc and appc nodes should be obvious from the above tree The N _ and NEXT_ _ _ come from the extendible Notation
10. we have experimented with TEX acg interactive mode with Coq In section we have shown that the editor TEX cg offers a session mode with external programs To make such communication possible with COQ very little is needed as the following session with Coq shows A sample session is presented in figure From this example we can make some useful observations Up to now our explanations were mainly concerned with formulas Actually exporting a full script does not raise any more difficult issues But when interacting with Coa it appears that the prover really decides the presentation in various contexts The information displayed during a proof session error messages or answers to vernacular 17 AUDEBAUD RIDEAU LG Welcome to Coq 7 4 Feb 2003 S Interactive Session A Coq lt Print all all AA Set P A Prop Vx A P x VA Set A Prop Prop Coq lt Lemma 1 foo Va b Prop a gt b gt aA b Va b Prop a gt b a Ab foo lt Intros a Prop b Prop H a H0 b a b foo lt Split 2 sub goal s a Subgoal 2 is b foo lt Exact H v foo lt Trivial Subtree proved foo lt Save foo is defined Coq lt Print f Error 6 7 Error f not a defined object Coq lt Print foo foo Aa b Prop H a HO b lt a b gt H HO Va b Prop a gt b aA b Coq lt Print bool Inductive 2 bool Set true bool false bool Fig 5 A sample session with T
11. MCOQ 18 AUDEBAUD RIDEAU commands are controlled by the prover The most interesting issue concerns proof editing Along the lines of the above session one would expect the editor to allow the user to edit the proof script rather than accumulating steps in the buffer This is possible in TEXmacs thanks to the SCHEME extension language and provided through specific tree commands together with the possibility for the document to be modified by the running program as well as the user or the editor interface 5 Conclusion and Perspectives Our initial motivation was to offer the users more powerful solutions for doc umenting their COQ formal developments Existing tools already offer useful means but lack the capability to render such mathematical or logical develop ment in the usual language for scientific documents and none of them permit significant modifications or even final adjustments while preserving the fun damental property that the underlying formal document has been certified by the prover In the first case we conclude that this is only possible at the cost of working behind a dedicated parser Due to complexity of the language dealt with by CoQ and also motivated by the purpose to share our work and offer CoQ various output formats we decided to implement our documentation generator tmdoc as part of the COQ source distribution At this stage the rendering of mathematical formulas and the possibility to prepare a scientific
12. UITP 2003 Preliminary Version TEX po a8 Authoring Tool for Formal Developments Philippe Audebaud Lemme Project INRIA Sophia Antipolis France Laurence Rideau 2 Lemme Project INRIA Sophia Antipolis France Abstract We present an authoring tool for publication and dissemination of formal theories certified by a proof assistant We have used TeXmacs a wysiwyg editor for scien tific documents which allows a connection with symbolic systems and we evaluate this tool on our formal developments certified using Coq Key words Certification Authoring Tool Proof Assistant Formal Development Structured Document IATFX 1 Introduction We present a toolkit named TMCoQ helpful for users who have validated some formal developments with a theorem prover assistant such as Coq and who want to ready their work for a scientific publication or online browsing As such we assume the user s main requirements are firstly to be able to present their work in the usual language for a mathematical article and sec ondly to preserve the property that the underlying development still remains certified by the prover For the first goal we offer a powerful tool which pro vides BIFX quality typesetting for presenting the formal development and its documentation together To preserve correctness of the development at each 1 Email Philippe Audebaud sophia inria fr 2 Email Laurence Rideau inria fr This is a preliminary versio
13. WGLI deliverables http mowgli cs unibo it misc deliverables interfaces 13 Joris van der Hoeven The GNU TeXmacs free scientific text editor Available at http www texmacs org 20
14. ation frag ments are inserted in the appropriate comment regions Second and more importantly this target is evidence that one can extract from the enriched document the parts which concern the user formal development this new script must be accepted by the prover afterwards 1 2 Some examples Our tool is not tightly coupled to a given theorem prover In the future it should even be an independent tool However we begin with a case study of our formal developments which are mainly done using the Coq theorem prover Thus the presented examples use Coq syntax Let us take a simple example Note that in Coq concrete syntax X A B stands for the the universal quantification VX A B A for the logical negation A while EXT x C P is meant for the existential connective dx C P x Welcome to Coq 7 4 Feb 2003 Coq lt Classical_Pred_Type Coq lt Check not_all_ex_not not_all_ex_not U Type P U gt Prop n U P n gt EXT n U P n 4 AUDEBAUD RIDEAU Therefore instead of displaying the type of not_all_ex_not as U Type P U gt Prop m U P n gt EXT n UI P n 1 one would rather see VU Type P U Prop Wn U Pn gt an U Pn 2 Eventually one would even hope to have the possibility of pretty printing this statement in natural language For instance instead of the raw CoQ lemma Lemma Set_nrootIR n nat 1t 0 n gt c IR Zero lt c gt x IR amp Zero lt
15. he underlying proof assistant Such demands are reasonable since one cannot expect any automatic generation from a formal development to provide any article ready text As soon as interactive editing introduces changes with respect to the initial development there is a possi bility for introducing errors It is these errors we would like to avoid with our tool AUDEBAUD RIDEAU 2 Software Design Decisions To build our tool we have decided to use TEXmacsg to write scientific articles and we have developed an extension for handling Coq input and output The resulting system named TMCOQ implements the functionalities described in figure where editor is TEXmacs Exportations to and translations between the different formats TEXmacs POSTSCRIPT are handled by the native TEXmacsg system but TMCOQ needs to have control on the macros expension mechanism to avoid the lost of the structure information This is the prereq uisite for BTFX exportation as well as for re exportation toward COQ script syntax from a TEXy cg document see section for more details Regarding the Proof Assistant issue we restrict ourselves to COQ devel opments for experimental purposes with the long term objective to build a tool adaptable to various theorem prover systems 2 1 The scientific editor GNU TREX acg Quoting its documentation page GNU TEXmacg ts a free scientific text editor which was both inspired by TEX and GNU Emacs The editor allow
16. iles This is based on a SCHEME script which is easily configurable 13 AUDEBAUD RIDEAU 4 Enhanced Features One of our initial goals was to preserve the invariant that the script part of the document remains certifiable by the prover at any time For this purpose we have developed several functionalities described below and based on the following remarks In the introduction we stated that a COQ script is a source program where the inactive regions tagged as comments are good places for inserting documentation The writing of an article from a formal development gives us another view Everything is printable text unless the macros or environments treat elements differently In Knuth s view everything each character could be active However for the casual user the symbol is commonly known as the first character of a document fragment which is going to be executed by the TFX engine So the key idea is that the user is working in a dual world with respect to program source editing Our tool transforms any program source file into a dual document source file since TEXmacsg is basically working in the same way as TRX Another property we get with the TEXmacsg view of our document is that it is strongly structured This structure allows us to introduce various inter esting features including communication with XSLT oriented tools Coq script recovery BIFX exportation and interactive certification This is made pos sible beca
17. l the comments are ignored However doing this in every place where comments may occur would result in a parser with unreasonable complexity We decided on a model where documentation and code alternate but no documentation is looked for within the vernacular commands Documentation fragments may appear in many places within the TEXmacg representation of a given script We ensure that they do not get lost through the exportation step by placing them in places where the modified Cog lexer is able to find them However we cannot guarantee that their exact position is preserved 4 8 ETRX exportation TEXmacg already supports ERX exportation However the documents we are dealing with are particular ones Therefore we have split the exportation in two steps where the first one profits from the fact that we are able to identify the fragments specific to COQ among the whole document This first step is designed as a GUILE script filter which can be rewritten by the user at will Selecting the exported material can be locally tuned inside the document source by assigning values to specific variables locally following the same idea as marking a fragment as math bold or italic Afterwards everything is put in the hands of the common ETRX exportation filter This solution offers both portability and enough expressiveness from the user point of view 4 4 COQ TEXyracs Let us have a look at the coq tex tool provided with Coq distribution This i
18. n The final version will be published in Electronic Notes in Theoretical Computer Science URL waw elsevier nl locate entcs AUDEBAUD RIDEAU step our approach to the second goal is to work always on the whole develop ment but to provide different views on this development For documentation purposes the user would prefer to be able to see the whole development while the article is a selected view on the fully documented development displaying only fragments of the whole development code A first solution that comes to mind consists in writing a BTEX document This is how one typically diffuses his results inserting in places selected pieces of the formal development This method has obvious drawbacks The cut and paste process may introduce errors when the formal development had none Any modification in the development requires the synchronization in the article otherwise making the latter inaccurate or even wrong with respect to the certification step performed using the theorem prover The inserted pieces of source code are introduced verbatim which means that the syntax could be quite far from usual mathematical language and natural language as well Notation and informal explanations are thus very different from the formal text The theorem prover syntax may even change introducing another source of misunderstanding To find a better solution to our problem let us have a closer look at what makes up such a formal development in C
19. nak gt Waterloo Maple Inc Type for help Interface with TeXmacs by Christian Even c 2002 Maple i f x gt x 3 sin x f 2 23 sin x Let us evaluate this function on the default value of 7 Maple 2 f evalf Pi 31 00627669 Maple 3 Pi Maple 4 int f x x Jat cos x Fig 2 A sample session with MAPLE We see that the presentation facilities are automatically available for the output generated by MAPLE the TEXmacs interface interprets the BIpXoutput generated by MAPLE Note that the session is allowed at any place within the document Actually TEXmacsg permits editing commands to be applied during the session multiple interruptions as well as the interleaving of computations and explanations This session mode benefits to some extent from the standardization of mathematical notation and the relative simplicity of the concrete syntax found in Computer Algebra Systems CAS Also it must be emphasized that PTEX output is offered by MAPLE MATHEMATICA and other CAS which shows that the CAS must be adapted in order to gain richer output Finally 7 AUDEBAUD RIDEAU note that the session mode is closer to the interaction the user gets with a calculator or a Unix shell than what is expected for developing proofs with the help of a Theorem Prover Assistant TPA 2 2 On the COQ side To go further than COQDOC our work proposes a solution to offer richer output formats to COQ So we
20. ned the most general DTD see figure which does not restrict to documents generated by tmdoc but describes any TEXmacg document as made of several paragraphs and enriched 14 AUDEBAUD RIDEAU with special macros and environments in a same way as we are used to with TeX documents Since we concluded our experiment TEXmacs has also been enriched with such a format although based on a different view and consequently without a generic DTD From both MOWGLI and TMCOQ sides our approach is robust enough for not requiring more than rewriting the outputs generated by templates into stylesheets owing to the common structural approach Hence we are going to provide the same functionality for TEXmacg users Liss texmacs dtd v 1 0 gt lt ENTITY TeXmacs PUBLIC TeXmacs DTD TeXmacs Document EN http www sop inria fr lemme Philippe Audebaud tmcog texmacs dtd gt lt Document structure gt lt ELEMENT document paragraph gt lt ELEMENT paragraph macro sym spc gt lt ELEMENT macro document paragraph gt lt ATTLIST macro name CDATA REQUIRED gt lt ELEMENT spc EMPTY gt lt Takes care of specials like lt rightarrow gt symbol within text o lt ELEMENT sym EMPTY gt lt ATTLIST sym arg CDATA REQUIRED gt lt Symbols gt lt ENTITY HTMLlat1 PUBLIC W3C ENTITIES Latin 1 for XHTML EN http www w3 org TR xhtm11 DTD xhtml lat1 ent gt YHTMLlat 1
21. on as far as we know For Isabelle isatool provides a batch BTEX document generator In Coq context this functionality is per formed by Coqpoc which offers TEX and HTML as output formats from scripts This tool makes a simple lexical analysis which is sufficient for the generation of hyper links for identifiers and index tables for the various 2 AUDEBAUD RIDEAU sorts of statements The vernacular sentences are simply inserted verbatim in the generated document Such a tool still fails to present the formal devel opment fragments in a user friendly syntax as independent as possible from changes on the CoQ side Also documentation and code still belong to dif ferent worlds It is not possible to make forward references insure uniform notation throughout the generated document While the process has been automated thus less prone to human errors the result is still bound to the version of COQ used for the certification 1 1 Objectives The dissemination of formal developments in scientific articles or by code distribution on the Web is an important part of the development s life cycle so we want to make a tool to help the user perform this task with the assurance that the correctness of the presented source code is preserved This tool must help the user to write code documentation e g writing comments in programs and it also must help the user to produce scientific articles by allowing code importation and by making i
22. oq It consists of one or several files called scripts whose structure follows the usual one from a programming point of view Declarations statements commands specific to the prover etc are part of the vernacular sentences They form the active part of the script which means they are the only parts of the script that the theorem prover needs to know anything about Any piece of documentation or explanation placed throughout the code can only be placed in the comments fields which are irrelevant i e inactive from the prover s point of view Note that many documentation tools have been developed thus far for programming languages JAVADOC and DOXYGEN among others have made interesting contributions for this purpose However they are much too code centric to be useful in our context The users want to use BTEX for writing documenting and publishing their work since a formal development consists of definitions theorems and proofs rather than pieces of programs Nevertheless a starting point is simply putting TFX commands within comments as part of the scripts On the Theorem Prover Assistant side a MTRX generation facility is of fered by Pvs for displaying formulas and proofs It is based on an easy to use substitution mechanism METAPRL provides low level formatting instructions based on the formatting library of its OCAML implementation language together with POSTSCRIPT and HTML output formats but no BTEX code generati
23. paring it with a spelling checker Inside TEXmacsg the spelling checker is launched the same way as inside EMACS That is the editor selects each word one after the other and sends it to the spelling checker The spelling checker is launched in background As far as spelling is concerned the atomic item that has to be isolated in the buffer is a word meaning a sequence of characters delimited by spaces or punctuation marks depending on the underlying language Assume now the spelling checker is COQ words are to be replaced by vernacular commands But we know how to isolate this kind of item therefore making TEX cg smart enough to send each vernac ular command in the correct order to some COQ process run in background This mode offers a way to certify the underlying formal development in side the editor Obviously the expected behavior cannot be the same as for a spelling checker Wherever an error is encountered this might inhibit the certification mechanism to continue Actually some dependency information between statements and their proofs will prove sufficient to allow to have a partial run of the certification process leaving rejected subtrees pieces of our development marked as requiring further correction 4 6 Interactivity Since the user is working inside an interactive editor it is highly desirable to offer on the fly certification which requires that the editor keeps commu nicating with a Coq process Towards this goal
24. plained before This module proves the validity of e well founded recursion also called course of values e well founded induction from a well founded ordering on a given set Well founded induction principle on Prop Variable A Set Variable R A A Prop The accessibility predicate is defined to be non informative Inductive 4 Acc A gt Prop Acc_intro Vax A Wy A R yx gt Acc y gt Acc a Lemma 5 Acc_inv Var A Acc t gt Vy A R yu gt Acc y the informative elimination let Acc_rec F let rec wf x F x wf in wf Note that Require commands and proofs do not appear although they have been translated and still remain present in the generated document We provide flags that allow one to modify the material presented which comes in handy for full script rendering or to show the mathematical contents of this file Needless to say TEXmacs offers many more options either through the 12 AUDEBAUD RIDEAU existing environment macros or GUILE scripting Following these brief explanations the full COQ Standard Library is gen erated automatically by our documentation tool as a bunch of TREX saqg files which can be browsed within the editor The blue items Acc in lemma 5 represent hyperlinks to the definition declaration Inductive 4 Our con tribution consists in a complete set of TEXmacsg files accessible online from within the editor and browsable in the same way as the web
25. s a stand alone program which processes COQ phrases embedded in IXTRxX files This tool greps the TRX for Coq vernacular commands identified by par ticular YTRX environment tags coq_examples coq_examples coq_eval The result is stored in a temporary script and sent to COQ toplevel coqtop for evaluation Depending on the surrounding tag the command itself or the result are then re inserted in place in the BTFX file As it stands the environ ment tags offered with coq tex gives the user the different possibilities based on two criteria i is the vernacular command to be displayed and ii is the result of its evaluation to be displayed Whenever the answer to a question is positive the appropriate text is printed verbatim at the appropriate place 16 AUDEBAUD RIDEAU Assuming instead we start with a TEXmacsg file we can simulate the same behavior However we can do much more The displayed material is no longer restricted to the raw verbatim format nor the simple combination of two criteria Moreover since the source document is structured there is no need for preparing an intermediate COQ script whenever required the corresponding answers can be directly inserted following the command which has been sent Thus our coq texmacs implements this functionality based on the above exportation tools 4 5 Certification in edition mode In fact we are very close to provide another functionality which we are go ing to explain by com
26. s you to write structured documents via a wysiwyg what you see is what you get and user friendly interface New styles may be created by the user The program implements high quality typesetting algorithms and TEX fonts which help you to produce professionally looking documents We definitively want to offer the user a way to enrich their formal devel opment with convenient documentation or informal explanations Typically after the automated importation step of a COQ script the user will do some interactive editing to prepare for dissemination of results TEX exportation is satisfactory as a scientific document format However we must be able to recover the script to certify a posteriori the embedded code Using XTRX as the generic format for the script leads to a substantial loss of structure information The resulting document is enriched text while on the CoQ side a script is a program where documentation is in comments Therefore the crucial distinction between the active parts of the script the vernacu lar commands mainly and the inactive parts the interleaved comments as documentation fragments is lost in the conversion process if we use ATX as the generic format Although this could be handled to some extent with the help of tricky annotations within the TX end of line based comments this is not satisfactory The TEXmacg editor deals with structured documents which is precisely what we want As far as presentation style is
27. serve links connections corre spondences back and forth between the presentation and the scripts produced and controlled by the prover Automatic translation preserves the visualized code s correctness as long as the user does not modify it Here one can import only fragments of the certified code in the final document But as soon as one needs to modify the 3 AUDEBAUD RIDEAU imported code to assure the correctness means that our tool has to manage the whole development even if only fragments are displayed either to allow an extraction of the development for certification outside of the tool or to allow an interactive certification inside the tool communicating directly with the prover Actually unlike a fragment of programming code that can be consid ered independently of the rest of the code a fragment of formal development can only be certified in the context of the whole development Figure shows the documentation process with the initial importation of the script followed by the documentation steps and finally the extraction into various formats in particular the COQ script extraction allowing another cycle of certification Conversion tool documentation step x TAT EX Postscript HTML gt Coa script Fig 1 Generation of the documentation from a COQ script The Coaseript target is important First for compatibility reasons we must provide a stand alone version of the script where the document
28. t Set nil list A cons A gt list A gt list A Length for such lists Inductive Length A Set list A gt nat gt Prop Lnil Length A nil A 0 Lcons a A 1 list A n nat Length A 1 n gt Length A cons A a 1 S n Depending on the context presentations like a A l list A n Nt Length Aln n a A lilist A n Nt Length Aln On A l list A n NF Length A a l n 1 or length l n i ee length al n 1 when the context is clear enough could be desired without any change in the underlying document These representations raise no technical difficulty Rather they require more decomposition in the Coq structure representation output In XT FX the constructor types for the case of inductive definitions could be prepared along the lines of this example constructor Lcons inferrule a A 1 list A n nat Length A 1 n Length A cons A a 1 S n The section addresses other places where such output questions have to be dealt with on the Coa side 3 Utilization The TMCOQ system consists in several components CoQ which gives us parsing of scripts for free Actually our version is modified to allow for generation of TEXmacg format A set of TEXmacs styles and macros for the rendering The user is free to customize this package the same way as LLNCS class does with respect to the standard TRX article class 10 AUDEBAUD RIDEAU
29. t Prop Acc_intro x A y A R y x gt Acc y gt Acc x Lemma Acc_inv x A Acc x gt y A R y x gt Acc y NewDestruct 1 Trivial Defined the informative elimination let Acc_rec F let rec wf x F x wf in wf 11 AUDEBAUD RIDEAU CoQ comments have the form The documentation fragments are identified by the special comment construction This con struction follows COQDOC almost text conventions which helps in writing structured pieces of text without knowing too much of TeX or HTML syntax and more importantly in a independent syntax way Therefore to keep com patibility with existing documentation fragments in COQDOC style we have added to tmdoc another output format to make these tags understandable by TEX acs This comment is thus translated into texmacs This module proves the validity of lt itemize gt lt item gt well founded recursion also called course of values lt item gt well founded induction lt itemize gt from a well founded ordering on a given set One can see that we have extend the class of comments as documentation by the syntax filter where filter ranges over coqdoc scheme texmacs latex and defaults to coqdoc for compatibility s sake As for translation of the vernacular commands our tool goes far beyond COQDOC capabilities but at the cost of requiring coqtop to perform both parsing and TRX s cg aware structured output as ex
30. t easy to add natural language explanations We want to offer various output formats for example allowing the consulting and browsing of the commented code through a Web interface i e the tool has to manage navigation links in the code and offering all standard output formats used in scientific document publishing TRX HTML POSTSCRIPT etc The tool must provide high quality visualization using notation that is familiar to the reader e g using standard mathematical notation as well as a user friendly interface It also must allow one to present the formal devel opments using a natural syntax and must avoid whenever possible the use of a given theorem prover s scripting language That is the interface should dis play Va nat Va a rather than a nat equal sqrt power a 2 absolu a The user must be able to define his own notation and this no tation must be kept consistent throughout the various parts of the document i e keep the same notation in the explanations as in the imported code fragments Finally to avoid a common source of errors in the translation from the source code to the presentation typos are always unpleasant but are par ticularly annoying in the context of certified developments the tool must allow the automatic importation of the source code for example the theorems statements the definitions etc to preserve their correctness This automatic translation should also make it possible to pre
31. use we can deal with all these features using a single interpretation model The key idea consists in traversing the document according to its structure For each Coq related tag we transform the corresponding subtree according to our specific needs 4 1 A Portable XML Format for External Purposes With respect to the structural shape of TEX g documents it must be noted that TFXmacs does not yet use MATHML standards for file format on disk this is ongoing work by its development team However the XML format has been introduced recently to the set of import export filters and quite independently by us for a particular purpose explained thereafter In the context of the MOWGLI European project there is a need for al lowing annotations and reorganisation of proof fragments in a way that makes the presentation more readable Since the proofs come from CoQ and this feature requires an editor our extension to TEXmacg was a good candidate XML is the dedicated format for documents inside the MOWGLI project together with an intensive use of stylesheets XSLT as transformation lan guage Therefore we have proposed a specific importation exportation filter for XML While we could have decided for a specific set of filters wrt to TM Coq it is better offering a generic way of conversion because such documents should be allowed for edition even outside the editor for instance by means of the edition of stylesheets Therefore we have defi
32. ve definition comes with its name its parameters the resulting type and a finite list of constructors Inductive sum A B Set Set constructors constructor inl arrowc A sum A B constructor inr arrowc B sum A B So it suffices to grab these fields as part of the structure to be able to display the inductive definition in various styles A straightforward representation in TEXmacg would be Inductive 3 sum A B Set Set inl A sum A B inr B sum A B A simple variation closer to mathematical notation could be inl A gt A B The user is free to decide globally or on a local basis among all these repre sentations Even more switching between them is also available within the TEXmacg interface The same result can be obtained in TX from the corresponding source Inductive sum A B sort Set sort Set begin constructors constructor inl arrowc A appc sum A B contructor inr arrowc B appc sum A B 9 AUDEBAUD RIDEAU end constructors with the help of the appropriate macro definitions The more structure COQ is required to produce the more freedom the user gets on their side to get the appropriate notation As an example one might want to present such inductive definition with the help of inference rules In the Coq user manual section 4 5 1 one finds Lists of elements of set A Inductive list A Se

Download Pdf Manuals

image

Related Search

Related Contents

Imetec Acqua WP 120  WFP150 - 堀内電機製作所  Guia do Usuário do Symantec pcAnywhere™  

Copyright © All rights reserved.
DMCA: DMCA_mwitty#outlook.com.