2 <!-- ============= Getting started ============================== -->
4 <chapter id="sec_gettingstarted">
5 <title>Getting started</title>
6 <para> If you are already familiar with the Calculus of (Co)Inductive
7 Constructions (CIC) and with interactive theorem provers with procedural
8 proof languages (expecially Coq), getting started with Matita is relatively
9 easy. You just need to learn how to type Unicode symbols, how to browse
10 and search the library and how to author a proof script.</para>
13 <title>How to type Unicode symbols</title>
14 <para>Unicode characters can be typed in several ways:</para>
16 <listitem><para>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</para>
18 <listitem><para>Typing the ligature "\name" where "name"
19 is a standard Unicode or LaTeX name for the character. Pressing
20 "Alt+L" just after the last character of the name converts
21 the ligature to the Unicode symbol. This operation is
22 not required since Matita understands also the "\name"
23 sequences. E.g. "\Omega" followed by Alt+L generates
26 <listitem><para>Typing one of the following ligatures (and optionally
27 converting the ligature to the Unicode character has described before):
28 ":=" (which stands for ≝); "->" (which stands for
29 "→"); "=>" (which stands for "⇒").</para>
33 <sect1 id="cicbrowser">
34 <title>Browsing and searching</title>
35 <para>The CIC browser is used to browse and search the library.
36 You can open a new CIC browser selecting "New Cic Browser"
37 from the "View" menu of Matita, or by pressing "F3".
38 The CIC browser is similar to a traditional Web browser.</para>
39 <sect2 id="browsinglib">
40 <title>Browsing the library</title>
41 <para>To browse the library, type in the location bar the absolute URI of
42 the theorem, definition or library fragment you are interested in.
43 "cic:/" is the root of the library. Contributions developed
44 in Matita are under "cic:/matita"; all the others are
45 part of the library of Coq.</para>
46 <para>Following the hyperlinks it is possible to navigate in the Web
47 of mathematical notions. Proof are rendered in pseudo-natural language
48 and mathematical notation is used for formulae. For now, mathematical
49 notation must be included in the current script to be activated, but we
50 plan to remove this limitation.</para>
52 <sect2 id="aboutproof">
53 <title>Looking at a proof under development</title>
54 <para>A proof under development is not yet part of the library.
55 The special URI "about:proof" can be used to browse the
56 proof currently under development, if there is one.
57 The "home" button of the CIC browser sets the location bar to
58 "about:proof".
62 <title>Searching the library</title>
63 <para>The query bar of the CIC browser can be used to search the library
64 of Matita for theorems or definitions that match certain criteria.
65 The criteria is given by typing a term in the query bar and selecting
66 an action in the drop down menu right of it.</para>
68 <title>Searching by name</title>
72 <title>List of lemmas that can be applied</title>
76 <title>Searching by exact match</title>
80 <title>List of elimination principles for a given type</title>
84 <title>Searching by instantiation</title>
89 <sect1 id="authoring">
90 <title>Authoring</title>
91 <sect2 id="compilation">
92 <title>How to compile a script</title>
94 Scripts are compiled to base URIs. Base URIs are of the form
95 "cic:/matita/path" and are given once for all for a set
96 of scripts using the "root" file.
99 A "root" file has to be placed in the root of a script set,
100 for example, consider the following files and directories, and
101 assume you keep files in "list" separated from files
102 in "sort" (for example the former directory may contain
103 functions and proofs about lists, while latter sorting algorithms
105 <programlisting><![CDATA[
107 list.ma (* depending just on the standard library *)
109 swap.ma (* including list.ma *)
111 qsort.ma (* including utils/swap.ma *)
113 To be able to compile properly the contents of "list"
114 a file called root has to be placed in it. The file should be like
115 the following snippet.
116 <programlisting><![CDATA[
117 baseuri=cic:/matita/mydatastructures
119 This file tells &appname; that objects generated by
120 "list.ma" have to be placed in
121 "cic:/matita/mydatastructures/list" while
123 "swap.ma" have to be placed in
124 "cic:/matita/mydatastructures/utils/swap".
127 Once you created the root file, you must generate a depend file.
128 Enter the "list" directory (the root of yuor file set)
129 and type "matitadep". Remember to regenerate the depend file
130 every time you alter the dependencies of your files (for example
131 including other scripts).
132 You can now compile you files typing "matitac".
135 To compile the "sort" directory, create a root file
136 in "sort/" like the following one and then run
137 "matitadep".
138 <programlisting><![CDATA[
139 baseuri=cic:/matita/myalgorithms
140 include_paths=../list
142 The include_paths field can declare a list of paths separated by space.
143 Please omit any "/" from the end of base URIs or paths.
146 <sect2 id="authoringinterface">
147 <title>The authoring interface</title>