2 \ 5h1
\ 6Matita Interactive Tutorial
\ 5/h1
\ 6
3 This is an interactive tutorial. To let you interact on line with the system,
4 you must first of all register yourself.
6 Before starting, let us briefly explain the meaning of the menu buttons.
7 With the Advance and Retract buttons you respectively perform and undo single
8 computational steps. Each step consists in reading a user command, and processing
9 it. The part of the user input file (called script) already executed by the
10 system will be colored, and will not be editable any more. The advance bottom
11 will also automatically advance the focus of the window, but you can inspect the
12 whole file using the scroll bars, as usual. Comments are skipped.
13 Try to advance and retract a few steps, to get the feeling of the system. You can
14 also come back here by using the top button, that takes you at the beginning of
15 a file. The play button is meant to process the script up to a position
16 previously selected by the user; the bottom button execute the whole script.
17 That's it: we are
\ 5span style="font-family: Verdana,sans-serif;"
\ 6 \ 5/span
\ 6now ready to start.
19 \ 5h2 class="section"
\ 6Data types, functions and theorems
\ 5/h2
\ 6
20 Matita is both a programming language and a theorem proving environment:
21 you define datatypes and programs, and then prove properties on them.
22 Very few things are built-in: not even booleans or logical connectives
23 (but you may of course use libraries, as in normal programming languages).
24 The main philosophy of the system is to let you define your own data-types
25 and functions using a powerful computational mechanism based on the
26 declaration of inductive types.
28 Let us start this tutorial with a simple example based on the following well
31 \ 5b
\ 6The goat, the wolf and the cabbage
\ 5/b
\ 6
32 A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
33 is only one place available on his boat. Furthermore, the goat will eat the
34 cabbage if they are left alone on the same bank, and similarly the wolf will eat
35 the goat. The problem consists in bringing all three items safely across the
38 Our first data type defines the two banks of the river, which will be named east
39 and west. It is a simple example of enumerated type, defined by explicitly
40 declaring all its elements. The type itself is called "bank".
41 Before giving its definition we "include" the file "logic.ma" that contains a
42 few preliminary notions not worth discussing for the moment.
45 include "basics/logic.ma".
47 inductive bank: Type[0] ≝
51 (* We can now define a simple function computing, for each bank of the river, the
54 definition opposite ≝ λs.
56 [ east ⇒
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"
\ 6west
\ 5/a
\ 6
57 | west ⇒
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6
60 (* Functions are live entities, and can be actually computed. To check this, let
61 us state the property that the opposite bank of east is west; every lemma needs a
62 name for further reference, and we call it "east_to_west". *)
64 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.
66 (* If you stop the execution here you will see a new window on the right side
67 of the screen: it is the goal window, providing a sequent like representation of
74 -----------------------
77 for each open goal remaining to be solved. A is the conclusion of the goal and
78 B1, ..., Bk is its context, that is the set of current hypothesis and type
79 declarations. In this case, we have only one goal, and its context is empty.
80 The proof proceeds by typing commands to the system. In this case, we
81 want to evaluate the function, that can be done by invoking the "normalize"
87 (* By executing it - just type the advance command - you will see that the goal
88 has changed to west = west, by reducing the subexpression (opposite east).
89 You may use the retract bottom to undo the step, if you wish.
91 The new goal west = west is trivial: it is just a consequence of reflexivity.
92 Such trivial steps can be just closed in Matita by typing a double slash.
93 We complete the proof by the qed command, that instructs the system to store the
94 lemma performing some book-keeping operations.
99 (* In exactly the same way, we can prove that the opposite side of west is east.
100 In this case, we avoid the unnecessary simplification step: // will take care of
103 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.
107 \ 5h2 class="section"
\ 6Case analysis
\ 5/h2
\ 6
108 A slightly more complex problem consists in proving that opposite is idempotent *)
110 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.
112 (* we start the proof moving x from the conclusion into the context, that is a
113 (backward) introduction step. Matita syntax for an introduction step is simply
114 the sharp character followed by the name of the item to be moved into the
115 context. This also allows us to rename the item, if needed: for instance if we
116 wish to rename x into b (since it is a bank), we just type #b. *)
120 (* See the effect of the execution in the goal window on the right: b has been
121 added to the context (replacing x in the conclusion); moreover its implicit type
122 "bank" has been made explicit.
124 But how are we supposed to proceed, now? Simplification cannot help us, since b
125 is a variable: just try to call normalize and you will see that it has no effect.
126 The point is that we must proceed by cases according to the possible values of b,
127 namely east and west. To this aim, you must invoke the cases command, followed by
128 the name of the hypothesis (more generally, an arbitrary expression) that must be
129 the object of the case analysis (in our case, b).
134 (* Executing the previous command has the effect of opening two subgoals,
135 corresponding to the two cases b=east and b=west: you may switch from one to the
136 other by using the hyperlinks over the top of the goal window.
137 Both goals can be closed by trivial computations, so we may use // as usual.
138 If we had to treat each subgoal in a different way, we should focus on each of
139 them in turn, in a way that will be described at the end of this section.
145 \ 5h2 class="section"
\ 6Predicates
\ 5/h2
\ 6
146 Instead of working with functions, it is sometimes convenient to work with
147 predicates. For instance, instead of defining a function computing the opposite
148 bank, we could declare a predicate stating when two banks are opposite to each
149 other. Only two cases are possible, leading naturally to the following
153 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 ≝
154 | 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
155 | 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.
157 (* In precisely the same way as "bank" is the smallest type containing east and
158 west, opp is the smallest predicate containing the two sub-cases east_west and
159 weast_east. If you have some familiarity with Prolog, you may look at opp as the
160 predicate defined by the two clauses - in this case, the two facts - ast_west and
163 Between opp and opposite we have the following relation:
164 opp a b iff a = opposite b
165 Let us prove it, starting from the left to right implication, first *)
167 lemma opp_to_opposite: ∀a,b.
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 a b → a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 b.
169 (* We start the proof introducing a, b and the hypothesis opp a b, that we
173 (* Now we proceed by cases on the possible proofs of (opp a b), that is on the
174 possible shapes of oppab. By definition, there are only two possibilities,
175 namely east_west or west_east. Both subcases are trivial, and can be closed by
181 \ 5h2 class="section"
\ 6Rewriting
\ 5/h2
\ 6
182 Let us come to the opposite direction. *)
184 lemma opposite_to_opp: ∀a,b. a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"
\ 6opposite
\ 5/a
\ 6 b →
\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"
\ 6opp
\ 5/a
\ 6 a b.
186 (* As usual, we start introducing a, b and the hypothesis (a = opposite b),
191 (* The right way to proceed, now, is by rewriting a into (opposite b). We do
192 this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
193 opposite b into a, we would have typed "<eqa". *)
197 (* We conclude the proof by cases on b. *)
202 \ 5h2 class="section"
\ 6Records
\ 5/h2
\ 6
203 It is time to proceed with our formalization of the farmer's problem.
204 A state of the system is defined by the position of four item: the goat, the
205 wolf, the cabbage, and the boat. The simplest way to declare such a data type
209 record state : Type[0] ≝
210 {goat_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
211 wolf_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
212 cabbage_pos:
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6;
213 boat_pos :
\ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"
\ 6bank
\ 5/a
\ 6}.
215 (* When you define a record named foo, the system automatically defines a record
216 constructor named mk_foo. To construct a new record you pass as arguments to
217 mk_foo the values of the record fields *)
219 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.
220 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.
222 (* We must now define the possible moves. A natural way to do it is in the form
223 of a relation (a binary predicate) over states. *)
225 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 ≝
226 | 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)
227 (* We can move the goat from a bank g to the opposite bank g1 if and only if the
228 boat is on the same bank g of the goat and we move the boat along with it. *)
229 | 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)
230 | 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)
231 | 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).
233 (* A state is safe if either the goat is on the same bank of the boat, or both
234 the wolf and the cabbage are on the opposite bank of the goat. *)
236 inductive safe_state :
\ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
\ 6state
\ 5/a
\ 6 → Prop ≝
237 | 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)
238 | 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).
240 (* Finally, a state y is reachable from x if either there is a single move
241 leading from x to y, or there is a safe state z such that z is reachable from x
242 and there is a move leading from z to y *)
244 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 ≝
245 | one : ∀x,y.
\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"
\ 6move
\ 5/a
\ 6 x y → reachable x y
246 | 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.
249 \ 5h2 class="section"
\ 6Automation
\ 5/h2
\ 6
250 Remarkably, Matita is now able to solve the problem by itslef, provided
251 you allow automation to exploit more resources. The command /n/ is similar to
252 //, where n is a measure of this complexity: in particular it is a bound to
253 the depth of the expected proof tree (more precisely, to the number of nested
254 applicative nodes). In this case, there is a solution in six moves, and we
255 need a few more applications to handle reachability, and side conditions.
256 The magic number to let automation work is, in this case, 9. *)
258 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.
259 normalize /
\ 5span class="autotactic"
\ 69
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"
\ 6one
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"
\ 6with_boat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"
\ 6opposite_side
\ 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/move.con(0,2,0)"
\ 6move_wolf
\ 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/move.con(0,4,0)"
\ 6move_boat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"
\ 6west_east
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
262 \ 5h2 class="section"
\ 6Application
\ 5/h2
\ 6
263 Let us now try to derive the proof in a more interactive way. Of course, we
264 expect to need several moves to transfer all items from a bank to the other, so
265 we should start our proof by applying "more". Matita syntax for invoking the
266 application of a property named foo is to write "@foo". In general, the philosophy
267 of Matita is to describe each proof of a property P as a structured collection of
268 results required for proving P, prefixed by simple modalities (<,@,...) explaining
269 the way the result is used (e.g. for rewriting, in an applicative step, and so on).
272 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.
273 normalize @
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"
\ 6more
\ 5/a
\ 6
276 \ 5h2 class="section"
\ 6Focusing
\ 5/h2
\ 6
277 After performing the previous application, we have four open subgoals:
280 Y : reachable [east,east,east,east] X
282 Z : move X [west,west,west,west]
284 That is, we must guess a state X, such that this is reachable from start, it is
285 safe, and there is a move leading from X to end. All goals are active, that is
286 emphasized by the fact that they are all red. Any command typed by the user is
287 normally applied in parallel to all active goals, but clearly we must proceed
288 here is a different way for each of them. The way to do it, is by structuring
289 the script using the following syntax: [...|... |...|...] where we typically have
290 as many cells inside the brackets as the number of the active subgoals. The
291 interesting point is that we can associate with the three symbol "[", "|" and
292 "]" a small-step semantics that allow to execute them individually. In particular
294 - the operator "[" opens a new focusing section for the currently active goals,
295 and focus on the first of them
296 - the operator "|" shift the focus to the next goal
297 - the operator "]" close the focusing section, falling back to the previous level
298 and adding to it all remaining goals not yet closed
300 Let us see the effect of the "[" on our proof:
305 (* As you see, only the first goal has now the focus on. Moreover, all goals got
306 a progressive numerical label, to help designating them, if needed.
307 We can now proceed in several possible ways. The most straightforward way is to
308 provide the intermediate state, that is [east,west,west,east]. We can do it, by
309 just applying this term. *)
311 @(
\ 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)
313 (* This application closes the goal; at present, no goal has the focus on.
314 In order to act on the next goal, we must focus on it using the "|" operator. In
315 this case, we would like to skip the next goal, and focus on the trivial third
316 subgoal: a simple way to do it, is by retyping "|". The proof that
317 [east,west,west,east] is safe is trivial and can be done with //.*)
322 We then advance to the next goal, namely the fact that there is a move from
323 [east,west,west,east] to [west,west,west,west]; this is trivial too, but it
324 requires /2/ since move_goat opens an additional subgoal. By applying "]" we
325 refocus on the skipped goal, going back to a situation similar to the one we
328 | /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"
\ 6move_goat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ ]
331 \ 5h2 class="section"
\ 6Implicit arguments
\ 5/h2
\ 6
332 Let us perform the next step, namely moving back the boat, in a sligtly
333 different way. The more operation expects as second argument the new
334 intermediate state, hence instead of applying more we can apply this term
335 already instatated on the next intermediate state. As first argument, we
336 type a question mark that stands for an implicit argument to be guessed by
339 @(
\ 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))
341 (* We now get three independent subgoals, all actives, and two of them are
342 trivial. We
\ 5span style="font-family: Verdana,sans-serif;"
\ 6 \ 5/span
\ 6can just apply automation to all of them, and it will close the two
345 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"
\ 6opposite_side
\ 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/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"
\ 6west_east
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
347 (* Let us come to the next step, that consists in moving the wolf. Suppose that
348 instead of specifying the next intermediate state, we prefer to specify the next
349 move. In the spirit of the previous example, we can do it in the following way
352 @(
\ 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 … ))
354 (* The dots stand here for an arbitrary number of implicit arguments, to be
355 guessed by the system.
356 Unfortunately, the previous move is not enough to fully instantiate the new
357 intermediate state: a bank B remains unknown. Automation cannot help here,
358 since all goals depend from this bank and automation refuses to close some
359 subgoals instantiating other subgoals remaining open (the instantiation could
360 be arbitrary). The simplest way to proceed is to focus on the bank, that is
361 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
362 we can perform focusing by typing "4:" as described by the following command. *)
364 [4: @
\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"
\ 6east
\ 5/a
\ 6] /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"
\ 6with_boat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
366 (* Alternatively, we can directly instantiate the bank into the move. Let
367 us complete the proof in this, very readable way. *)
369 @(
\ 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 … )) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"
\ 6with_boat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"
\ 6west_east
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
370 @(
\ 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 … )) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"
\ 6opposite_side
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"
\ 6west_east
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
371 @(
\ 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 … )) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"
\ 6with_boat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"
\ 6west_east
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
372 @
\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"
\ 6one
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"
\ 6move_goat
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"
\ 6east_west
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.