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><para>Non terminal symbols are emphasized and have a link to their
9 definition. E.g.: &term;</para></listitem>
10 <listitem><para>Terminal symbols are in bold. E.g.:
11 <emphasis role="bold">theorem</emphasis></para></listitem>
12 <listitem><para>Optional sequences of elements are put in square brackets.
13 E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
14 <listitem><para>Alternatives are put in square brakets and they are
15 separated by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</para></listitem>
16 <listitem><para>Repetition of sequences of elements are given by putting the
17 first sequence in square brackets, that are followed by three dots.
18 E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
20 <sect1 id="terms_and_co">
21 <title>Terms & co.</title>
23 <title>Lexical conventions</title>
25 <table frame="all" rowsep="0" colsep="0">
30 <entry id="id">&id;</entry>
32 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
37 <table frame="all" rowsep="0" colsep="0">
42 <entry id="nat">&nat;</entry>
44 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
49 <table frame="all" rowsep="0" colsep="0">
54 <entry id="uri">&uri;</entry>
56 <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
66 <table frame="all" rowsep="0" colsep="0">
71 <entry id="term">&term;</entry>
73 <entry>&sterm;</entry>
74 <entry>simple or delimited term</entry>
79 <entry>&term; &term;</entry>
80 <entry>application</entry>
85 <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
86 <entry>λ-abstraction</entry>
91 <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
92 <entry>dependent product meant to define a datatype</entry>
97 <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
98 <entry>dependent product meant to define a proposition</entry>
103 <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
104 <entry>non-dependent product (logical implication or function space)</entry>
109 <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>
110 <entry>local definition</entry>
115 <entry><emphasis role="bold">let</emphasis>
116 [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
117 &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;]
118 [<emphasis role="bold">:</emphasis> &term;]
119 <emphasis role="bold">≝</emphasis> &term;
121 <entry>(co)recursive definitions</entry>
127 [<emphasis role="bold">and</emphasis>
128 [&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;]
129 [<emphasis role="bold">:</emphasis> &term;]
130 <emphasis role="bold">≝</emphasis> &term;]…
138 <emphasis role="bold">in</emphasis> &term;
146 <entry>user provided notation</entry>
152 <table frame="all" rowsep="0" colsep="0">
153 <title>Simple terms</title>
157 <entry id="sterm">&sterm;</entry>
159 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
165 <entry>&id;[<emphasis role="bold">\subst[</emphasis>
166 &id;<emphasis role="bold">≔</emphasis>&term;
167 [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
168 <emphasis role="bold">]</emphasis>]
170 <entry>identifier with optional explicit named substitution</entry>
176 <entry>a qualified reference</entry>
181 <entry><emphasis role="bold">Prop</emphasis></entry>
182 <entry>the impredicative sort of propositions</entry>
187 <entry><emphasis role="bold">Set</emphasis></entry>
188 <entry>the impredicate sort of datatypes</entry>
193 <entry><emphasis role="bold">Type</emphasis></entry>
194 <entry>one predicative sort of datatypes</entry>
199 <entry><emphasis role="bold">?</emphasis></entry>
200 <entry>implicit argument</entry>
205 <entry><emphasis role="bold">?n</emphasis>
206 [<emphasis role="bold">[</emphasis>
207 [<emphasis role="bold">_</emphasis>|&term;]…
208 <emphasis role="bold">]</emphasis>]</entry>
209 <entry>metavariable</entry>
214 <entry><emphasis role="bold">match</emphasis> &term;
215 [ <emphasis role="bold">in</emphasis> &term; ]
216 [ <emphasis role="bold">return</emphasis> &term; ]
217 <emphasis role="bold">with</emphasis>
219 <entry>case analysis</entry>
225 <emphasis role="bold">[</emphasis>
226 &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
228 <emphasis role="bold">|</emphasis>
229 &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
230 ]…<emphasis role="bold">]</emphasis> </entry>
236 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
243 <entry>user provided notation at precedence 90</entry>
249 <table frame="all" rowsep="0" colsep="0">
250 <title>Arguments</title>
254 <entry id="args">&args;</entry>
257 <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
259 <entry>ignored argument</entry>
265 <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
267 <entry>ignored argument</entry>
272 <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
278 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
285 <table frame="all" rowsep="0" colsep="0">
286 <title>Miscellaneous arguments</title>
290 <entry id="args2">&args2;</entry>
298 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
305 <table frame="all" rowsep="0" colsep="0">
306 <title>Pattern matching</title>
310 <entry id="match_pattern">&match_pattern;</entry>
313 <entry>0-ary constructor</entry>
318 <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
319 <entry>n-ary constructor (binds the n arguments)</entry>
329 <sect1 id="axiom_definition_declaration">
330 <title>Definitions and declarations</title>
332 <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
333 <titleabbrev>axiom</titleabbrev>
334 <para><userinput>axiom H: P</userinput></para>
335 <para><command>H</command> is declared as an axiom that states <command>P</command></para>
337 <sect2 id="definition">
338 <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
339 <titleabbrev>definition</titleabbrev>
340 <para><userinput>definition f: T ≝ t</userinput></para>
341 <para><command>f</command> is defined as <command>t</command>;
342 <command>T</command> is its type. An error is raised if the type of
343 <command>t</command> is not convertible to <command>T</command>.</para>
344 <para><command>T</command> is inferred from <command>t</command> if
346 <para><command>t</command> can be omitted only if <command>T</command> is
347 given. In this case Matita enters in interactive mode and
348 <command>f</command> must be defined by means of tactics.</para>
349 <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
351 <sect2 id="inductive">
352 <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;]…
353 [<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;]…]…
355 <titleabbrev>(co)inductive types declaration</titleabbrev>
356 <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
357 <para>Declares a family of two mutually inductive types
358 <command>i</command> and <command>i'</command> whose types are
359 <command>S</command> and <command>S'</command>, which must be convertible
361 <para>The constructors <command>ki</command> of type <command>Ti</command>
362 and <command>ki'</command> of type <command>Ti'</command> are also
363 simultaneously declared. The declared types <command>i</command> and
364 <command>i'</command> may occur in the types of the constructors, but
365 only in strongly positive positions according to the rules of the
367 <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
368 <para>If the keyword <command>coinductive</command> is used, the declared
369 types are considered mutually coinductive.</para>
370 <para>Elimination principles for the record are automatically generated
371 by Matita, if allowed by the typing rules of the calculus according to
372 the sort <command>S</command>. If generated,
373 they are named <command>i_ind</command>, <command>i_rec</command> and
374 <command>i_rect</command> according to the sort of their induction
378 <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>
379 <titleabbrev>record</titleabbrev>
380 <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
381 <para>Declares a new record family <command>id</command> parameterized over
382 <command>x,y,z</command>.</para>
383 <para><command>S</command> is the type of the record
384 and it must be convertible to a sort.</para>
385 <para>Each field <command>fi</command> is declared by giving its type
386 <command>Ti</command>. A record without any field is admitted.</para>
387 <para>Elimination principles for the record are automatically generated
388 by Matita, if allowed by the typing rules of the calculus according to
389 the sort <command>S</command>. If generated,
390 they are named <command>i_ind</command>, <command>i_rec</command> and
391 <command>i_rect</command> according to the sort of their induction
393 <para>For each field <command>fi</command> a record projection
394 <command>fi</command> is also automatically generated if projection
395 is allowed by the typing rules of the calculus according to the
396 sort <command>S</command>, the type <command>T1</command> and
397 the definability of depending record projections.</para>
398 <para>If the type of a field is declared with <command>:></command>,
399 the corresponding record projection becomes an implicit coercion.
400 This is just syntactic sugar and it has the same effect of declaring the
401 record projection as a coercion later on.</para>
406 <title>Proofs</title>
408 <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
409 <titleabbrev>theorem</titleabbrev>
410 <para><userinput>theorem f: P ≝ p</userinput></para>
411 <para>Proves a new theorem <command>f</command> whose thesis is
412 <command>P</command>.</para>
413 <para>If <command>p</command> is provided, it must be a proof term for
414 <command>P</command>. Otherwise an interactive proof is started.</para>
415 <para><command>P</command> can be omitted only if the proof is not
417 <para>Proving a theorem already proved in the library is an error.
418 To provide an alternative name and proof for the same theorem, use
419 <command>variant f: P ≝ p</command>.</para>
420 <para>A warning is raised if the name of the theorem cannot be obtained
421 by mangling the name of the constants in its thesis.</para>
422 <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
425 <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
426 <titleabbrev>variant</titleabbrev>
427 <para><userinput>variant f: T ≝ t</userinput></para>
428 <para>Same as <command>theorem f: T ≝ t</command>, but it does not
429 complain if the theorem has already been proved. To be used to give
430 an alternative name or proof to a theorem.</para>
433 <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
434 <titleabbrev>lemma</titleabbrev>
435 <para><userinput>lemma f: T ≝ t</userinput></para>
436 <para>Same as <command>theorem f: T ≝ t</command></para>
439 <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
440 <titleabbrev>fact</titleabbrev>
441 <para><userinput>fact f: T ≝ t</userinput></para>
442 <para>Same as <command>theorem f: T ≝ t</command></para>
445 <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
446 <titleabbrev>remark</titleabbrev>
447 <para><userinput>remark f: T ≝ t</userinput></para>
448 <para>Same as <command>theorem f: T ≝ t</command></para>