]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/tutorial/chapter1.ma
A compiling version
[helm.git] / matita / matita / lib / tutorial / chapter1.ma
1 (****************** Data types, functions and theorems ************************)
2
3 (* Matita is both a programming language and a theorem proving environment: you 
4 define datatypes and programs, and then prove properties on them.
5 Very few things are built-in: not even booleans or logical connectives (but you 
6 may of course use libraries, as in normal programming languages). 
7 The main philosophy of the system is to let you define your own data-types and 
8 functions using a powerful computational mechanism based on the declaration of 
9 inductive types. 
10
11 Let us start this tutorial with a simple example based on the following well 
12 known problem: the goat, the wolf and the cabbage.
13
14 A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
15 is only one place available on his boat. Furthermore, the goat will eat the 
16 cabbage if they are left alone on the same bank, and similarly the wolf will eat
17 the goat. The problem consists in bringing all three items safely across the 
18 river. 
19
20 Our first data type defines the two banks of the river, which will be named east
21 and west. It is a simple example of enumerated type, defined by explicitly 
22 declaring all its elements. The type itself is called "bank".
23 Before giving its definition we "include" the file "logic.ma" that contains a 
24 few preliminary notions not worth discussing for the moment.
25 *)
26
27 include "basics/logic.ma".
28
29 inductive bank: Type[0] ≝ 
30 | east : bank 
31 | west : bank.
32
33 (* The definition starts with the keyword "inductive" followed by the name we 
34 want to give to the new datatype (in this case, "bank"), followed by its type (a
35 type of a type is traditionally called a "sort" in type theory). We have 
36 basically two sorts in Matita: "Prop" and "Type". "Prop" is meant for logical 
37 propositions, while "Type" should be used for dataypes (we shall tell more about 
38 the attribute $0$ in a later Section).
39
40 The definition proceeds with the keyword ``:='' (or "\def") followed by the 
41 "body" of the definition. The body is just a list of "constructors" for the 
42 inductive type, separated by the keyword | (vertical bar). Each constructor is a
43 pair composed by a name and its type. Constructors (in our case, "east" and 
44 "west") are the "canonical inhabitants" of the inductive type we are defining 
45 (in our case, "bank"), hence their type must be of type "bank". 
46 In general, as we shall see, constructors for an inductive type T may have a 
47 more complex structure, and in particular can be recursive: the general proviso 
48 is that they must always "return" a result of type T. 
49 Hence, the declaration of a constructor c for and inductive type T has the 
50 following typical shape: 
51                       A1 → …  → An → T
52 where A1 … A_n can be arbitrary types, comprising T itself. Not every form of 
53 recursive constructors is accepted however: in order to ensure logical 
54 consistency, we must respect some positivity conditions, that we shall discuss 
55 in Section ??. 
56
57 As a general rule, the inductive type must be conceptually understood as the 
58 smallest collection of terms freely generated by its constructors. *)
59
60 (********************************* functions **********************************) 
61
62 (* We define a first simple function computing, for each bank of the river, the
63 opposite one. *)
64
65 definition opposite ≝ λs.
66 match s with
67   [ east ⇒ west
68   | west ⇒ east
69   ].
70
71 (* Non recursive functions must be defined in Matita using the keyword 
72 "definition" followed by the name of the function. The type of the function is 
73 optional, since in many cases it can be automatically inferred by the system. 
74 The definition proceeds with the keyword ``:='' followed by the function body. 
75 The body starts with a list of "input parameters", preceded by the symbol λ 
76 (\lambda); many latex-like macro are automatically converted by Matita into 
77 Unicode symbols: see \verb+View >Tex\UTF-8 table+ in the menu bar for a complete 
78 list.
79
80 The definition proceeds by "pattern matching" on the parameter s: if the input 
81 bank is east we return west, and conversely if it is west we return east.
82
83 Pattern matching is a well known feature typical of functional programming 
84 (especially of the ML family), allowing simple access to the components of 
85 complex data structures. A function definition most often corresponds to pattern 
86 matching over one or more of its parameters, allowing the function to be easily 
87 defined by cases.
88
89 The syntactic structure of a match expression is the following:
90
91 match expr with
92   [ p1 => expr1
93   | p2 => expr1
94   :
95   | pn => exprn
96   ]
97
98 The expression expr, that is supposed to be an element of an inductive type T, 
99 is matched sequentially to the various patterns p1, ..., pn. A pattern pi is 
100 just a constructor of the inductive type T possibly applied to a list of 
101 variables, bound inside the corresponding branch expri. 
102 If the pattern pi matches the value expr, then the corresponding branch expri is 
103 evaluated (after replacing in it the pattern variables with the corresponding 
104 subterms of expr).
105 Usually, all expressions expr have a same, uniform type; since however Matita 
106 supports dependent types, the type of branches could depend on the matched 
107 expression, too. *)
108
109 (******************************* A first lemma ********************************)
110
111 (* Functions are live entities, and can be actually computed. To check this, let
112 us state the property that the opposite bank of east is west; every lemma needs 
113 a name for further reference, and we call it "east_to_west". *)
114  
115 lemma east_to_west : opposite east = west.
116
117 (* 
118 The goal window
119
120 If you stop the execution here you will see a new window on the  right side
121 of the screen: it is the goal window, providing a sequent like representation of
122 the form
123
124 B1
125 B2
126 ....
127 Bk
128 -----------------------
129 A
130
131 for each open goal remaining to be solved. A is the conclusion of the goal and 
132 B1, ..., Bk is its context, that is the set of current hypothesis and type 
133 declarations. In this case, we have only one goal, and its context is empty. 
134 The proof proceeds by typing commands to the system. In this case, we
135 want to evaluate the function, that can be done by invoking the  "normalize"
136 command:
137 *)
138
139 normalize
140
141 (* By executing it - just type the advance command - you will see that the goal
142 has changed to west = west, by reducing the subexpression (opposite east). 
143 You may use the retract bottom to undo the step, if you wish. 
144
145 The new goal west = west is trivial: it is just a consequence of reflexivity.
146 Such trivial steps can be just closed in Matita by typing a double slash. 
147 We complete the proof by the qed command, that instructs the system to store the
148 lemma performing some book-keeping operations. 
149 *)
150
151 // qed.
152
153 (* In exactly the same way, we can prove that the opposite side of west is east.
154 In this case, we avoid the unnecessary simplification step: // will take care of 
155 it. *) 
156
157 lemma west_to_east: opposite west = east.
158 // qed.
159
160 (* Instead of "lemma", you may also use "theorem" or "corollary". Matita does 
161 not attempt to make a semantic distinction between them, and their use is 
162 entirely up to the user. *)
163
164 (********************************* Introduction *******************************)
165
166 (* A slightly more complex problem consists in proving that opposite is 
167 idempotent *)
168
169 lemma idempotent_opposite : ∀x. opposite (opposite x) = x.
170
171 (* we start the proof moving x from the conclusion into the context, that is a 
172 (backward) introduction step. Matita syntax for an introduction step is simply 
173 the sharp character followed by the name of the item to be moved into the 
174 context. This also allows us to rename the item, if needed: for instance if we 
175 wish to rename x into b (since it is a bank), we just type #b. *)
176
177 #b
178
179 (* See the effect of the execution in the goal window on the right: b has been 
180 added to the context (replacing x in the conclusion); moreover its implicit type 
181 "bank" has been made explicit. 
182 *)
183
184 (*
185 Case analysis
186
187 But how are we supposed to proceed, now? Simplification cannot help us, since b
188 is a variable: just try to call normalize and you will see that it has no effect.
189 The point is that we must proceed by cases according to the possible values of b,
190 namely east and west. To this aim, you must invoke the cases command, followed by
191 the name of the hypothesis (more generally, an arbitrary expression) that must be
192 the object of the case analysis (in our case, b).
193 *)
194
195 cases b 
196
197 (* Executing the previous command has the effect of opening two subgoals, 
198 corresponding to the two cases b=east and b=west: you may switch from one to the 
199 other by using the hyperlinks over the top of the goal window. 
200 Both goals can be closed by trivial computations, so we may use // as usual.
201 If we had to treat each subgoal in a different way, we should focus on each of 
202 them in turn, in a way that will be described at the end of this section.
203 *)
204
205 // qed.
206
207 (********************************** Predicates ********************************)
208
209 (* Instead of working with functions, it is sometimes convenient to work with
210 predicates. For instance, instead of defining a function computing the opposite 
211 bank, we could declare a predicate stating when two banks are opposite to each 
212 other. Only two cases are possible, leading naturally to the following 
213 definition:
214 *)
215
216 inductive opp : bank → bank → Prop ≝ 
217 | east_west : opp east west
218 | west_east : opp west east.
219
220 (* In precisely the same way as "bank" is the smallest type containing east and
221 west, opp is the smallest predicate containing the two sub-cases east_west and
222 weast_east. If you have some familiarity with Prolog, you may look at opp as the
223 predicate defined by the two clauses - in this case, the two facts - ast_west 
224 and west_east.
225
226 Between opp and opposite we have the following relation:
227     opp a b iff a = opposite b
228 Let us prove it, starting from the left to right implication, first *)
229
230 lemma opp_to_opposite: ∀a,b. opp a b → a = opposite b.
231  
232 (* We start the proof introducing a, b and the hypothesis opp a b, that we
233 call oppab. *)
234 #a #b #oppab
235
236 (* Now we proceed by cases on the possible proofs of (opp a b), that is on the 
237 possible shapes of oppab. By definition, there are only two possibilities, 
238 namely east_west or west_east. Both subcases are trivial, and can be closed by
239 automation *)
240
241 cases oppab // qed.
242
243 (******************************** Rewriting ***********************************)
244
245 (* Let us come to the opposite direction. *)
246
247 lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b.
248
249 (* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
250 that we call eqa. *)
251
252 #a #b #eqa
253
254 (* The right way to proceed, now, is by rewriting a into (opposite b). We do
255 this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
256 opposite b into a, we would have typed "<eqa". *)
257
258 >eqa
259
260 (* We conclude the proof by cases on b. *)
261
262 cases b // qed.
263
264 (******************************** Records *************************************)
265
266 (* It is time to proceed with our formalization of the farmer's problem. 
267 A state of the system is defined by the position of four items: the goat, the 
268 wolf, the cabbage, and the boat. The simplest way to declare such a data type
269 is to use a record.
270 *)
271
272 record state : Type[0] ≝
273   {goat_pos : bank;
274    wolf_pos : bank;
275    cabbage_pos: bank;
276    boat_pos : bank}.
277
278 (* When you define a record named foo, the system automatically defines a record 
279 constructor named mk_foo. To construct a new record you pass as arguments to 
280 mk_foo the values of the record fields *)
281
282 definition start ≝ mk_state east east east east.
283 definition end ≝ mk_state west west west west.
284
285 (* We must now define the possible moves. A natural way to do it is in the form 
286 of a relation (a binary predicate) over states. *)
287
288 inductive move : state → state → Prop ≝
289 | move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1)
290   (* We can move the goat from a bank g to the opposite bank g1 if and only if the
291      boat is on the same bank g of the goat and we move the boat along with it. *)
292 | move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
293 | move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
294 | move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).
295
296 (* A state is safe if either the goat is on the same bank of the boat, or both 
297 the wolf and the cabbage are on the opposite bank of the goat. *)
298
299 inductive safe_state : state → Prop ≝
300 | with_boat : ∀g,w,c.safe_state (mk_state g w c g)
301 | opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b).
302
303 (* Finally, a state y is reachable from x if either there is a single move 
304 leading from x to y, or there is a safe state z such that z is reachable from x 
305 and there is a move leading from z to y *)
306
307 inductive reachable : state → state → Prop ≝
308 | one : ∀x,y.move x y → reachable x y
309 | more : ∀x,z,y. reachable x z → safe_state z → move z y → reachable x y.
310
311 (********************************* Automation *********************************)
312
313 (* Remarkably, Matita is now able to solve the problem by itslef, provided you 
314 allow automation to exploit more resources. The command /n/ is similar to //, 
315 where n is a measure of this complexity: in particular it is a bound to the 
316 depth of the expected proof tree (more precisely, to the number of nested
317 applicative nodes). In this case, there is a solution in six moves, and we need 
318 a few more applications to handle reachability, and side conditions. 
319 The magic number to let automation work is, in this case, 9.  *)
320
321 lemma problem: reachable start end.
322 normalize /9/ qed.
323
324 (********************************* Application ********************************)
325
326 (* Let us now try to derive the proof in a more interactive way. Of course, we
327 expect to need several moves to transfer all items from a bank to the other, so 
328 we should start our proof by applying "more". Matita syntax for invoking the 
329 application of a property named foo is to write "@foo". In general, the 
330 philosophy of Matita is to describe each proof of a property P as a structured 
331 collection of objects involved in the proof, prefixed by simple modalities (#,<,
332 @,...) explaining the way it is actually used (e.g. for introduction, rewriting, 
333 in an applicative step, and so on).
334 *)
335
336 lemma problem1: reachable start end.
337 normalize @more
338
339 (********************************* Focusing ***********************************)
340
341 (* After performing the previous application, we have four open subgoals:
342
343   X : STATE
344   Y : reachable [east,east,east,east] X
345   W : safe_state X
346   Z : move X [west,west,west,west]
347  
348 That is, we must guess a state X, such that this is reachable from start, it is 
349 safe, and there is a move leading from X to end. All goals are active, that is
350 emphasized by the fact that they are all red. Any command typed by the user is
351 normally applied in parallel to all active goals, but clearly we must proceed 
352 here is a different way for each of them. The way to do it, is by structuring
353 the script using the following syntax: [...|... |...|...] where we typically have
354 as many cells inside the brackets as the number of the active subgoals. The
355 interesting point is that we can associate with the three symbol "[", "|" and
356 "]" a small-step semantics that allow to execute them individually. In particular
357
358 - the operator "[" opens a new focusing section for the currently active goals,
359   and focus on the first of them
360 - the operator "|" shift the focus to the next goal
361 - the operator "]" close the focusing section, falling back to the previous level
362   and adding to it all remaining goals not yet closed
363
364 Let us see the effect of the "[" on our proof:
365 *)
366
367   [
368   
369 (* As you see, only the first goal has now the focus on. Moreover, all goals got
370 a progressive numerical label, to help designating them, if needed. 
371 We can now proceed in several possible ways. The most straightforward way is to 
372 provide the intermediate state, that is [east,west,west,east]. We can do it, by 
373 just applying this term. *)
374
375    @(mk_state east west west east) 
376
377 (* This application closes the goal; at present, no goal has the focus on.
378 In order to act on the next goal, we must focus on it using the "|" operator. In
379 this case, we would like to skip the next goal, and focus on the trivial third 
380 subgoal: a simple way to do it, is by retyping "|". The proof that 
381 [east,west,west,east] is safe is trivial and can be done with //.*)
382
383   || //
384
385 (*
386 We then advance to the next goal, namely the fact that there is a move from 
387 [east,west,west,east] to [west,west,west,west]; this is trivial too, but it 
388 requires /2/ since move_goat opens an additional subgoal. By applying "]" we
389 refocus on the skipped goal, going back to a situation similar to the one we
390 started with. *)
391
392   | /2/ ] 
393
394 (************************** Implicit arguments ********************************)
395
396 (* Let us perform the next step, namely moving back the boat, in a sligtly 
397 different way. The more operation expects as second argument the new 
398 intermediate state, hence instead of applying more we can apply this term
399 already instatated on the next intermediate state. As first argument, we type a 
400 question mark that stands for an implicit argument to be guessed by the system.
401 *)
402
403 @(more ? (mk_state east west west west))
404
405 (* We now get three independent subgoals, all actives, and two of them are 
406 trivial. We can just apply automation to all of them, and it will close the two
407 trivial goals. *)
408
409 /2/
410
411 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
412 instead of specifying the next intermediate state, we prefer to specify the next 
413 move. In the spirit of the previous example, we can do it in the following way 
414 *)
415
416 @(more … (move_wolf … ))
417
418 (* The dots stand here for an arbitrary number of implicit arguments, to be 
419 guessed by the system. 
420 Unfortunately, the previous move is not enough to fully instantiate the new 
421 intermediate state: a bank B remains unknown. Automation cannot help here,
422 since all goals depend from this bank and automation refuses to close some
423 subgoals instantiating other subgoals remaining open (the instantiation could
424 be arbitrary). The simplest way to proceed is to focus on the bank, that is
425 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
426 we can perform focusing by typing "4:" as described by the following command. *)
427
428 [4: @east] /2/
429
430 (* Alternatively, we can directly instantiate the bank into the move. Let
431 us complete the proof in this, very readable way. *)
432
433 @(more … (move_goat west … )) /2/
434 @(more … (move_cabbage ?? east … )) /2/
435 @(more … (move_boat ??? west … )) /2/
436 @one /2/ qed.