<!-- =========== Terms, declarations and definitions ============ -->
<chapter id="sec_terms">
- <title>Terms, axioms, definitions, declarations and proofs</title>
-
- <sect1 id="terms">
+ <title>Syntax</title>
+ <para>To describe syntax in this manual we use the following conventions:</para>
+ <orderedlist>
+ <listitem><para>Non terminal symbols are emphasized and have a link to their
+ definition. E.g.: &term;</para></listitem>
+ <listitem><para>Terminal symbols are in bold. E.g.:
+ <emphasis role="bold">theorem</emphasis></para></listitem>
+ <listitem><para>Optional sequences of elements are put in square brackets.
+ E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+ <listitem><para>Alternatives are put in square brakets and they are
+ separated by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</para></listitem>
+ <listitem><para>Repetition of sequences of elements are given by putting the
+ first sequence in square brackets, that are followed by three dots.
+ E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
+ </orderedlist>
+ <sect1 id="terms_and_co">
+ <title>Terms & co.</title>
+ <sect2 id="lexical">
+ <title>Lexical conventions</title>
+ <para>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>id</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="id">&id;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>nat</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="nat">&nat;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>uri</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="uri">&uri;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ </para>
+ </sect2>
+ <sect2 id="terms">
<title>Terms</title>
- <table>
- <tgroup>
- <thead />
+ <para>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Terms</title>
+ <tgroup cols="4">
<tbody>
<row>
- <entry id="id">&id;</entry>
+ <entry id="term">&term;</entry>
<entry>::=</entry>
- <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ <entry>&sterm;</entry>
+ <entry>simple or delimited term</entry>
</row>
- </tbody>
- </tgroup>
- </table>
- <table>
- <tgroup>
- <thead />
- <tbody>
<row>
- <entry id="nat">&nat;</entry>
- <entry>::=</entry>
- <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ <entry/>
+ <entry>|</entry>
+ <entry>&term; &term;</entry>
+ <entry>application</entry>
</row>
- </tbody>
- </tgroup>
- </table>
- <table>
- <tgroup>
- <thead />
- <tbody>
<row>
- <entry id="uri">&uri;</entry>
- <entry>::=</entry>
- <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>λ-abstraction</entry>
</row>
- </tbody>
- </tgroup>
- </table>
- <table>
- <tgroup>
- <thead />
- <tbody>
<row>
- <entry id="term">&term;</entry>
- <entry>::=</entry>
- <entry>&id;</entry>
- <entry>identifier</entry>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>dependent product meant to define a datatype</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry>&uri;</entry>
- <entry>a qualified reference</entry>
+ <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>dependent product meant to define a proposition</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">Prop</emphasis></entry>
- <entry>the impredicative sort of propositions</entry>
+ <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
+ <entry>non-dependent product (logical implication or function space)</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">Set</emphasis></entry>
- <entry>the impredicate sort of datatypes</entry>
+ <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
+ <entry>local definition</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">Type</emphasis></entry>
- <entry>one predicatie sort of datatypes</entry>
+ <entry><emphasis role="bold">let</emphasis>
+ [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
+ &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+ [<emphasis role="bold">:</emphasis> &term;]
+ <emphasis role="bold">≝</emphasis> &term;
+ </entry>
+ <entry>(co)recursive definitions</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ [<emphasis role="bold">and</emphasis>
+ [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+ [<emphasis role="bold">:</emphasis> &term;]
+ <emphasis role="bold">≝</emphasis> &term;]…
+ </entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ <emphasis role="bold">in</emphasis> &term;
+ </entry>
+ <entry/>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry>&term; &term;</entry>
- <entry>application</entry>
+ <entry>…</entry>
+ <entry>user provided notation</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Simple terms</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="sterm">&sterm;</entry>
+ <entry>::=</entry>
+ <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+ <entry/>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">λ</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
- <entry>λ-abstraction</entry>
+ <entry>&id;[<emphasis role="bold">\subst[</emphasis>
+ &id;<emphasis role="bold">≔</emphasis>&term;
+ [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
+ <emphasis role="bold">]</emphasis>]
+ </entry>
+ <entry>identifier with optional explicit named substitution</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">Π</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
- <entry>dependent product meant to define a datatype</entry>
+ <entry>&uri;</entry>
+ <entry>a qualified reference</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">∀</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
- <entry>dependent product meant to define a proposition</entry>
+ <entry><emphasis role="bold">Prop</emphasis></entry>
+ <entry>the impredicative sort of propositions</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
- <entry>non-dependent product (logical implication or function space)</entry>
+ <entry><emphasis role="bold">Set</emphasis></entry>
+ <entry>the impredicate sort of datatypes</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
- <entry>local definition</entry>
+ <entry><emphasis role="bold">Type</emphasis></entry>
+ <entry>one predicative sort of datatypes</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">?</emphasis></entry>
+ <entry>implicit argument</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">?n</emphasis>
+ [<emphasis role="bold">[</emphasis>
+ [<emphasis role="bold">_</emphasis>|&term;]…
+ <emphasis role="bold">]</emphasis>]</entry>
+ <entry>metavariable</entry>
</row>
<row>
<entry/>
<entry/>
<entry>
<emphasis role="bold">[</emphasis>
- &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+ &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
[
<emphasis role="bold">|</emphasis>
- &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+ &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
]…<emphasis role="bold">]</emphasis> </entry>
<entry/>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">let</emphasis>
- [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
- &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
- [<emphasis role="bold">:</emphasis> &term;]
- <emphasis role="bold">≝</emphasis> &term;
- </entry>
- <entry>(co)recursive definitions</entry>
+ <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+ <entry>cast</entry>
</row>
<row>
<entry/>
+ <entry>|</entry>
+ <entry>…</entry>
+ <entry>user provided notation at precedence 90</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Arguments</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="args">&args;</entry>
+ <entry>::=</entry>
+ <entry>
+ <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
+ </entry>
+ <entry>ignored argument</entry>
+ </row>
+ <row>
<entry/>
+ <entry>|</entry>
<entry>
- [<emphasis role="bold">and</emphasis>
- &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
- [<emphasis role="bold">:</emphasis> &term;]
- <emphasis role="bold">≝</emphasis> &term;]…
+ <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
</entry>
+ <entry>ignored argument</entry>
+ </row>
+ <row>
<entry/>
+ <entry>|</entry>
+ <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
+ <entry></entry>
</row>
<row>
<entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
<entry/>
- <entry>
- <emphasis role="bold">in</emphasis> &term;
- </entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Miscellaneous arguments</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="args2">&args2;</entry>
+ <entry>::=</entry>
+ <entry>&id;</entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
<entry/>
</row>
</tbody>
</tgroup>
</table>
- <table>
- <tgroup>
- <thead />
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Pattern matching</title>
+ <tgroup cols="4">
<tbody>
<row>
- <entry id="term_pattern">&term_pattern;</entry>
+ <entry id="match_pattern">&match_pattern;</entry>
<entry>::=</entry>
<entry>&id;</entry>
<entry>0-ary constructor</entry>
</tbody>
</tgroup>
</table>
+ </para>
+
+ </sect2>
</sect1>
- <sect1 id="axiom">
- <title>axiom &id;: &term;</title>
+ <sect1 id="axiom_definition_declaration">
+ <title>Definitions and declarations</title>
+ <sect2 id="axiom">
+ <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
<titleabbrev>axiom</titleabbrev>
<para><userinput>axiom H: P</userinput></para>
<para><command>H</command> is declared as an axiom that states <command>P</command></para>
- </sect1>
-
- <sect1 id="definition">
- <title>definition &id;[: &term;] [≝ &term;]</title>
+ </sect2>
+ <sect2 id="definition">
+ <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>definition</titleabbrev>
<para><userinput>definition f: T ≝ t</userinput></para>
<para><command>f</command> is defined as <command>t</command>;
given. In this case Matita enters in interactive mode and
<command>f</command> must be defined by means of tactics.</para>
<para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
- </sect1>
-
- <sect1 id="inductive">
- <title>[co]inductive &id; (of inductive types)</title>
+ </sect2>
+ <sect2 id="inductive">
+ <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
+[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…
+</title>
<titleabbrev>(co)inductive types declaration</titleabbrev>
- <para> &TODO; </para>
+ <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
+ <para>Declares a family of two mutually inductive types
+ <command>i</command> and <command>i'</command> whose types are
+ <command>S</command> and <command>S'</command>, which must be convertible
+ to sorts.</para>
+ <para>The constructors <command>ki</command> of type <command>Ti</command>
+ and <command>ki'</command> of type <command>Ti'</command> are also
+ simultaneously declared. The declared types <command>i</command> and
+ <command>i'</command> may occur in the types of the constructors, but
+ only in strongly positive positions according to the rules of the
+ calculus.</para>
+ <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
+ <para>If the keyword <command>coinductive</command> is used, the declared
+ types are considered mutually coinductive.</para>
+ <para>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <command>S</command>. If generated,
+ they are named <command>i_ind</command>, <command>i_rec</command> and
+ <command>i_rect</command> according to the sort of their induction
+ predicate.</para>
+ </sect2>
+ <sect2 id="record">
+ <title><emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
+ <titleabbrev>record</titleabbrev>
+ <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
+ <para>Declares a new record family <command>id</command> parameterized over
+ <command>x,y,z</command>.</para>
+ <para><command>S</command> is the type of the record
+ and it must be convertible to a sort.</para>
+ <para>Each field <command>fi</command> is declared by giving its type
+ <command>Ti</command>. A record without any field is admitted.</para>
+ <para>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <command>S</command>. If generated,
+ they are named <command>i_ind</command>, <command>i_rec</command> and
+ <command>i_rect</command> according to the sort of their induction
+ predicate.</para>
+ <para>For each field <command>fi</command> a record projection
+ <command>fi</command> is also automatically generated if projection
+ is allowed by the typing rules of the calculus according to the
+ sort <command>S</command>, the type <command>T1</command> and
+ the definability of depending record projections.</para>
+ <para>If the type of a field is declared with <command>:></command>,
+ 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.</para>
+ </sect2>
</sect1>
<sect1 id="proofs">
<title>Proofs</title>
<sect2 id="theorem">
- <title>theorem &id;[: &term;] [≝ &term;]</title>
+ <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>theorem</titleabbrev>
<para><userinput>theorem f: P ≝ p</userinput></para>
<para>Proves a new theorem <command>f</command> whose thesis is
<para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
</sect2>
<sect2 id="variant">
- <title>variant &id;[: &term;] [≝ &term;]</title>
+ <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>variant</titleabbrev>
<para><userinput>variant f: T ≝ t</userinput></para>
<para>Same as <command>theorem f: T ≝ t</command>, but it does not
an alternative name or proof to a theorem.</para>
</sect2>
<sect2 id="lemma">
- <title>lemma &id;[: &term;] [≝ &term;]</title>
+ <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>lemma</titleabbrev>
<para><userinput>lemma f: T ≝ t</userinput></para>
<para>Same as <command>theorem f: T ≝ t</command></para>
</sect2>
<sect2 id="fact">
- <title>fact &id;[: &term;] [≝ &term;]</title>
+ <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>fact</titleabbrev>
<para><userinput>fact f: T ≝ t</userinput></para>
<para>Same as <command>theorem f: T ≝ t</command></para>
</sect2>
<sect2 id="remark">
- <title>remark &id;[: &term;] [≝ &term;]</title>
+ <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<titleabbrev>remark</titleabbrev>
<para><userinput>remark f: T ≝ t</userinput></para>
<para>Same as <command>theorem f: T ≝ t</command></para>
projects / helm.git / blobdiff