2 <!-- =========== Terms, declarations and definitions ============ -->
4 <chapter id="sec_terms">
5 <title>Terms, axioms, definitions, declarations and proofs</title>
16 <tr><td/><td>|</td><td><term> <term></td>
17 <td>application</td></tr>
24 <entry><term></entry>
26 <entry><id></entry>
27 <entry>identifier</entry>
32 <entry><term> <term></entry>
33 <entry>application</entry>
38 <entry>λ<id>[: <term>].<term></entry>
39 <entry>λ-abstraction</entry>
44 <entry>Π<id>[: <term>].<term></entry>
45 <entry>dependent product meant to define a datatype</entry>
50 <entry>∀<id>[: <term>].<term></entry>
51 <entry>dependent product meant to define a proposition</entry>
56 <entry><term> → <term></entry>
57 <entry>non-dependent product (logical implication or function space)</entry>
62 <entry>let [<id>|(<id>: <term>)] ≝ <term> in <term></entry>
63 <entry>local definition</entry>
68 <entry>let [co]rec <id> ≝ <term> in <term></entry>
69 <entry>local definition</entry>
83 <title>axiom <id>: <term></title>
84 <titleabbrev>axiom</titleabbrev>
85 <para><userinput>axiom H: P</userinput></para>
86 <para><command>H</command> is declared as an axiom that states <command>P</command></para>
89 <sect1 id="definition">
90 <title>definition <id>[: <term>] [≝ <term>]</title>
91 <titleabbrev>definition</titleabbrev>
92 <para><userinput>definition f: T ≝ t</userinput></para>
93 <para><command>f</command> is defined as <command>t</command>;
94 <command>T</command> is its type. An error is raised if the type of
95 <command>t</command> is not convertible to <command>T</command>.</para>
96 <para><command>T</command> is inferred from <command>t</command> if
98 <para><command>t</command> can be omitted only if <command>T</command> is
99 given. In this case Matita enters in interactive mode and
100 <command>f</command> must be defined by means of tactics.</para>
101 <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
104 <sect1 id="inductive">
105 <title>[co]inductive <id> (of inductive types)</title>
106 <titleabbrev>(co)inductive types declaration</titleabbrev>
107 <para> &TODO; </para>
111 <title>Proofs</title>
113 <title>theorem <id>[: <term>] [≝ <term>]</title>
114 <titleabbrev>theorem</titleabbrev>
115 <para><userinput>theorem f: P ≝ p</userinput></para>
116 <para>Proves a new theorem <command>f</command> whose thesis is
117 <command>P</command>.</para>
118 <para>If <command>p</command> is provided, it must be a proof term for
119 <command>P</command>. Otherwise an interactive proof is started.</para>
120 <para><command>P</command> can be omitted only if the proof is not
122 <para>Proving a theorem already proved in the library is an error.
123 To provide an alternative name and proof for the same theorem, use
124 <command>variant f: P ≝ p</command>.</para>
125 <para>A warning is raised if the name of the theorem cannot be obtained
126 by mangling the name of the constants in its thesis.</para>
127 <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
130 <title>variant <id>[: <term>] [≝ <term>]</title>
131 <titleabbrev>variant</titleabbrev>
132 <para><userinput>variant f: T ≝ t</userinput></para>
133 <para>Same as <command>theorem f: T ≝ t</command>, but it does not
134 complain if the theorem has already been proved. To be used to give
135 an alternative name or proof to a theorem.</para>
138 <title>lemma <id>[: <term>] [≝ <term>]</title>
139 <titleabbrev>lemma</titleabbrev>
140 <para><userinput>lemma f: T ≝ t</userinput></para>
141 <para>Same as <command>theorem f: T ≝ t</command></para>
144 <title>fact <id>[: <term>] [≝ <term>]</title>
145 <titleabbrev>fact</titleabbrev>
146 <para><userinput>fact f: T ≝ t</userinput></para>
147 <para>Same as <command>theorem f: T ≝ t</command></para>
150 <title>remark <id>[: <term>] [≝ <term>]</title>
151 <titleabbrev>remark</titleabbrev>
152 <para><userinput>remark f: T ≝ t</userinput></para>
153 <para>Same as <command>theorem f: T ≝ t</command></para>