1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Matita V0.5.9 User Manual (rev. 0.5.9 )</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center"><span class="application">Matita</span> V0.5.9
3 User Manual (rev. 0.5.9
4 )</th></tr><tr><td width="20%" align="left"> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr></table><hr /></div><div xml:lang="en" class="book" lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.5.9
5 User Manual (rev. 0.5.9
6 )</h1></div><div><ul xmlns="" class="authorgroup"><li class="author">Andrea Asperti <<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>></li><li class="author">Claudio Sacerdoti Coen <<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>></li><li class="author">Ferruccio Guidi <<a href="mailto:fguidi@cs.unibo.it">fguidi@cs.unibo.it</a>></li><li class="author">Enrico Tassi <<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>></li><li class="author">Stefano Zacchiroli <<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>></li></ul></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="idp64061872"></a><p> Both Matita and this document are free software, you can
7 redistribute them and/or modify them under the terms of the GNU General
8 Public License as published by the Free Software Foundation. See <a class="xref" href="sec_license.html" title="Chapter 10. License">Chapter 10, <em>License</em></a> for more information. </p></div></div><div><div xmlns="" class="revhistory"><span class="revision">Revision: <span class="revnumber">0.5.9
9 </span>, <span class="date">12/07/2006</span></span></div></div></div><hr /></div><div class="toc"><p><strong>Table of Contents</strong></p><dl class="toc"><dt><span class="chapter"><a href="sec_intro.html">1. Introduction</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_intro.html#Features">Features</a></span></dt><dt><span class="sect1"><a href="WrtCoq.html">Matita vs Coq</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_install.html">2. Installation</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_install.html#inst_livecd">Using the LiveCD</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#make_vmachine">Creating the virtual machine</a></span></dt><dt><span class="sect2"><a href="sec_install.html#idp68645040">Sharing files with the real PC</a></span></dt></dl></dd><dt><span class="sect1"><a href="inst_from_src.html">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="inst_from_src.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="inst_from_src.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="inst_from_src.html#database_setup">(optional) MySQL setup</a></span></dt><dt><span class="sect2"><a href="inst_from_src.html#build_instructions">Compiling and installing</a></span></dt></dl></dd><dt><span class="sect1"><a href="matita.conf.xml.html">Configuring Matita</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_gettingstarted.html">3. Getting started</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_gettingstarted.html#unicode">How to type Unicode symbols</a></span></dt><dt><span class="sect1"><a href="cicbrowser.html">Browsing and searching</a></span></dt><dd><dl><dt><span class="sect2"><a href="cicbrowser.html#browsinglib">Browsing the library</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#aboutproof">Looking at a proof under development</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#whelp">Searching the library</a></span></dt></dl></dd><dt><span class="sect1"><a href="authoring.html">Authoring</a></span></dt><dd><dl><dt><span class="sect2"><a href="authoring.html#compilation">How to compile a script</a></span></dt><dt><span class="sect2"><a href="authoring.html#authoringinterface">The authoring interface</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_terms.html">4. Syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_terms.html#terms_and_co">Terms & co.</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_terms.html#lexical">Lexical conventions</a></span></dt><dt><span class="sect2"><a href="sec_terms.html#terms">Terms</a></span></dt></dl></dd><dt><span class="sect1"><a href="axiom_definition_declaration.html">Definitions and declarations</a></span></dt><dd><dl><dt><span class="sect2"><a href="axiom_definition_declaration.html#axiom">axiom</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#definition">definition</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#letrec"><span class="emphasis"><em>TODO</em></span></a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#inductive">(co)inductive types declaration</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#record">record</a></span></dt></dl></dd><dt><span class="sect1"><a href="proofs.html">Proofs</a></span></dt><dd><dl><dt><span class="sect2"><a href="proofs.html#theorem">theorem</a></span></dt><dt><span class="sect2"><a href="proofs.html#variant">variant</a></span></dt><dt><span class="sect2"><a href="proofs.html#lemma">lemma</a></span></dt><dt><span class="sect2"><a href="proofs.html#fact">fact</a></span></dt><dt><span class="sect2"><a href="proofs.html#remark">remark</a></span></dt></dl></dd><dt><span class="sect1"><a href="tacticargs.html">Tactic arguments</a></span></dt><dd><dl><dt><span class="sect2"><a href="tacticargs.html#introsspec">intros-spec</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#pattern">pattern</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#reduction-kind">reduction-kind</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#auto-params">auto-params</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#justification">justification</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_usernotation.html">5. Extending the syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_usernotation.html#idp70046384">notation</a></span></dt><dt><span class="sect1"><a href="ch05s02.html">interpretation</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tacticals.html">6. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#idp70716848">Interactive proofs and definitions</a></span></dt><dt><span class="sect1"><a href="proofstatus.html">The proof status</a></span></dt><dt><span class="sect1"><a href="tacticals.html">Tacticals</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">7. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tactics_quickref">Quick reference card</a></span></dt><dt><span class="sect1"><a href="tac_absurd.html">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_applyS.html">applyS</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_cases.html">cases</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_compose.html">compose</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_demodulate.html">demodulate</a></span></dt><dt><span class="sect1"><a href="tac_destruct.html">destruct</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">fail</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</a></span></dt><dt><span class="sect1"><a href="tac_inversion.html">inversion</a></span></dt><dt><span class="sect1"><a href="tac_lapply.html">lapply</a></span></dt><dt><span class="sect1"><a href="tac_left.html">left</a></span></dt><dt><span class="sect1"><a href="tac_letin.html">letin</a></span></dt><dt><span class="sect1"><a href="tac_normalize.html">normalize</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_subst.html">subst</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_declarative_tactics.html">8. Declarative Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_declarative_tactics.html#declarative_tactics_quickref">Quick reference card</a></span></dt><dt><span class="sect1"><a href="tac_assume.html">assume</a></span></dt><dt><span class="sect1"><a href="tac_byinduction.html">by induction hypothesis we know</a></span></dt><dt><span class="sect1"><a href="tac_case.html">case</a></span></dt><dt><span class="sect1"><a href="tac_bydone.html">done</a></span></dt><dt><span class="sect1"><a href="tac_exitselim.html">let such that</a></span></dt><dt><span class="sect1"><a href="tac_obtain.html">obtain</a></span></dt><dt><span class="sect1"><a href="tac_suppose.html">suppose</a></span></dt><dt><span class="sect1"><a href="tac_thesisbecomes.html">the thesis becomes</a></span></dt><dt><span class="sect1"><a href="tac_weneedtoprove.html">we need to prove</a></span></dt><dt><span class="sect1"><a href="tac_andelim.html">we have</a></span></dt><dt><span class="sect1"><a href="tac_weproceedbycases.html">we proceed by cases on</a></span></dt><dt><span class="sect1"><a href="tac_weproceedbyinduction.html">we proceed by induction on</a></span></dt><dt><span class="sect1"><a href="tac_bytermweproved.html">we proved</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">9. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#command_alias">alias</a></span></dt><dt><span class="sect1"><a href="command_check.html">check</a></span></dt><dt><span class="sect1"><a href="command_eval.html">eval</a></span></dt><dt><span class="sect1"><a href="command_prefer_coercion.html">prefer coercion</a></span></dt><dt><span class="sect1"><a href="command_coercion.html">coercion</a></span></dt><dt><span class="sect1"><a href="command_default.html">default</a></span></dt><dt><span class="sect1"><a href="command_hint.html">hint</a></span></dt><dt><span class="sect1"><a href="command_include.html">include</a></span></dt><dt><span class="sect1"><a href="command_include_first.html">include' "s"</a></span></dt><dt><span class="sect1"><a href="command_whelp.html">whelp</a></span></dt><dt><span class="sect1"><a href="command_qed.html">qed</a></span></dt><dt><span class="sect1"><a href="command_inline.html">inline</a></span></dt><dd><dl><dt><span class="sect2"><a href="command_inline.html#inline-params">inline-params</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_license.html">10. License</a></span></dt></dl></div><div class="list-of-figures"><p><strong>List of Figures</strong></p><dl><dt>2.1. <a href="sec_install.html#idp68630080">The brand new virtual machine</a></dt><dt>2.2. <a href="sec_install.html#idp68633472">Mounting an ISO image</a></dt><dt>2.3. <a href="sec_install.html#idp68637552">Choosing the ISO image</a></dt><dt>2.4. <a href="sec_install.html#idp68641216">Choosing the ISO image</a></dt><dt>2.5. <a href="sec_install.html#idp68647616">Set up a shared folder</a></dt><dt>2.6. <a href="sec_install.html#idp68651136">Choosing the folder to share</a></dt><dt>2.7. <a href="sec_install.html#idp68654928">Naming the shared folder</a></dt><dt>2.8. <a href="sec_install.html#idp68658672">Using it from the virtual machine</a></dt><dt>2.9. <a href="matita.conf.xml.html#idp68778624">Configuring the Databases</a></dt></dl></div><div class="list-of-tables"><p><strong>List of Tables</strong></p><dl><dt>4.1. <a href="sec_terms.html#idp69058128">qstring</a></dt><dt>4.2. <a href="sec_terms.html#idp69064992">id</a></dt><dt>4.3. <a href="sec_terms.html#idp69071584">nat</a></dt><dt>4.4. <a href="sec_terms.html#idp69079568">char</a></dt><dt>4.5. <a href="sec_terms.html#idp69086976">uri-step</a></dt><dt>4.6. <a href="sec_terms.html#idp69095648">uri</a></dt><dt>4.7. <a href="sec_terms.html#idp69112080">csymbol</a></dt><dt>4.8. <a href="sec_terms.html#idp69118752">symbol</a></dt><dt>4.9. <a href="sec_terms.html#tbl_terms">Terms</a></dt><dt>4.10. <a href="sec_terms.html#idp69190544">Simple terms</a></dt><dt>4.11. <a href="sec_terms.html#idp69241744">Arguments</a></dt><dt>4.12. <a href="sec_terms.html#idp69274944">Pattern matching</a></dt><dt>4.13. <a href="tacticargs.html#idp69423248">intros-spec</a></dt><dt>4.14. <a href="tacticargs.html#idp69433952">pattern</a></dt><dt>4.15. <a href="tacticargs.html#idp69453472">path</a></dt><dt>4.16. <a href="tacticargs.html#idp69506592">reduction-kind</a></dt><dt>4.17. <a href="tacticargs.html#idp69522400">auto-params</a></dt><dt>4.18. <a href="tacticargs.html#idp69531952">simple-auto-param</a></dt><dt>4.19. <a href="tacticargs.html#idp69555152">justification</a></dt><dt>5.1. <a href="sec_usernotation.html#idp70117712">usage</a></dt><dt>5.2. <a href="sec_usernotation.html#idp70126480">associativity</a></dt><dt>5.3. <a href="sec_usernotation.html#idp70139344">notation_rhs</a></dt><dt>5.4. <a href="sec_usernotation.html#idp70148064">unparsed_ast</a></dt><dt>5.5. <a href="sec_usernotation.html#idp70166064">enriched_term</a></dt><dt>5.6. <a href="sec_usernotation.html#idp70173616">unparsed_meta</a></dt><dt>5.7. <a href="sec_usernotation.html#idp70190032">level2_meta</a></dt><dt>5.8. <a href="sec_usernotation.html#idp70234960">notation_lhs</a></dt><dt>5.9. <a href="sec_usernotation.html#idp70242480">layout</a></dt><dt>5.10. <a href="sec_usernotation.html#idp70356272">literal</a></dt><dt>5.11. <a href="ch05s02.html#idp70392768">interpretation_argument</a></dt><dt>5.12. <a href="ch05s02.html#idp70401072">interpretation_rhs</a></dt><dt>6.1. <a href="tacticals.html#idp70790512">proof script</a></dt><dt>6.2. <a href="tacticals.html#idp70799712">proof steps</a></dt><dt>6.3. <a href="tacticals.html#idp70846288">tactics and LCF tacticals</a></dt><dt>7.1. <a href="sec_tactics.html#idp71070096">tactics</a></dt><dt>8.1. <a href="sec_declarative_tactics.html#idp73048816">tactics</a></dt><dt>9.1. <a href="command_default.html#idp73808912">clusters</a></dt><dt>9.2. <a href="command_inline.html#idp73947536">inline-params</a></dt><dt>9.3. <a href="command_inline.html#idp73955728">inline-param</a></dt></dl></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top"> </td><td width="20%" align="center"> </td><td width="40%" align="right" valign="top"> Chapter 1. Introduction</td></tr></table></div></body></html>
projects / helm.git / blob