@echo " images # build images for the splash screen"
@echo
+clean:
+
manual: manual-stamp
manual-stamp: $(DOCS_SRC_DIR)/*.xml
$(MAKE) -C $(DOCS_SRC_DIR)/ html
+ test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_SRC_DIR)/
cp $(DOCS_SRC_DIR)/*.html $(DOCS_DEST_DIR)/
touch $@
+.PHONY: images
images: images/matita.xcf
for Y in `seq 0 $(SEQ)`; do \
convert images/matita.png -crop \
rm tmp.png
clean:
+ rm -f manual-stamp
+dist-clean: clean
for X in `seq 0 $(SEQ)`; do\
rm images/bg$$X.png;\
done
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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 vs Coq</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="prev" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="next" href="sec_install.html" title="Chapter 2. Installation" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Matita vs Coq</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 1. Introduction</th><td width="20%" align="right"> <a accesskey="n" href="sec_install.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="WrtCoq"></a>Matita vs Coq</h2></div></div></div><p>
+ The system shares a common look&feel with the Coq proof assistant
+ and its graphical user interface. The two systems have the same logic,
+ very close proof languages and similar sets of tactics. Moreover,
+ Matita is compatible with the library of Coq.
+ From the user point of view the main lacking features
+ with respect to Coq are:
+ </p><div class="itemizedlist"><ul type="disc"><li><p>proof extraction;</p></li><li><p>an extensible language of tactics;</p></li><li><p>automatic implicit arguments;</p></li><li><p>several ad-hoc decision procedures;</p></li><li><p>several rarely used variants for most of the tactics;</p></li><li><p>sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.</p></li></ul></div><p>
+ Still from the user point of view, the main differences with respect
+ to Coq are:
+ </p><div class="itemizedlist"><ul type="disc"><li><p>the language of tacticals that allows execution of partial tactical application;</p></li><li><p>the unification of the concept of metavariable and existential variable;</p></li><li><p>terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;</p></li><li><p>ambiguous terms are disambiguated by direct interaction with the user;</p></li><li><p>theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.</p></li></ul></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_intro.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_intro.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_install.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 1. Introduction </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 2. Installation</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Authoring</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="cicbrowser.html" title="Browsing and searching" /><link rel="next" href="sec_terms.html" title="Chapter 4. Syntax" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Authoring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="authoring"></a>Authoring</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="developments"></a>How to use developments</h3></div></div></div><p>
+ A development is a set of scripts files that are strictly related (i.e.
+ they depend on each other). Matita is able to automatically manage
+ dependencies among the scripts in a development, compiling them in the
+ correct order.
+ </p><p>
+ The include statement can be performed by Matita only if the mentioned
+ script is compiled. If both scripts (the one that includes and the included)
+ are part of the same development, the included script (and recursively all
+ its dependencies) can be compiled automatically. Dependencies among scripts
+ belonging to different developments is not implemented yet.
+ </p><p>
+ The "Developments..." item the File menu (or pressing
+ Ctrl+D) opens the Developments window.
+ </p><div class="figure"><a id="id2520494"></a><p class="title"><b>Figure 3.1. The Developments window</b></p><div class="mediaobject" align="center"><img src="developments.png" align="middle" alt="Screenshot of the Developments window." /></div></div><p>
+ </p><div class="variablelist"><p class="title"><b>Developments window buttons</b></p><dl><dt><span class="term"><code class="filename">New</code></span></dt><dd><p>
+ To create a new Development the user needs to specify a name<sup>[<a id="id2520538" href="#ftn.id2520538">1</a>]</sup>
+ and the root directory in which all scripts will be placed,
+ eventually organized in subdirectories. The Development should be
+ named as the directory in which it lives. A "makefile"
+ file is placed in the specified root directory. That makefile
+ supports the following targets:
+ </p><div class="variablelist"><dl><dt><span class="term"><code class="filename">all</code></span></dt><dd><p>
+ Build the whole development.
+ </p></dd><dt><span class="term"><code class="filename">clean</code></span></dt><dd><p>
+ Cleans the whole development.
+ </p></dd><dt><span class="term"><code class="filename">cleanall</code></span></dt><dd><p>
+ Resets the user environment (i.e. deleting all the results
+ of compilation of every development, including the contents
+ of the database). This target should be used only in case
+ something goes wrong and Matita behaves incorrectly.
+ </p></dd><dt><span class="term"><code class="filename">scriptname.mo</code></span></dt><dd><p>
+ Compiles "scriptname.ma"
+ </p></dd></dl></div><p>
+ </p></dd><dt><span class="term"><code class="filename">Delete</code></span></dt><dd><p>
+ Decompiles the whole development and removes it.
+ </p></dd><dt><span class="term"><code class="filename">Build</code></span></dt><dd><p>
+ Compiles all the scripts in the development.
+ </p></dd><dt><span class="term"><code class="filename">Clean</code></span></dt><dd><p>
+ Decompiles the whole development.
+ </p></dd><dt><span class="term"><code class="filename">Publish</code></span></dt><dd><p>
+ All the user developments live in the "user" space. That is, the
+ result of the compilation of scripts is placed in his home directory
+ and the tuples are placed in personal tables inside the database.
+ Publishing a development means putting it in the "library" space. This
+ means putting the result of compilation in the same place where the
+ standard library lives. This feature will be improved in the future
+ to support publishing the development in the "distributed
+ library" space (making your development public).
+ </p></dd><dt><span class="term"><code class="filename">Close</code></span></dt><dd><p>
+ Closes the Developments window
+ </p></dd></dl></div><p>
+ </p></div><div class="footnotes"><br /><hr width="100" align="left" /><div class="footnote"><p><sup>[<a id="ftn.id2520538" href="#id2520538">1</a>] </sup>
+ The name of the Development should be the name of the directory in
+ which it lives. This is not a requirement, but the makefile
+ automatically generated by matita in the root directory of the
+ development will eventually generate a new Development with a name
+ that follows this convention. Having more than one development for
+ the same set of files is not an issue.
+ </p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Browsing and searching </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 4. Syntax</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Definitions and declarations</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="next" href="proofs.html" title="Proofs" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Definitions and declarations</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="proofs.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="axiom_definition_declaration"></a>Definitions and declarations</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="axiom"></a><span class="bold"><strong>axiom</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></h3></div></div></div><p><strong class="userinput"><code>axiom H: P</code></strong></p><p><span><strong class="command">H</strong></span> is declared as an axiom that states <span><strong class="command">P</strong></span></p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="definition"></a><span class="bold"><strong>definition</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>definition f: T ≝ t</code></strong></p><p><span><strong class="command">f</strong></span> is defined as <span><strong class="command">t</strong></span>;
+ <span><strong class="command">T</strong></span> is its type. An error is raised if the type of
+ <span><strong class="command">t</strong></span> is not convertible to <span><strong class="command">T</strong></span>.</p><p><span><strong class="command">T</strong></span> is inferred from <span><strong class="command">t</strong></span> if
+ omitted.</p><p><span><strong class="command">t</strong></span> can be omitted only if <span><strong class="command">T</strong></span> is
+ given. In this case Matita enters in interactive mode and
+ <span><strong class="command">f</strong></span> must be defined by means of tactics.</p><p>Notice that the command is equivalent to <span><strong class="command">theorem f: T ≝ t</strong></span>.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="inductive"></a>[<span class="bold"><strong>inductive</strong></span>|<span class="bold"><strong>coinductive</strong></span>] <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#args2">args2</a></em></span>]… <span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>≝</strong></span> [<span class="bold"><strong>|</strong></span>] [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>|</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…
+[<span class="bold"><strong>with</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> <span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>≝</strong></span> [<span class="bold"><strong>|</strong></span>] [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>|</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…]…
+</h3></div></div></div><p><strong class="userinput"><code>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</code></strong></p><p>Declares a family of two mutually inductive types
+ <span><strong class="command">i</strong></span> and <span><strong class="command">i'</strong></span> whose types are
+ <span><strong class="command">S</strong></span> and <span><strong class="command">S'</strong></span>, which must be convertible
+ to sorts.</p><p>The constructors <span><strong class="command">ki</strong></span> of type <span><strong class="command">Ti</strong></span>
+ and <span><strong class="command">ki'</strong></span> of type <span><strong class="command">Ti'</strong></span> are also
+ simultaneously declared. The declared types <span><strong class="command">i</strong></span> and
+ <span><strong class="command">i'</strong></span> may occur in the types of the constructors, but
+ only in strongly positive positions according to the rules of the
+ calculus.</p><p>The whole family is parameterized over the arguments <span><strong class="command">x,y,z</strong></span>.</p><p>If the keyword <span><strong class="command">coinductive</strong></span> is used, the declared
+ types are considered mutually coinductive.</p><p>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <span><strong class="command">S</strong></span>. If generated,
+ they are named <span><strong class="command">i_ind</strong></span>, <span><strong class="command">i_rec</strong></span> and
+ <span><strong class="command">i_rect</strong></span> according to the sort of their induction
+ predicate.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="record"></a><span class="bold"><strong>record</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#args2">args2</a></em></span>]… <span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>≝</strong></span><span class="bold"><strong>{</strong></span>[<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="bold"><strong>:</strong></span>|<span class="bold"><strong>:></strong></span>] <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>;</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="bold"><strong>:</strong></span>|<span class="bold"><strong>:></strong></span>] <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…<span class="bold"><strong>}</strong></span></h3></div></div></div><p><strong class="userinput"><code>record id x y z: S ≝ { f1: T1; …; fn:Tn }</code></strong></p><p>Declares a new record family <span><strong class="command">id</strong></span> parameterized over
+ <span><strong class="command">x,y,z</strong></span>.</p><p><span><strong class="command">S</strong></span> is the type of the record
+ and it must be convertible to a sort.</p><p>Each field <span><strong class="command">fi</strong></span> is declared by giving its type
+ <span><strong class="command">Ti</strong></span>. A record without any field is admitted.</p><p>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <span><strong class="command">S</strong></span>. If generated,
+ they are named <span><strong class="command">i_ind</strong></span>, <span><strong class="command">i_rec</strong></span> and
+ <span><strong class="command">i_rect</strong></span> according to the sort of their induction
+ predicate.</p><p>For each field <span><strong class="command">fi</strong></span> a record projection
+ <span><strong class="command">fi</strong></span> is also automatically generated if projection
+ is allowed by the typing rules of the calculus according to the
+ sort <span><strong class="command">S</strong></span>, the type <span><strong class="command">T1</strong></span> and
+ the definability of depending record projections.</p><p>If the type of a field is declared with <span><strong class="command">:></strong></span>,
+ the corresponding record projection becomes an implicit coercion.
+ This is just syntactic sugar and it has the same effect of declaring the
+ record projection as a coercion later on.</p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_terms.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="proofs.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 4. Syntax </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Proofs</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Browsing and searching</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="next" href="authoring.html" title="Authoring" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Browsing and searching</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="cicbrowser"></a>Browsing and searching</h2></div></div></div><p>The CIC browser is used to browse and search the library.
+ You can open a new CIC browser selecting "New Cic Browser"
+ from the "View" menu of Matita, or by pressing "F3".
+ The CIC browser is similar to a traditional Web browser.</p><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="browsinglib"></a>Browsing the library</h3></div></div></div><p>To browse the library, type in the location bar the absolute URI of
+ the theorem, definition or library fragment you are interested in.
+ "cic:/" is the root of the library. Contributions developed
+ in Matita are under "cic:/matita"; all the others are
+ part of the library of Coq.</p><p>Following the hyperlinks it is possible to navigate in the Web
+ of mathematical notions. Proof are rendered in pseudo-natural language
+ and mathematical notation is used for formulae. For now, mathematical
+ notation must be included in the current script to be activated, but we
+ plan to remove this limitation.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="aboutproof"></a>Looking at a proof under development</h3></div></div></div><p>A proof under development is not yet part of the library.
+ The special URI "about:proof" can be used to browse the
+ proof currently under development, if there is one.
+ The "home" button of the CIC browser sets the location bar to
+ "about:proof".
+ </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="whelp"></a>Searching the library</h3></div></div></div><p>The query bar of the CIC browser can be used to search the library
+ of Matita for theorems or definitions that match certain criteria.
+ The criteria is given by typing a term in the query bar and selecting
+ an action in the drop down menu right of it.</p><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="locate"></a>Searching by name</h4></div></div></div><p> <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="hint"></a>List of lemmas that can be applied</h4></div></div></div><p> <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="match"></a>Searching by exact match</h4></div></div></div><p> <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="elim"></a>List of elimination principles for a given type</h4></div></div></div><p> <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="instance"></a>Searching by instantiation</h4></div></div></div><p> <span class="emphasis"><em>TODO</em></span></p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 3. Getting started </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Authoring</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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.1.0
+ Manual (rev. 0)</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center"><span class="application">Matita</span> V0.1.0
+ Manual (rev. 0)</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 class="book" lang="en" xml:lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.1.0
+ Manual (rev. 0)</h1></div><div><div class="authorgroup"><div class="author"><h3 class="author"><span class="firstname">Andrea</span> <span class="surname">Asperti</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Claudio</span> <span class="surname">Sacerdoti Coen</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Enrico</span> <span class="surname">Tassi</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Stefano</span> <span class="surname">Zacchiroli</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>></code> </p></div></div></div></div></div><div><p class="releaseinfo">This manual describes version 0.1.0
+ of Matita.
+ </p></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="id2472240"></a><p> This file is part of HELM, an Hypertextual, Electronic Library of
+ Mathematics, developed at the Computer Science Department, University of
+ Bologna, Italy. </p><p> HELM is free software; you can redistribute it and/or modify it under
+ the terms of the GNU General Public License as published by the Free
+ Software Foundation; either version 2 of the License, or (at your option)
+ any later version. </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT
+ ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+ more details. </p><p> You should have received a copy of the GNU General Public License
+ along with HELM; if not, write to the Free Software Foundation, Inc., 59
+ Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
+ General Public License is available at <a href="ghelp:gpl" target="_top">this link</a>. </p></div></div><div><div class="legalnotice"><a id="id2472567"></a><p class="legalnotice-title"><b>Feedback</b></p><p>To report a bug or make a suggestion regarding the <span class="application">Matita</span>
+ application or this manual, follow the directions in the
+ <a href="http://bugs.mowgli.cs.unibo.it" target="_top">HELM Bug
+ Tracking System Page</a>.
+ </p></div></div><div><div class="revhistory"><table border="1" width="100%" summary="Revision history"><tr><th align="left" valign="top" colspan="3"><b>Revision History</b></th></tr><tr><td align="left">Revision Matita V0.1.0
+ Manual (rev. 0)</td><td align="left">February 2006</td><td> </td></tr><tr><td align="left" colspan="3">
+ <p class="author">The HELM team
+
+ </p>
+
+ </td></tr><tr><td align="left">Revision 0</td><td align="left">4 February 2006</td><td align="left">HELM</td></tr><tr><td align="left" colspan="3">
+ First draft completed.
+ </td></tr></table></div></div></div><hr /></div><div class="toc"><p><b>Table of Contents</b></p><dl><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_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></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#developments">How to use developments</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#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></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#id2526491">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">6. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</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_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_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_discriminate.html">discriminate</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">failt</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_injection.html">injection</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</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_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_tacticals.html">7. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2534769">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">8. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#id2535309">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_license.html">9. License</a></span></dt></dl></div><div class="list-of-figures"><p><b>List of Figures</b></p><dl><dt>3.1. <a href="authoring.html#id2520494">The Developments window</a></dt></dl></div><div class="list-of-tables"><p><b>List of Tables</b></p><dl><dt>2.1. <a href="sec_install.html#id2518871"> <span class="application">configure</span> command line
+ arguments</a></dt><dt>4.1. <a href="sec_terms.html#id2521399">id</a></dt><dt>4.2. <a href="sec_terms.html#id2521488">nat</a></dt><dt>4.3. <a href="sec_terms.html#id2521498">uri</a></dt><dt>4.4. <a href="sec_terms.html#id2521554">Terms</a></dt><dt>4.5. <a href="sec_terms.html#id2522106">Simple terms</a></dt><dt>4.6. <a href="sec_terms.html#id2522561">Arguments</a></dt><dt>4.7. <a href="sec_terms.html#id2522763">Miscellaneous arguments</a></dt><dt>4.8. <a href="sec_terms.html#id2522867">Pattern matching</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>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Proofs</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="axiom_definition_declaration.html" title="Definitions and declarations" /><link rel="next" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Proofs</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="axiom_definition_declaration.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="sec_usernotation.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="proofs"></a>Proofs</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="theorem"></a><span class="bold"><strong>theorem</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>theorem f: P ≝ p</code></strong></p><p>Proves a new theorem <span><strong class="command">f</strong></span> whose thesis is
+ <span><strong class="command">P</strong></span>.</p><p>If <span><strong class="command">p</strong></span> is provided, it must be a proof term for
+ <span><strong class="command">P</strong></span>. Otherwise an interactive proof is started.</p><p><span><strong class="command">P</strong></span> can be omitted only if the proof is not
+ interactive.</p><p>Proving a theorem already proved in the library is an error.
+ To provide an alternative name and proof for the same theorem, use
+ <span><strong class="command">variant f: P ≝ p</strong></span>.</p><p>A warning is raised if the name of the theorem cannot be obtained
+ by mangling the name of the constants in its thesis.</p><p>Notice that the command is equivalent to <span><strong class="command">definition f: T ≝ t</strong></span>.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="variant"></a><span class="bold"><strong>variant</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>variant f: T ≝ t</code></strong></p><p>Same as <span><strong class="command">theorem f: T ≝ t</strong></span>, but it does not
+ complain if the theorem has already been proved. To be used to give
+ an alternative name or proof to a theorem.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="lemma"></a><span class="bold"><strong>lemma</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>lemma f: T ≝ t</code></strong></p><p>Same as <span><strong class="command">theorem f: T ≝ t</strong></span></p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="fact"></a><span class="bold"><strong>fact</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>fact f: T ≝ t</code></strong></p><p>Same as <span><strong class="command">theorem f: T ≝ t</strong></span></p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="remark"></a><span class="bold"><strong>remark</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>remark f: T ≝ t</code></strong></p><p>Same as <span><strong class="command">theorem f: T ≝ t</strong></span></p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="axiom_definition_declaration.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_terms.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_usernotation.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Definitions and declarations </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 5. Extending the syntax</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 8. Other commands</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_tacticals.html" title="Chapter 7. Tacticals" /><link rel="next" href="sec_license.html" title="Chapter 9. License" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 8. Other commands</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tacticals.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_license.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_commands"></a>Chapter 8. Other commands</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_commands.html#id2535309">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2535309"></a>Introduction</h2></div></div></div><p>
+ <span class="emphasis"><em>TODO</em></span>
+ </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_tacticals.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_license.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 7. Tacticals </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 9. License</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 3. Getting started</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_install.html" title="Chapter 2. Installation" /><link rel="next" href="cicbrowser.html" title="Browsing and searching" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 3. Getting started</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="cicbrowser.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_gettingstarted"></a>Chapter 3. Getting started</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><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#developments">How to use developments</a></span></dt></dl></dd></dl></div><p> If you are already familiar with the Calculus of (co)Inductive
+ Constructions (CIC) and with interactive theorem provers with procedural
+ proof languages (expecially Coq), getting started with Matita is relatively
+ easy. You just need to learn how to type Unicode symbols, how to browse
+ and search the library and how to author a proof script.</p><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="unicode"></a>How to type Unicode symbols</h2></div></div></div><p>Unicode characters can be typed in several ways:</p><div class="itemizedlist"><ul type="disc"><li><p>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</p></li><li><p>Typing the ligature "\name" where "name"
+ is a standard Unicode or LaTeX name for the character. Pressing
+ "Alt+L" just after the last character of the name converts
+ the ligature to the Unicode symbol. This operation is
+ not required since Matita understands also the "\name"
+ sequences. E.g. "\Omega" followed by Alt+L generates
+ "Ω".</p></li><li><p>Typing one of the following ligatures (and optionally
+ converting the ligature to the Unicode character has described before):
+ ":=" (which stands for ≝); "->" (which stands for
+ "→"); "=>" (which stands for "⇒").</p></li></ul></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="cicbrowser.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 2. Installation </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Browsing and searching</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 2. Installation</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="WrtCoq.html" title="Matita vs Coq" /><link rel="next" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 2. Installation</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_install"></a>Chapter 2. Installation</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_install.html#inst_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="inst_from_src"></a>Installing from sources</h2></div></div></div><p>Currently, the only intended way to install Matita is starting
+ from its source code. </p><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="get_source_code"></a>Getting the source code</h3></div></div></div><p>You can get the Matita source code in two ways:
+ </p><div class="orderedlist"><ol type="1"><li><p> go to the <a href="http://matita.cs.unibo.it/download.shtml" target="_top">download
+ page</a> and get the <a href="http://matita.cs.unibo.it/sources/matita-latest.tar.gz" target="_top">latest released source tarball</a>;</p></li><li><p> get the development sources from <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0" target="_top">our
+ SVN repository</a>. You will need the
+ <span class="application">components/</span> and
+ <span class="application">matita/</span> directories from the
+ <code class="filename">trunk/helm/software/</code> directory, plus the
+ <code class="filename">configure</code> and <code class="filename">Makefile*</code>
+ stuff from the same directory. </p><p>In this case you will need to run
+ <span><strong class="command">autoconf</strong></span> before proceding with the building
+ instructions below.</p></li></ol></div><p>
+ </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="build_requirements"></a>Requirements</h3></div></div></div><p>In order to build Matita from sources you will need some
+ tools and libraries. They are listed below.
+
+ </p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note for Debian users</h3><p>If you are running a <a href="http://www.debian.org" target="_top">Debian GNU/Linux</a> distribution
+ you can have APT install all the required tools and libraries by
+ adding the following repository to your
+ <code class="filename">/etc/apt/sources.list</code>: </p><pre class="programlisting">
+ deb <a href="http://people.debian.org/~zack" target="_top">http://people.debian.org/~zack</a> unstable helm
+ </pre><p> and installing the
+ <span class="application">helm-matita-deps</span> package.</p></div><p>
+
+ </p><div class="variablelist"><p class="title"><b>Required tools and libraries</b></p><dl><dt><span class="term">
+ <span class="application"> <a href="http://caml.inria.fr" target="_top">OCaml</a> </span>
+ </span></dt><dd><p> the Objective Caml compiler, version 3.09 or above </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://www.ocaml-programming.de/packages/" target="_top">Findlib</a>
+ </span>
+ </span></dt><dd><p> OCaml package manager, version 1.1.1 or above</p></dd><dt><span class="term">
+ <span class="application"> <a href="http://www.xs4all.nl/~mmzeeman/ocaml/" target="_top">OCaml
+ Expat</a> </span>
+ </span></dt><dd><p>OCaml bindings for the <span class="application"><a href="http://expat.sourceforge.net/" target="_top">expat</a>
+ library</span> </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://gmetadom.sourceforge.net/" target="_top">GMetaDOM</a>
+ </span>
+ </span></dt><dd><p>OCaml bindings for the <span class="application"><a href="http://gdome2.cs.unibo.it/" target="_top">Gdome 2</a>
+ library</span></p></dd><dt><span class="term">
+ <span class="application"> <a href="http://www.bononia.it/~zack/ocaml-http.en.html" target="_top">OCaml
+ HTTP</a> </span>
+ </span></dt><dd><p> OCaml library to write HTTP daemons (and clients) </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html" target="_top">LablGTK</a>
+ </span>
+ </span></dt><dd><p> OCaml bindings for the <span class="application"> <a href="http://www.gtk.org" target="_top"> GTK+</a> library
+ </span>, version 2.6.0 or above </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://helm.cs.unibo.it/mml-widget/" target="_top">GtkMathView</a>
+ </span>
+ , </span><span class="term">
+ <span class="application"> <a href="http://helm.cs.unibo.it/mml-widget/" target="_top">LablGtkMathView</a>
+ </span>
+ </span></dt><dd><p> GTK+ widget to render <a href="http://www.w3.org/Math/" target="_top">MathML</a> documents and its
+ OCaml bindings </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://gtksourceview.sourceforge.net/" target="_top">GtkSourceView</a>
+ </span>
+ , </span><span class="term">
+ <span class="application"> <a href="http://helm.cs.unibo.it/software/lablgtksourceview/" target="_top">LablGtkSourceView</a>
+ </span>
+ </span></dt><dd><p> extension for the GTK+ text widget (adding the typical
+ features of source code editors) and its OCaml bindings </p></dd><dt><span class="term"> <span class="application"> <a href="http://www.mysql.com" target="_top">MySQL</a> </span> , </span><span class="term">
+ <span class="application"> <a href="http://raevnos.pennmush.org/code/ocaml-mysql/" target="_top">OCaml
+ MySQL</a> </span>
+ </span></dt><dd><p> SQL database and OCaml bindings for its client-side library
+ </p><p> The SQL database itself is not strictly needed to run
+ Matita, but we stronly encourage its use since a lot of
+ features are disabled without it. Still, the OCaml bindings of
+ the library are needed at compile time.</p></dd><dt><span class="term">
+ <span class="application"> <a href="http://ocamlnet.sourceforge.net/" target="_top">Ocamlnet</a>
+ </span>
+ </span></dt><dd><p> collection of OCaml libraries to deal with
+ application-level Internet protocols and conventions </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://www.cduce.org/download.html" target="_top">ulex</a>
+ </span>
+ </span></dt><dd><p> Unicode lexer generator for OCaml </p></dd><dt><span class="term">
+ <span class="application"> <a href="http://cristal.inria.fr/~xleroy/software.html" target="_top">CamlZip</a>
+ </span>
+ </span></dt><dd><p> OCaml library to access <code class="filename">.gz</code> files
+ </p></dd></dl></div><p> </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="database_setup"></a>Database setup</h3></div></div></div><p> To fully exploit Matita indexing and search capabilities you
+ will need a working <span class="application"> <a href="http://www.mysql.com" target="_top">MySQL</a> </span> database. Detalied instructions on how to do
+ it can be found in the <a href="http://dev.mysql.com/doc/" target="_top">MySQL documentation</a>. Here you
+ can find a quick howto. </p><p> In order to create a database you need administrator permissions on
+ your MySQL installation, usually the root account has them. Once you
+ have the permissions, a new database can be created executing
+ <strong class="userinput"><code>mysqladmin create matita</code></strong>
+ (<span class="emphasis"><em>matita</em></span> is the default database name, you can
+ change it using the <em class="parameter"><code>db.user</code></em> key of the
+ configuration file). </p><p> Then you need to grant the necessary access permissions to the
+ database user of Matita, typing <strong class="userinput"><code>echo "grant all privileges
+ on matita.* to helm;" | mysql matita</code></strong> should do the trick
+ (<span class="emphasis"><em>helm</em></span> is the default user name used by Matita to
+ access the database, you can change it using the
+ <em class="parameter"><code>db.user</code></em> key of the configuration file).
+ </p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note</h3><p> This way you create a database named <span class="emphasis"><em>matita</em></span>
+ on which anyone claiming to be the <span class="emphasis"><em>helm</em></span> user can
+ do everything (like adding dummy data or destroying the contained
+ one). It is strongly suggested to apply more fine grained permissions,
+ how to do it is out of the scope of this manual.</p></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="build_instructions"></a>Compiling and installing</h3></div></div></div><p> Once you get the source code the installations steps should be
+ quite familiar.</p><p> First of all you need to configure the build process executing
+ <strong class="userinput"><code>./configure</code></strong>. This will check that all needed
+ tools and library are installed and prepare the sources for compilation
+ and installation. </p><p> Quite a few (optional) arguments may be passed to the
+ <span class="application">configure</span> command line to change build time
+ parameters. They are listed in the table below, together with their
+ default values.
+
+ </p><div class="table"><a id="id2518871"></a><p class="title"><b>Table 2.1. <span class="application">configure</span> command line
+ arguments</b></p><table summary=" configure command line 	 arguments" border="1"><colgroup><col /><col /><col /></colgroup><thead><tr><th align="center">Argument</th><th align="center">Default</th><th align="center">Description</th></tr></thead><tbody><tr><td align="left">
+ <strong class="userinput"><code>--with-runtime-dir=<em class="replaceable"><code>dir</code></em></code></strong>
+ </td><td align="left"> <code class="filename">/usr/local/matita/</code> </td><td align="left"> <p> Runtime base directory where all Matita stuff
+ (executables, configuration files, standard
+ library, ...) will be installed </p> </td></tr><tr><td align="left">
+ <strong class="userinput"><code>--with-dbhost=<em class="replaceable"><code>host</code></em></code></strong>
+ </td><td align="left"> localhost </td><td align="left"> <p>Default SQL server hostname. Will be used while
+ building the standard library during the installation and to
+ create the default Matita configuration. May be changed
+ later in configuration file.</p></td></tr><tr><td align="left"> <strong class="userinput"><code>--enable-debug</code></strong></td><td align="left"> disabled </td><td align="left"> <p> Enable debugging code. Not for the casual user.
+ </p> </td></tr></tbody></table></div><p>
+
+ </p><p> Then you will manage the build and install process using
+ <span class="application"><a href="http://www.gnu.org/software/make/" target="_top">make</a></span>
+ as usual. Below are reported the targets you have to invoke in sequence
+ to build and install.
+
+ </p><div class="variablelist"><p class="title"><b><span class="application">make</span> targets</b></p><dl><dt><span class="term"><strong class="userinput"><code>world</code></strong></span></dt><dd><p>builds components needed by Matita and Matita itself
+ (in bytecode or native code depending
+ on the availability of the OCaml native code compiler) </p></dd><dt><span class="term"><strong class="userinput"><code>install</code></strong></span></dt><dd><p>installs Matita related tools, standard library and the
+ needed runtime stuff in the proper places on the filesystem.
+ </p><p>As a part of the installation process the Matita
+ standard library will be compiled, thus testing that the just
+ built <span class="application">matitac</span> compiler works
+ properly.</p><p>For this step you will need a working SQL database (for
+ indexing the standard library while you are compiling it). See
+ <a href="#database_setup" target="_top">Database setup</a>
+ for instructions on how to set it up.
+ </p></dd></dl></div><p>
+
+ </p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Matita vs Coq </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 3. Getting started</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 1. Introduction</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="next" href="WrtCoq.html" title="Matita vs Coq" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 1. Introduction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="index.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="WrtCoq.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_intro"></a>Chapter 1. Introduction</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><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></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="Features"></a>Features</h2></div></div></div><p><span class="application">Matita</span> is an interactive theorem prover
+ (or proof assistant) with the following characteristics:</p><div class="itemizedlist"><ul type="disc"><li><p>It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</p></li><li><p>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</p></li><li><p>It has a stand-alone graphical user interface (GUI) inspired by
+CtCoq/Proof General. The GUI is implemented according to the state
+of the art. In particular:</p><div class="itemizedlist"><ul type="circle"><li><p>It is based and fully integrated with Gtk/Gnome.</p></li><li><p>An on-line help can be browsed via the Gnome documentation browser.</p></li><li><p>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</p></li></ul></div></li><li><p>It integrates advanced browsing and searching procedures.</p></li><li><p>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</p></li><li><p>It is compatible with the library of Coq (definitions and proof objects).</p></li></ul></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="index.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="WrtCoq.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top"><span class="application">Matita</span> V0.1.0
+ Manual (rev. 0) </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Matita vs Coq</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 9. License</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_commands.html" title="Chapter 8. Other commands" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 9. License</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> </td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_license"></a>Chapter 9. License</h2></div></div></div><p> This file is part of HELM, an Hypertextual, Electronic Library of
+ Mathematics, developed at the Computer Science Department, University of
+ Bologna, Italy. </p><p> HELM is free software; you can redistribute it and/or modify it under
+ the terms of the GNU General Public License as published by the Free
+ Software Foundation; either version 2 of the License, or (at your option)
+ any later version. </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT
+ ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+ more details. </p><p> You should have received a copy of the GNU General Public License
+ along with HELM; if not, write to the Free Software Foundation, Inc., 59
+ Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
+ General Public License is available at <a href="ghelp:gpl" target="_top">this link</a>. </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> </td></tr><tr><td width="40%" align="left" valign="top">Chapter 8. Other commands </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> </td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 7. Tacticals</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="tac_whd.html" title="whd <pattern>" /><link rel="next" href="sec_commands.html" title="Chapter 8. Other commands" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 7. Tacticals</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_whd.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_commands.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_tacticals"></a>Chapter 7. Tacticals</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2534769">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2534769"></a>Introduction</h2></div></div></div><p>
+ <span class="emphasis"><em>TODO</em></span>
+ </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_whd.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_commands.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">whd <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 8. Other commands</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 6. Tactics</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /><link rel="next" href="tac_apply.html" title="apply sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 6. Tactics</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="tac_apply.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_tactics"></a>Chapter 6. Tactics</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</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_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_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_discriminate.html">discriminate</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">failt</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_injection.html">injection</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</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_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></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_absurd"></a>absurd <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>absurd P</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by eliminating an
+ absurd term.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents of conclusion <span><strong class="command">P</strong></span>
+ and <span><strong class="command">¬P</strong></span>.</p></dd></dl></div><p>
+ </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="tac_apply.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 5. Extending the syntax </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> apply sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 4. Syntax</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="authoring.html" title="Authoring" /><link rel="next" href="axiom_definition_declaration.html" title="Definitions and declarations" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 4. Syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="authoring.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="axiom_definition_declaration.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_terms"></a>Chapter 4. Syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><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#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></dl></div><p>To describe syntax in this manual we use the following conventions:</p><div class="orderedlist"><ol type="1"><li><p>Non terminal symbols are emphasized and have a link to their
+ definition. E.g.: <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></p></li><li><p>Terminal symbols are in bold. E.g.:
+ <span class="bold"><strong>theorem</strong></span></p></li><li><p>Optional sequences of elements are put in square brackets.
+ E.g.: [<span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</p></li><li><p>Alternatives are put in square brakets and they are
+ separated by vertical bars. E.g.: [<span class="bold"><strong><</strong></span>|<span class="bold"><strong>></strong></span>]</p></li><li><p>Repetition of sequences of elements are given by putting the
+ first sequence in square brackets, that are followed by three dots.
+ E.g.: [<span class="bold"><strong>and</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…</p></li></ol></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="terms_and_co"></a>Terms & co.</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="lexical"></a>Lexical conventions</h3></div></div></div><p>
+ </p><div class="table"><a id="id2521399"></a><p class="title"><b>Table 4.1. id</b></p><table summary="id" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="id"></a><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id2521488"></a><p class="title"><b>Table 4.2. nat</b></p><table summary="nat" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="nat"></a><span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id2521498"></a><p class="title"><b>Table 4.3. uri</b></p><table summary="uri" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="uri"></a><span class="emphasis"><em><a href="sec_terms.html#uri">uri</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="terms"></a>Terms</h3></div></div></div><p>
+ </p><div class="table"><a id="id2521554"></a><p class="title"><b>Table 4.4. Terms</b></p><table summary="Terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="term"></a><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>simple or delimited term</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>application</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>λ</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>λ-abstraction</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Π</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a datatype</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>∀</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a proposition</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>→</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>non-dependent product (logical implication or function space)</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|(<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>)] <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>local definition</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span>
+ [<span class="bold"><strong>co</strong></span>]<span class="bold"><strong>rec</strong></span>
+ <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|<span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]… <span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span>]… [<span class="bold"><strong>on</strong></span> <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>]
+ [<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]
+ <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ </td><td>(co)recursive definitions</td></tr><tr><td> </td><td> </td><td>
+ [<span class="bold"><strong>and</strong></span>
+ [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|<span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]… <span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span>]… [<span class="bold"><strong>on</strong></span> <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>]
+ [<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]
+ <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…
+ </td><td> </td></tr><tr><td> </td><td> </td><td>
+ <span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ </td><td> </td></tr><tr><td> </td><td>|</td><td>…</td><td>user provided notation</td></tr></tbody></table></div><p>
+
+ </p><div class="table"><a id="id2522106"></a><p class="title"><b>Table 4.5. Simple terms</b></p><table summary="Simple terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="sterm"></a><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>::=</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>\subst[</strong></span>
+ <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>≔</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ [<span class="bold"><strong>;</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>≔</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…
+ <span class="bold"><strong>]</strong></span>]
+ </td><td>identifier with optional explicit named substitution</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#uri">uri</a></em></span></td><td>a qualified reference</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Prop</strong></span></td><td>the impredicative sort of propositions</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Set</strong></span></td><td>the impredicate sort of datatypes</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Type</strong></span></td><td>one predicative sort of datatypes</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>?</strong></span></td><td>implicit argument</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>?n</strong></span>
+ [<span class="bold"><strong>[</strong></span>
+ [<span class="bold"><strong>_</strong></span>|<span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…
+ <span class="bold"><strong>]</strong></span>]</td><td>metavariable</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>match</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ [ <span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> ]
+ [ <span class="bold"><strong>return</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> ]
+ <span class="bold"><strong>with</strong></span>
+ </td><td>case analysis</td></tr><tr><td> </td><td> </td><td>
+ <span class="bold"><strong>[</strong></span>
+ <span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span> <span class="bold"><strong> ⇒ </strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ [
+ <span class="bold"><strong>|</strong></span>
+ <span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span> <span class="bold"><strong> ⇒ </strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
+ ]…<span class="bold"><strong>]</strong></span> </td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td>cast</td></tr><tr><td> </td><td>|</td><td>…</td><td>user provided notation at precedence 90</td></tr></tbody></table></div><p>
+
+ </p><div class="table"><a id="id2522561"></a><p class="title"><b>Table 4.6. Arguments</b></p><table summary="Arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args"></a><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span></td><td>::=</td><td>
+ <span class="bold"><strong>_</strong></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]
+ </td><td>ignored argument</td></tr><tr><td> </td><td>|</td><td>
+ <span class="bold"><strong>(</strong></span><span class="bold"><strong>_</strong></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]<span class="bold"><strong>)</strong></span>
+ </td><td>ignored argument</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]<span class="bold"><strong>)</strong></span></td><td> </td></tr></tbody></table></div><p>
+
+ </p><div class="table"><a id="id2522763"></a><p class="title"><b>Table 4.7. Miscellaneous arguments</b></p><table summary="Miscellaneous arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args2"></a><span class="emphasis"><em><a href="sec_terms.html#args2">args2</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr></tbody></table></div><p>
+
+ </p><div class="table"><a id="id2522867"></a><p class="title"><b>Table 4.8. Pattern matching</b></p><table summary="Pattern matching" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="match_pattern"></a><span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>0-ary constructor</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>)</strong></span></td><td>n-ary constructor (binds the n arguments)</td></tr></tbody></table></div><p>
+ </p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="authoring.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="axiom_definition_declaration.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Authoring </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Definitions and declarations</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>Chapter 5. Extending the syntax</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="proofs.html" title="Proofs" /><link rel="next" href="sec_tactics.html" title="Chapter 6. Tactics" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 5. Extending the syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_tactics.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_usernotation"></a>Chapter 5. Extending the syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_usernotation.html#id2526491">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2526491"></a>Introduction</h2></div></div></div><p>
+ <span class="emphasis"><em>TODO</em></span>
+ </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_tactics.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Proofs </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 6. Tactics</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>apply sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="next" href="tac_assumption.html" title="assumption" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">apply sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tactics.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_assumption.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_apply"></a>apply <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>apply t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">t</strong></span> must have type
+ <span><strong class="command">T<sub>1</sub> → ... →
+ T<sub>n</sub> → G</strong></span>
+ where <span><strong class="command">G</strong></span> can be unified with the conclusion
+ of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying <span><strong class="command">t</strong></span> to <span><strong class="command">n</strong></span> implicit arguments (that become new sequents).</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise
+ <span><strong class="command">T<sub>i</sub></strong></span> that is not
+ instantiated by unification. <span><strong class="command">T<sub>i</sub></strong></span> is
+ the conclusion of the <span><strong class="command">i</strong></span>-th new sequent to
+ prove.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_tactics.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_assumption.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 6. Tactics </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> assumption</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>assumption</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_apply.html" title="apply sterm" /><link rel="next" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">assumption</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_apply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_auto.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_assumption"></a>assumption</h2></div></div></div><p><strong class="userinput"><code>assumption </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>There must exist an hypothesis whose type can be unified with
+ the conclusion of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent exploiting an hypothesis.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_apply.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_auto.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">apply sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> auto [depth=nat] [width=nat] [paramodulation] [full]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>auto [depth=nat] [width=nat] [paramodulation] [full]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_assumption.html" title="assumption" /><link rel="next" href="tac_clear.html" title="clear id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">auto [depth=nat] [width=nat] [paramodulation] [full]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_assumption.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clear.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_auto"></a>auto [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [width=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [paramodulation] [full]</h2></div></div></div><p><strong class="userinput"><code>auto depth=d width=w paramodulation full</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None, but the tactic may fail finding a proof if every
+ proof is in the search space that is pruned away. Pruning is
+ controlled by <span><strong class="command">d</strong></span> and <span><strong class="command">w</strong></span>.
+ Moreover, only lemmas whose type signature is a subset of the
+ signature of the current sequent are considered. The signature of
+ a sequent is ...TODO</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by repeated application of
+ rewriting steps (unless <span><strong class="command">paramodulation</strong></span> is
+ omitted), hypothesis and lemmas in the library.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_assumption.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_clear.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">assumption </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> clear id</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>change <pattern> with sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clearbody.html" title="clearbody id" /><link rel="next" href="tac_constructor.html" title="constructor nat" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">change <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clearbody.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_constructor.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_change"></a>change <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>Each subterm matched by the pattern must be convertible
+ with the term <span><strong class="command">t</strong></span> disambiguated in the context
+ of the matched subterm.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces the subterms of the current sequent matched by
+ <span><strong class="command">patt</strong></span> with the new term <span><strong class="command">t</strong></span>.
+ For each subterm matched by the pattern, <span><strong class="command">t</strong></span> is
+ disambiguated in the context of the subterm.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_clearbody.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_constructor.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">clearbody id </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> constructor nat</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>clear id</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /><link rel="next" href="tac_clearbody.html" title="clearbody id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">clear id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_auto.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clearbody.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_clear"></a>clear <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clear H</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">H</strong></span> must be an hypothesis of the
+ current sequent to prove.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It hides the hypothesis <span><strong class="command">H</strong></span> from the
+ current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_auto.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_clearbody.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">auto [depth=nat] [width=nat] [paramodulation] [full] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> clearbody id</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>clearbody id</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clear.html" title="clear id" /><link rel="next" href="tac_change.html" title="change <pattern> with sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">clearbody id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clear.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_change.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_clearbody"></a>clearbody <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clearbody H</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">H</strong></span> must be an hypothesis of the
+ current sequent to prove.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It hides the definiens of a definition in the current
+ sequent context. Thus the definition becomes an hypothesis.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_clear.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_change.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">clear id </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> change <pattern> with sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>constructor nat</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_change.html" title="change <pattern> with sterm" /><link rel="next" href="tac_contradiction.html" title="contradiction" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">constructor nat</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_change.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_contradiction.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_constructor"></a>constructor <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></h2></div></div></div><p><strong class="userinput"><code>constructor n</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least <span><strong class="command">n</strong></span> constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the <span><strong class="command">n</strong></span>-th constructor of the
+ inductive type of the conclusion of the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the constructor
+ that can not be inferred by unification. For more details,
+ see the <span><strong class="command">apply</strong></span> tactic.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_change.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_contradiction.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">change <pattern> with sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> contradiction</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>contradiction</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_constructor.html" title="constructor nat" /><link rel="next" href="tac_cut.html" title="cut sterm [as id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">contradiction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_constructor.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_cut.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_contradiction"></a>contradiction</h2></div></div></div><p><strong class="userinput"><code>contradiction </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>There must be in the current context an hypothesis of type
+ <span><strong class="command">False</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying an hypothesis of
+ type <span><strong class="command">False</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_constructor.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_cut.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">constructor nat </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> cut sterm [as id]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>cut sterm [as id]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_contradiction.html" title="contradiction" /><link rel="next" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">cut sterm [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_contradiction.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_decompose.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_cut"></a>cut <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>cut P as H</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents. The first one has an extra
+ hypothesis <span><strong class="command">H:P</strong></span>. If <span><strong class="command">H</strong></span> is
+ omitted, the name of the hypothesis is automatically generated.
+ The second sequent has conclusion <span><strong class="command">P</strong></span> and
+ hypotheses the hypotheses of the current sequent to prove.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_contradiction.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_decompose.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">contradiction </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> decompose id [id]… [<intros_spec>]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>decompose id [id]… [<intros_spec>]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_cut.html" title="cut sterm [as id]" /><link rel="next" href="tac_discriminate.html" title="discriminate sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">decompose id [id]… [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_cut.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_discriminate.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_decompose"></a>decompose <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]… [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>decompose ???</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_cut.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_discriminate.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">cut sterm [as id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> discriminate sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>discriminate sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /><link rel="next" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">discriminate sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_decompose.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elim.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_discriminate"></a>discriminate <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>discriminate p</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must have type <span><strong class="command">K t<sub>1</sub> ... t<sub>n</sub> = K' t'<sub>1</sub> ... t'<sub>m</sub></strong></span> where <span><strong class="command">K</strong></span> and <span><strong class="command">K'</strong></span> must be different constructors of the same inductive type and each argument list can be empty if
+its constructor takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by proving the absurdity of
+ <span><strong class="command">p</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_decompose.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_elim.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">decompose id [id]… [<intros_spec>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> elim sterm [using sterm] [<intros_spec>]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>elim sterm [using sterm] [<intros_spec>]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_discriminate.html" title="discriminate sterm" /><link rel="next" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">elim sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_discriminate.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elimType.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_elim"></a>elim <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elim t using th hyps</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">t</strong></span> must inhabit an inductive type and
+ <span><strong class="command">th</strong></span> must be an elimination principle for that
+ inductive type. If <span><strong class="command">th</strong></span> is omitted the appropriate
+ standard elimination principle is chosen.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on the values of <span><strong class="command">t</strong></span>,
+ according to the elimination principle <span><strong class="command">th</strong></span>.
+ </p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens one new sequent for each case. The names of
+ the new hypotheses are picked by <span><strong class="command">hyps</strong></span>, if
+ provided. If hyps specifies also a number of hypotheses that
+ is less than the number of new hypotheses for a new sequent,
+ then the exceeding hypothesis will be kept as implications in
+ the conclusion of the sequent.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_discriminate.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_elimType.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">discriminate sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> elimType sterm [using sterm] [<intros_spec>]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>elimType sterm [using sterm] [<intros_spec>]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exact.html" title="exact sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">elimType sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elim.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exact.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_elimType"></a>elimType <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elimType T using th hyps</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">T</strong></span> must be an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO (severely bugged now).</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_elim.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_exact.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">elim sterm [using sterm] [<intros_spec>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> exact sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>exact sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exists.html" title="exists" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">exact sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elimType.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exists.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_exact"></a>exact <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>exact p</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of <span><strong class="command">p</strong></span> must be convertible
+ with the conclusion of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent using <span><strong class="command">p</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_elimType.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_exists.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">elimType sterm [using sterm] [<intros_spec>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> exists</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>exists</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exact.html" title="exact sterm" /><link rel="next" href="tac_fail.html" title="fail " /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">exists</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exact.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fail.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_exists"></a>exists</h2></div></div></div><p><strong class="userinput"><code>exists </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <span><strong class="command">constructor</strong></span> tactic.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_exact.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_fail.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">exact sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> fail </td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>fail </title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exists.html" title="exists" /><link rel="next" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fail </th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exists.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fold.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_fail"></a>fail </h2></div></div></div><p><strong class="userinput"><code>fail</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>This tactic always fail.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>N.A.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_exists.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_fold.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">exists </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> fold <reduction_kind> sterm <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>fold <reduction_kind> sterm <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fail.html" title="fail " /><link rel="next" href="tac_fourier.html" title="fourier" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fold <reduction_kind> sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fail.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fourier.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_fold"></a>fold <reduction_kind> <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>fold red t patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The pattern must not specify the wanted term.</p></dd><dt><span class="term">Action:</span></dt><dd><p>First of all it locates all the subterms matched by
+ <span><strong class="command">patt</strong></span>. In the context of each matched subterm
+ it disambiguates the term <span><strong class="command">t</strong></span> and reduces it
+ to its <span><strong class="command">red</strong></span> normal form; then it replaces with
+ <span><strong class="command">t</strong></span> every occurrence of the normal form in the
+ matched subterm.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_fail.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_fourier.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">fail </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> fourier</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>fourier</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /><link rel="next" href="tac_fwd.html" title="fwd id [<ident list>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fourier</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fwd.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_fourier"></a>fourier</h2></div></div></div><p><strong class="userinput"><code>fourier </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be a linear
+ inequation over real numbers taken from standard library of
+ Coq. Moreover the inequations in the hypotheses must imply the
+ inequation in the conclusion of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying the Fourier method.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_fold.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_fwd.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">fold <reduction_kind> sterm <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> fwd id [<ident list>]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>fwd id [<ident list>]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fourier.html" title="fourier" /><link rel="next" href="tac_generalize.html" title="generalize <pattern> [as id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fwd id [<ident list>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fourier.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_generalize.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_fwd"></a>fwd <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<ident list>]</h2></div></div></div><p><strong class="userinput"><code>fwd ...TODO</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_fourier.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_generalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">fourier </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> generalize <pattern> [as id]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>generalize <pattern> [as id]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fwd.html" title="fwd id [<ident list>]" /><link rel="next" href="tac_id.html" title="id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">generalize <pattern> [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fwd.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_id.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_generalize"></a>generalize <pattern> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>generalize patt as H</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>All the terms matched by <span><strong class="command">patt</strong></span> must be
+ convertible and close in the context of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying a stronger
+ lemma that is proved using the new generated sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent where the current sequent conclusion
+ <span><strong class="command">G</strong></span> is generalized to
+ <span><strong class="command">∀x.G{x/t}</strong></span> where <span><strong class="command">{x/t}</strong></span>
+ is a notation for the replacement with <span><strong class="command">x</strong></span> of all
+ the occurrences of the term <span><strong class="command">t</strong></span> matched by
+ <span><strong class="command">patt</strong></span>. If <span><strong class="command">patt</strong></span> matches no
+ subterm then <span><strong class="command">t</strong></span> is defined as the
+ <span><strong class="command">wanted</strong></span> part of the pattern.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_fwd.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_id.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">fwd id [<ident list>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> id</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>id</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_generalize.html" title="generalize <pattern> [as id]" /><link rel="next" href="tac_injection.html" title="injection sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_injection.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_id"></a>id</h2></div></div></div><p><strong class="userinput"><code>id </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>This identity tactic does nothing without failing.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_injection.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">generalize <pattern> [as id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> injection sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>injection sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_id.html" title="id" /><link rel="next" href="tac_intro.html" title="intro [id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">injection sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_id.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intro.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_injection"></a>injection <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>injection p</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must have type <span><strong class="command">K t<sub>1</sub> ... t<sub>n</sub> = K t'<sub>1</sub> ... t'<sub>n</sub></strong></span> where both argument lists are empty if
+<span><strong class="command">K</strong></span> takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It derives new hypotheses by injectivity of
+ <span><strong class="command">K</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>The new sequent to prove is equal to the current sequent
+ with the additional hypotheses
+ <span><strong class="command">t<sub>1</sub>=t'<sub>1</sub></strong></span> ... <span><strong class="command">t<sub>n</sub>=t'<sub>n</sub></strong></span>.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_id.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_intro.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">id </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> intro [id]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>intro [id]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_injection.html" title="injection sterm" /><link rel="next" href="tac_intros.html" title="intros <intros_spec>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">intro [id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_injection.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intros.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_intro"></a>intro [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>intro H</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the sequent to prove must be an implication
+ or a universal quantification.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the right introduction rule for implication,
+ closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding to the hypothesis
+ the antecedent of the implication and setting the conclusion
+ to the consequent of the implicaiton. The name of the new
+ hypothesis is <span><strong class="command">H</strong></span> if provided; otherwise it
+ is automatically generated.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_injection.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_intros.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">injection sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> intros <intros_spec></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>intros <intros_spec></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intro.html" title="intro [id]" /><link rel="next" href="tac_inversion.html" title="inversion sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">intros <intros_spec></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_inversion.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_intros"></a>intros <intros_spec></h2></div></div></div><p><strong class="userinput"><code>intros hyps</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>If <span><strong class="command">hyps</strong></span> specifies a number of hypotheses
+ to introduce, then the conclusion of the current sequent must
+ be formed by at least that number of imbricated implications
+ or universal quantifications.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies several times the right introduction rule for
+ implication, closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding a number of new
+ hypotheses equal to the number of new hypotheses requested.
+ If the user does not request a precise number of new hypotheses,
+ it adds as many hypotheses as possible.
+ The name of each new hypothesis is either popped from the
+ user provided list of names, or it is automatically generated when
+ the list is (or becomes) empty.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_intro.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_inversion.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">intro [id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> inversion sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>inversion sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intros.html" title="intros <intros_spec>" /><link rel="next" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">inversion sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_inversion"></a>inversion <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>inversion t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span><strong class="command">t</strong></span> must be an inductive
+ type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span><strong class="command">t</strong></span> paying attention
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens one new sequent to prove for each case in the
+ definition of the type of <span><strong class="command">t</strong></span>. With respect to
+ a simple elimination, each new sequent has additional hypotheses
+ that states the equalities of the "right parameters"
+ of the inductive type with terms originally present in the
+ sequent to prove.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">intros <intros_spec> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> lapply [depth=nat] sterm [to <term list>] [using id]</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>lapply [depth=nat] sterm [to <term list>] [using id]</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_inversion.html" title="inversion sterm" /><link rel="next" href="tac_left.html" title="left" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">lapply [depth=nat] sterm [to <term list>] [using id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_left.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_lapply"></a>lapply [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [to <term list>] [using <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>lapply ???</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_left.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">inversion sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> left</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>left</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /><link rel="next" href="tac_letin.html" title="letin id ≝ sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">left</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_lapply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_letin.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_left"></a>left</h2></div></div></div><p><strong class="userinput"><code>left </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <span><strong class="command">constructor</strong></span> tactic.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_lapply.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_letin.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">lapply [depth=nat] sterm [to <term list>] [using id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> letin id ≝ sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>letin id ≝ sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_left.html" title="left" /><link rel="next" href="tac_normalize.html" title="normalize <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">letin id ≝ sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_normalize.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_letin"></a>letin <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> ≝ <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>letin x ≝ t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It adds to the context of the current sequent to prove a new
+ definition <span><strong class="command">x ≝ t</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_normalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">left </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> normalize <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>normalize <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_letin.html" title="letin id ≝ sterm" /><link rel="next" href="tac_paramodulation.html" title="paramodulation <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">normalize <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_letin.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_paramodulation.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_normalize"></a>normalize <pattern></h2></div></div></div><p><strong class="userinput"><code>normalize patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
+ with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_letin.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_paramodulation.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">letin id ≝ sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> paramodulation <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>paramodulation <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_normalize.html" title="normalize <pattern>" /><link rel="next" href="tac_reduce.html" title="reduce <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">paramodulation <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_normalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reduce.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_paramodulation"></a>paramodulation <pattern></h2></div></div></div><p><strong class="userinput"><code>paramodulation patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_normalize.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reduce.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">normalize <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reduce <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>reduce <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_paramodulation.html" title="paramodulation <pattern>" /><link rel="next" href="tac_reflexivity.html" title="reflexivity" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">reduce <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reflexivity.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_reduce"></a>reduce <pattern></h2></div></div></div><p><strong class="userinput"><code>reduce patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
+ with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reflexivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">paramodulation <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reflexivity</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>reflexivity</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reduce.html" title="reduce <pattern>" /><link rel="next" href="tac_replace.html" title="replace <pattern> with sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">reflexivity</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reduce.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_replace.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_reflexivity"></a>reflexivity</h2></div></div></div><p><strong class="userinput"><code>reflexivity </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ <span><strong class="command">t=t</strong></span> for some term <span><strong class="command">t</strong></span></p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by reflexivity
+ of equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_reduce.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_replace.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">reduce <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> replace <pattern> with sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>replace <pattern> with sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reflexivity.html" title="reflexivity" /><link rel="next" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">replace <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reflexivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_rewrite.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_replace"></a>replace <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces the subterms of the current sequent matched by
+ <span><strong class="command">patt</strong></span> with the new term <span><strong class="command">t</strong></span>.
+ For each subterm matched by the pattern, <span><strong class="command">t</strong></span> is
+ disambiguated in the context of the subterm.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>For each matched term <span><strong class="command">t'</strong></span> it opens
+ a new sequent to prove whose conclusion is
+ <span><strong class="command">t'=t</strong></span>.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_reflexivity.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_rewrite.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">reflexivity </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> rewrite [<|>] sterm <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>rewrite [<|>] sterm <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_replace.html" title="replace <pattern> with sterm" /><link rel="next" href="tac_right.html" title="right" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">rewrite [<|>] sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_replace.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_right.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_rewrite"></a>rewrite [<|>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>rewrite dir p patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must be the proof of an equality,
+ possibly under some hypotheses.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It looks in every term matched by <span><strong class="command">patt</strong></span>
+ for all the occurrences of the
+ left hand side of the equality that <span><strong class="command">p</strong></span> proves
+ (resp. the right hand side if <span><strong class="command">dir</strong></span> is
+ <span><strong class="command"><</strong></span>). Every occurence found is replaced with
+ the opposite side of the equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens one new sequent for each hypothesis of the
+ equality proved by <span><strong class="command">p</strong></span> that is not closed
+ by unification.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_replace.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_right.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">replace <pattern> with sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> right</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>right</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /><link rel="next" href="tac_ring.html" title="ring" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">right</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_rewrite.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_ring.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_right"></a>right</h2></div></div></div><p><strong class="userinput"><code>right </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least two constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 2</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the second
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <span><strong class="command">constructor</strong></span> tactic.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_rewrite.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_ring.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">rewrite [<|>] sterm <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> ring</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>ring</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_right.html" title="right" /><link rel="next" href="tac_simplify.html" title="simplify <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">ring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_right.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_simplify.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_ring"></a>ring</h2></div></div></div><p><strong class="userinput"><code>ring </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be an
+ equality over Coq's real numbers that can be proved using
+ the ring properties of the real numbers only.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent veryfying the equality by
+ means of computation (i.e. this is a reflexive tactic, implemented
+ exploiting the "two level reasoning" technique).</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_right.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_simplify.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">right </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> simplify <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>simplify <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_ring.html" title="ring" /><link rel="next" href="tac_split.html" title="split" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">simplify <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_ring.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_split.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_simplify"></a>simplify <pattern></h2></div></div></div><p><strong class="userinput"><code>simplify patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
+ with other convertible terms that are supposed to be simpler.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_ring.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_split.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">ring </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> split</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>split</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_simplify.html" title="simplify <pattern>" /><link rel="next" href="tac_symmetry.html" title="symmetry" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">split</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_simplify.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_symmetry.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_split"></a>split</h2></div></div></div><p><strong class="userinput"><code>split </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <span><strong class="command">constructor</strong></span> tactic.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_simplify.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_symmetry.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">simplify <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> symmetry</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>symmetry</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_split.html" title="split" /><link rel="next" href="tac_transitivity.html" title="transitivity sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">symmetry</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_split.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_transitivity.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_symmetry"></a>symmetry</h2></div></div></div><p>The tactic <span><strong class="command">symmetry</strong></span> </p><p><strong class="userinput"><code>symmetry </code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It swaps the two sides of the equalityusing the symmetric
+ property.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_split.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_transitivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">split </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> transitivity sterm</td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>transitivity sterm</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_symmetry.html" title="symmetry" /><link rel="next" href="tac_unfold.html" title="unfold [sterm] <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">transitivity sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_symmetry.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_unfold.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_transitivity"></a>transitivity <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>transitivity t</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by transitivity of the equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents <span><strong class="command">l=t</strong></span> and
+ <span><strong class="command">t=r</strong></span> where <span><strong class="command">l</strong></span> and <span><strong class="command">r</strong></span> are the left and right hand side of the equality in the conclusion of
+the current sequent to prove.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_symmetry.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_unfold.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">symmetry </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> unfold [sterm] <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>unfold [sterm] <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_transitivity.html" title="transitivity sterm" /><link rel="next" href="tac_whd.html" title="whd <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">unfold [sterm] <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_transitivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_whd.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_unfold"></a>unfold [<span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] <pattern></h2></div></div></div><p><strong class="userinput"><code>unfold t patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It finds all the occurrences of <span><strong class="command">t</strong></span>
+ (possibly applied to arguments) in the subterms matched by
+ <span><strong class="command">patt</strong></span>. Then it δ-expands each occurrence,
+ also performing β-reduction of the obtained term. If
+ <span><strong class="command">t</strong></span> is omitted it defaults to each
+ subterm matched by <span><strong class="command">patt</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_transitivity.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_whd.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">transitivity sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> whd <pattern></td></tr></table></div></body></html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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>whd <pattern></title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_unfold.html" title="unfold [sterm] <pattern>" /><link rel="next" href="sec_tacticals.html" title="Chapter 7. Tacticals" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">whd <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_unfold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="sec_tacticals.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_whd"></a>whd <pattern></h2></div></div></div><p><strong class="userinput"><code>whd patt</code></strong></p><p>
+ </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
+ with their βδιζ-weak-head normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
+ </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_unfold.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_tacticals.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">unfold [sterm] <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 7. Tacticals</td></tr></table></div></body></html>
projects / helm.git / commitdiff