2 <!-- =========== Terms, declarations and definitions ============ -->
4 <chapter id="sec_terms">
6 <para>To describe syntax in this manual we use the following conventions:</para>
8 <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
9 <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
10 <listitem>Optional sequences of elements are put in square brackets.
11 E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
12 <listitem>Alternatives are put in square brakets and they are separated
13 by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</listitem>
14 <listitem>Repetition of sequences of elements are given by putting the
15 first sequence in square brackets, that are followed by three dots.
16 E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
18 <sect1 id="terms_and_co">
19 <title>Terms & co.</title>
21 <title>Lexical conventions</title>
27 <entry id="id">&id;</entry>
29 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
39 <entry id="nat">&nat;</entry>
41 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
51 <entry id="uri">&uri;</entry>
53 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
66 <entry id="term">&term;</entry>
69 <entry>identifier</entry>
75 <entry>a qualified reference</entry>
80 <entry><emphasis role="bold">Prop</emphasis></entry>
81 <entry>the impredicative sort of propositions</entry>
86 <entry><emphasis role="bold">Set</emphasis></entry>
87 <entry>the impredicate sort of datatypes</entry>
92 <entry><emphasis role="bold">Type</emphasis></entry>
93 <entry>one predicative sort of datatypes</entry>
98 <entry>&term; &term;</entry>
99 <entry>application</entry>
104 <entry><emphasis role="bold">λ</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
105 <entry>λ-abstraction</entry>
110 <entry><emphasis role="bold">Π</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
111 <entry>dependent product meant to define a datatype</entry>
116 <entry><emphasis role="bold">∀</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
117 <entry>dependent product meant to define a proposition</entry>
122 <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
123 <entry>non-dependent product (logical implication or function space)</entry>
128 <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>
129 <entry>local definition</entry>
134 <entry><emphasis role="bold">match</emphasis> &term;
135 [ <emphasis role="bold">in</emphasis> &term; ]
136 [ <emphasis role="bold">return</emphasis> &term; ]
137 <emphasis role="bold">with</emphasis>
139 <entry>case analysis</entry>
145 <emphasis role="bold">[</emphasis>
146 &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
148 <emphasis role="bold">|</emphasis>
149 &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
150 ]…<emphasis role="bold">]</emphasis> </entry>
156 <entry><emphasis role="bold">let</emphasis>
157 [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
158 &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
159 [<emphasis role="bold">:</emphasis> &term;]
160 <emphasis role="bold">≝</emphasis> &term;
162 <entry>(co)recursive definitions</entry>
168 [<emphasis role="bold">and</emphasis>
169 &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
170 [<emphasis role="bold">:</emphasis> &term;]
171 <emphasis role="bold">≝</emphasis> &term;]…
179 <emphasis role="bold">in</emphasis> &term;
192 <entry id="term_pattern">&term_pattern;</entry>
195 <entry>0-ary constructor</entry>
200 <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
201 <entry>n-ary constructor (binds the n arguments)</entry>
209 <sect1 id="axiom_definition_declaration">
210 <title>Definitions and declarations</title>
212 <title>axiom &id;: &term;</title>
213 <titleabbrev>axiom</titleabbrev>
214 <para><userinput>axiom H: P</userinput></para>
215 <para><command>H</command> is declared as an axiom that states <command>P</command></para>
217 <sect2 id="definition">
218 <title>definition &id;[: &term;] [≝ &term;]</title>
219 <titleabbrev>definition</titleabbrev>
220 <para><userinput>definition f: T ≝ t</userinput></para>
221 <para><command>f</command> is defined as <command>t</command>;
222 <command>T</command> is its type. An error is raised if the type of
223 <command>t</command> is not convertible to <command>T</command>.</para>
224 <para><command>T</command> is inferred from <command>t</command> if
226 <para><command>t</command> can be omitted only if <command>T</command> is
227 given. In this case Matita enters in interactive mode and
228 <command>f</command> must be defined by means of tactics.</para>
229 <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
231 <sect2 id="inductive">
232 <title>[co]inductive &id; (of inductive types)</title>
233 <titleabbrev>(co)inductive types declaration</titleabbrev>
234 <para> &TODO; </para>
239 <title>Proofs</title>
241 <title>theorem &id;[: &term;] [≝ &term;]</title>
242 <titleabbrev>theorem</titleabbrev>
243 <para><userinput>theorem f: P ≝ p</userinput></para>
244 <para>Proves a new theorem <command>f</command> whose thesis is
245 <command>P</command>.</para>
246 <para>If <command>p</command> is provided, it must be a proof term for
247 <command>P</command>. Otherwise an interactive proof is started.</para>
248 <para><command>P</command> can be omitted only if the proof is not
250 <para>Proving a theorem already proved in the library is an error.
251 To provide an alternative name and proof for the same theorem, use
252 <command>variant f: P ≝ p</command>.</para>
253 <para>A warning is raised if the name of the theorem cannot be obtained
254 by mangling the name of the constants in its thesis.</para>
255 <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
258 <title>variant &id;[: &term;] [≝ &term;]</title>
259 <titleabbrev>variant</titleabbrev>
260 <para><userinput>variant f: T ≝ t</userinput></para>
261 <para>Same as <command>theorem f: T ≝ t</command>, but it does not
262 complain if the theorem has already been proved. To be used to give
263 an alternative name or proof to a theorem.</para>
266 <title>lemma &id;[: &term;] [≝ &term;]</title>
267 <titleabbrev>lemma</titleabbrev>
268 <para><userinput>lemma f: T ≝ t</userinput></para>
269 <para>Same as <command>theorem f: T ≝ t</command></para>
272 <title>fact &id;[: &term;] [≝ &term;]</title>
273 <titleabbrev>fact</titleabbrev>
274 <para><userinput>fact f: T ≝ t</userinput></para>
275 <para>Same as <command>theorem f: T ≝ t</command></para>
278 <title>remark &id;[: &term;] [≝ &term;]</title>
279 <titleabbrev>remark</titleabbrev>
280 <para><userinput>remark f: T ≝ t</userinput></para>
281 <para>Same as <command>theorem f: T ≝ t</command></para>