2 This is an interactive tutorial. To let you interact on line with the system,
3 you must first of all register yourself.
5 Before starting, let us briefly explain the meaning of the menu buttons.
6 With the Advance and Retract buttons you respectively perform and undo single
7 computational steps. Each step consists in reading a user command, and processing
8 it. The part of the user input file (called script) already executed by the
9 system will be colored, and will not be editable any more. The advance bottom
10 will also automatically advance the focus of the window, but you can inspect the
11 whole file using the scroll bars, as usual. Comments are skipped.
12 Try to advance and retract a few steps, to get the feeling of the system. You can
13 also come back here by using the top button, that takes you at the beginning of
14 a file. The play button is meant to process the script up to a position
15 previously selected by the user; the bottom button execute the whole script.
16 That's it: we are
\ 5span style="font-family: Verdana,sans-serif;"
\ 6 \ 5/span
\ 6now ready to start.
18 The first thing to say is that in a system like Matita's very few things are
19 built-in: not even booleans or logical connectives. The main philosophy of the
20 system is to let you define your own data-types and functions using a powerful
21 computational mechanism based on the declaration of inductive types.
23 Let us start this tutorial with a simple example based on the following well
26 \ 5h2 class="section"
\ 6The goat, the wolf and the cabbage
\ 5/h2
\ 6\ 5div class="paragraph"
\ 6\ 5/div
\ 6A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
27 is only one place available on his boat. Furthermore, the goat will eat the
28 cabbage if they are left alone on the same bank, and similarly the wolf will eat
29 the goat. The problem consists in bringing all three items safely across the
32 Our first data type defines the two banks of the river, which will be named east
33 and west. It is a simple example of enumerated type, defined by explicitly
34 declaring all its elements. The type itself is called "bank".
35 Before giving its definition we "include" the file "logic.ma" that contains a
36 few preliminary notions not worth discussing for the moment.
39 include "basics/logic.ma".
41 inductive bank: Type[0] ≝
45 (* We can now define a simple function computing, for each bank of the river, the
48 definition opposite ≝ λs.
50 [ east ⇒
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6
51 | west ⇒
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6
54 (* Functions are live entities, and can be actually computed. To check this, let
55 us state the property that the opposite bank of east is west; every lemma needs a
56 name for further reference, and we call it "east_to_west". *)
58 lemma east_to_west :
\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6.
60 (* If you stop the execution here you will see a new window on the right side
61 of the screen: it is the goal window, providing a sequent like representation of
68 -----------------------
71 for each open goal remaining to be solved. A is the conclusion of the goal and
72 B1, ..., Bk is its context, that is the set of current hypothesis and type
73 declarations. In this case, we have only one goal, and its context is empty.
74 The proof proceeds by typing commands to the system. In this case, we
75 want to evaluate the function, that can be done by invoking the "normalize"
81 (* By executing it - just type the advance command - you will see that the goal
82 has changed to west = west, by reducing the subexpression (opposite east).
83 You may use the retract bottom to undo the step, if you wish.
85 The new goal west = west is trivial: it is just a consequence of reflexivity.
86 Such trivial steps can be just closed in Matita by typing a double slash.
87 We complete the proof by the qed command, that instructs the system to store the
88 lemma performing some book-keeping operations.
93 (* In exactly the same way, we can prove that the opposite side of west is east.
94 In this case, we avoid the unnecessary simplification step: // will take care of
97 lemma west_to_east :
\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6.
100 (* A slightly more complex problem consists in proving that opposite is
103 lemma idempotent_opposite : ∀x.
\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 x)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 x.
105 (* we start the proof moving x from the conclusion into the context, that is a
106 (backward) introduction step. Matita syntax for an introduction step is simply
107 the sharp character followed by the name of the item to be moved into the
108 context. This also allows us to rename the item, if needed: for instance if we
109 wish to rename x into b (since it is a bank), we just type #b. *)
113 (* See the effect of the execution in the goal window on the right: b has been
114 added to the context (replacing x in the conclusion); moreover its implicit type
115 "bank" has been made explicit.
117 But how are we supposed to proceed, now? Simplification cannot help us, since b
118 is a variable: just try to call normalize and you will see that it has no effect.
119 The point is that we must proceed by cases according to the possible values of b,
120 namely east and west. To this aim, you must invoke the cases command, followed by
121 the name of the hypothesis (more generally, an arbitrary expression) that must be
122 the object of the case analysis (in our case, b).
127 (* Executing the previous command has the effect of opening two subgoals,
128 corresponding to the two cases b=east and b=west: you may switch from one to the
129 other by using the hyperlinks over the top of the goal window.
130 Both goals can be closed by trivial computations, so we may use // as usual.
131 If we had to treat each subgoal in a different way, we should focus on each of
132 them in turn, in a way that will be described at the end of this section.
137 (* Instead of working with functions, it is sometimes convenient to work with
138 predicates. For instance, instead of defining a function computing the opposite
139 bank, we could declare a predicate stating when two banks are opposite to each
140 other. Only two cases are possible, leading naturally two the following
144 inductive opp :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6 →
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6 → Prop ≝
145 | east_west : opp
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6
146 | west_east : opp
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6.
148 (* In precisely the same way as "bank" is the smallest type containing east and
149 west, opp is the smallest predicate containing the two sub-cases east_west and
150 weast_east. If you have some familiarity with Prolog, you may look at opp as the
151 predicate definined by the two clauses - in this case, the two facts -
152 (opp east west) and (opp west east).
153 At the end of this section we shall prove that forall a and b,
154 (opp a b) iff a = opposite b.
155 For the moment, it is time to proceed with our formalization of the farmer's
157 A state of the system is defined by the position of four item: the goat, the
158 wolf, the cabbage, and the boat. The simplest way to declare such a data type
162 record state : Type[0] ≝
163 {goat_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
164 wolf_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
165 cabbage_pos:
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
166 boat_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6}.
168 (* When you define a record named foo, the system automatically defines a record
169 constructor named mk_foo. To construct a new record you pass as arguments to
170 mk_foo the values of the record fields *)
172 definition start ≝
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6.
173 definition end ≝
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6.
175 (* We must now define the possible moves. A natural way to do it is in the form
176 of a relation (a binary predicate) over states. *)
178 inductive move :
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 →
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 → Prop ≝
179 | move_goat: ∀g,g1,w,c.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 g g1 → move (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c g) (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g1 w c g1)
180 | move_wolf: ∀g,w,w1,c.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 w w1 → move (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c w) (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w1 c w1)
181 | move_cabbage: ∀g,w,c,c1.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 c c1 → move (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c c) (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c1 c1)
182 | move_boat: ∀g,w,c,b,b1.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 b b1 → move (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c b) (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c b1).
184 (* A state is safe if either the goat is on the same bank of the boat, or both
185 the wolf and the cabbage are on the opposite bank of the goat. *)
187 inductive safe_state :
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 → Prop ≝
188 | with_boat : ∀g,w,c.safe_state (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g w c g)
189 | opposite_side : ∀g,g1,b.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 g g1 → safe_state (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 g g1 g1 b).
191 (* Finally, a state y is reachable from x if either there is a single move
192 leading from x to y, or there is a safe state z such that z is reachable from x
193 and there is a move leading from z to y *)
195 inductive reachable :
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 →
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 → Prop ≝
196 | one : ∀x,y.
\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"
\ 6move
\ 5/a
\ 6 x y → reachable x y
197 | more : ∀x,z,y.
\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6reachable x z →
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"
\ 6safe_state
\ 5/a
\ 6 z →
\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"
\ 6move
\ 5/a
\ 6 z y → reachable x y.
199 (* Remarkably, Matita is now able to solve the problem by itslef, provided
200 you allow automation to exploit more resources. The command /n/ is similar to
201 //, where n is a measure of this complexity: in particular it is a bound to
202 the depth of the expected proof tree (more precisely, to the number of nested
203 applicative nodes). In this case, there is a solution in six moves, and we
204 need a few more applications to handle reachability, and side conditions.
205 The magic number to let automation work is, in this case, 9. *)
207 lemma problem:
\ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"
\ 6reachable
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"
\ 6start
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"
\ 6end
\ 5/a
\ 6.
210 (* Let us now try to derive the proof in a more interactive way. Of course, we
211 expect to need several moves to transfer all items from a bank to the other, so
212 we should start our proof by applying "more".
215 lemma problem1:
\ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"
\ 6reachable
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"
\ 6start
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"
\ 6end
\ 5/a
\ 6.
217 @
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6
219 (* We have now four open subgoals:
222 Y : reachable [east,east,east,east] X
224 Z : move X [west,west,west,west]
226 That is, we must guess a state X, such that this is reachable from start, it is
227 safe, and there is a move leading from X to end. All goals are active, that is
228 emphasized by the fact that they are all red. Any command typed by the user is
229 normally applied in parallel to all active goals, but clearly we must proceed
230 here is a different way for each of them. The way to do it, is by structuring
231 the script using the following syntax: [...|... |...|...] where we typically have
232 as many cells inside the brackets as the number of the active subgoals. The
233 interesting point is that we can associate with the three symbol "[", "|" and
234 "]" a small-step semantics that allow to execute them individually. In particular
236 - the operator "[" opens a new focusing section for the currently active goals,
237 and focus on the first of them
238 - the operator "|" shift the focus to the next goal
239 - the operator "]" close the focusing section, falling back to the previous level
240 and adding to it all remaining goals not yet closed
242 Let us see the effect of the "[" on our proof:
247 (* As you see, only the first goal has now the focus on. Moreover, all goals got
248 a progressive numerical label, to help designating them, if needed.
249 We can now proceed in several possible ways. The most straightforward way is to
250 provide the intermediate state, that is [east,west,west,east]. We can do it, by
251 just applying this term. *)
253 @(
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6)
255 (* This application closes the goal; at present, no goal has the focus on.
256 In order to act on the next goal, we must focus on it using the "|" operator. In
257 this case, we would like to skip the next goal, and focus on the trivial third
258 subgoal: a simple way to do it, is by retyping "|". The proof that
259 [east,west,west,east] is safe is trivial and can be done with //.*)
264 We then advance to the next goal, namely the fact that there is a move from
265 [east,west,west,east] to [west,west,west,west]; this is trivial too, but it
266 requires /2/ since move_goat opens an additional subgoal. By applying "]" we
267 refocus on the skipped goal, going back to a situation similar to the one we
272 (* Let us perform the next step, namely moving back the boat, in a sligtly
273 different way. The more operation expects as second argument the new
274 intermediate state, hence instead of applying more we can apply its
275 instantiation (more ? (mk_state east west west west)). The question mark is
276 an implicit argument to be guessed by the system. *)
278 \ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6@(
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"
\ 6mk_state
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6))
280 (* All subgoals are focused (they are all red). Two of them are trivial; we
281 just call automation at level 2, and it will close both of them, taking
282 us to the third move.*)
286 (* We must now move the wolf. Suppose that, instead of specifying the next state
287 we prefer to specify the move. In the style of the previous move, this amounts
288 to apply the term (more … (move_wolf … )) The dots are a convenient syntax to
289 express an arbitrary number of implicit parameters. *)
291 @(
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"
\ 6move_wolf
\ 5/a
\ 6 … ))
293 (* Unfortunately this is not enough to fully instantiate the intermediate state.
294 All goals still depend from an unknown bank B. Calling automation in this situation
295 does not help since it refuses to close subgoals instantiating other - still
296 open - goals. A way to proceed is to focus on the fourth "bank" subgoal,
297 instantiating it with the appropriate value, in this case east; then we close
298 focusing, and call automation. To focus on subgoal i, instead of typing "|" several
299 times we can just write "i:" as described by the following command. *)
301 [4: @
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6] /2/
303 (* An alternative, simpler way is to instantiate each move with the destination
304 bank. Let us complete the proof adopting this style. *)
306 @(
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"
\ 6move_goat
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 … )) /2/
307 @(
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"
\ 6move_cabbage
\ 5/a
\ 6 ??
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6 … )) /2/
308 @(
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"
\ 6move_boat
\ 5/a
\ 6 ???
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6 …)) /2/
309 @
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"
\ 6one
\ 5/a
\ 6 /2/