--- /dev/null
+(*
+\ 5h1\ 6Matita Interactive Tutorial\ 5/h1\ 6
+\ 5b\ 6The goat, the wolf and the cabbage\ 5/b\ 6
+A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
+is only one place available on his boat. Furthermore, the goat will eat the
+cabbage if they are left alone on the same bank, and similarly the wolf will eat
+the goat. The problem consists in bringing all three items safely across the
+river.
+
+Our first data type defines the two banks of the river, which will be named east
+and west. It is a simple example of enumerated type, defined by explicitly
+declaring all its elements. The type itself is called "bank".
+Before giving its definition we "include" the file "logic.ma" that contains a
+few preliminary notions not worth discussing for the moment.
+*)
+
+include "basics/logic.ma".
+
+inductive bank: Type[0] ≝
+| east : bank
+| west : bank.
+
+(* We can now define a simple function computing, for each bank of the river, the
+opposite one. *)
+
+definition opposite ≝ λs.
+match s with
+ [ east ⇒ west
+ | west ⇒ east
+ ].
+
+(* The goal window. Computation. *)
+lemma east_to_west : opposite east = west.
+normalize
+// qed.
+
+(* the computation step is not necessary *)
+lemma west_to_east : opposite west = east.
+// qed.
+
+(* A slightly more complex problem consists in proving that opposite is idempotent *)
+lemma idempotent_opposite : ∀x. opposite (opposite x) = x.
+#b
+cases b
+// qed.
+
+(*
+\ 5h2 class="section"\ 6Predicates\ 5/h2\ 6
+Instead of working with functions, it is sometimes convenient to work with
+predicates. For instance, instead of defining a function computing the opposite
+bank, we could declare a predicate stating when two banks are opposite to each
+other. Only two cases are possible, leading naturally to the following
+definition:
+*)
+
+inductive opp : bank → bank → Prop ≝
+| east_west : opp east west
+| west_east : opp west east.
+
+(* In precisely the same way as "bank" is the smallest type containing east and
+west, opp is the smallest predicate containing the two sub-cases east_west and
+weast_east. If you have some familiarity with Prolog, you may look at opp as the
+predicate defined by the two clauses - in this case, the two facts - ast_west and
+west_east.
+
+Between opp and opposite we have the following relation:
+ opp a b iff a = opposite b
+Let us prove it, starting from the left to right implication, first *)
+
+lemma opp_to_opposite: ∀a,b. opp a b → a = opposite b.
+#a #b #oppab
+cases oppab // qed.
+
+(*
+\ 5h2 class="section"\ 6Rewriting\ 5/h2\ 6
+Let us come to the opposite direction. *)
+
+lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b.
+#a #b #eqa
+>eqa
+cases b // qed.
+
+(*
+\ 5h2 class="section"\ 6Records\ 5/h2\ 6
+It is time to proceed with our formalization of the farmer's problem.
+A state of the system is defined by the position of four items: the goat, the
+wolf, the cabbage, and the boat. The simplest way to declare such a data type
+is to use a record.
+*)
+
+record state : Type[0] ≝
+ {goat_pos : bank;
+ wolf_pos : bank;
+ cabbage_pos: bank;
+ boat_pos : bank}.
+
+(* When you define a record named foo, the system automatically defines a record
+constructor named mk_foo. To construct a new record you pass as arguments to
+mk_foo the values of the record fields *)
+
+definition start ≝ mk_state east east east east.
+definition end ≝ mk_state west west west west.
+
+(* We must now define the possible moves. A natural way to do it is in the form
+of a relation (a binary predicate) over states.
+
+ g ⊥ g1
+ ----------------------- (move_goat)
+ (g,w,c,g) ↦ (g1,w,c,g1)
+
+ w ⊥ w1
+ ----------------------- (move_wolf)
+ (g,w,c,w) ↦ (g,w1,c,w1)
+
+ c ⊥ c1
+ ----------------------- (move_cabbage)
+ (g,w,c,c) ↦ (g,w,c1,c1)
+
+ b ⊥ b1
+ ---------------------- (move_boat)
+ (g,w,c,b) ↦ (g,w,c,b1)
+
+*)
+
+inductive move : state → state → Prop ≝
+| move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1)
+ (* We can move the goat from a bank g to the opposite bank g1 if and only if the
+ boat is on the same bank g of the goat and we move the boat along with it. *)
+| move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
+| move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
+| move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).
+
+(* A state is safe if either the goat is on the same bank of the boat, or both
+the wolf and the cabbage are on the opposite bank of the goat. *)
+
+inductive safe_state : state → Prop ≝
+| with_boat : ∀g,w,c.safe_state (mk_state g w c g)
+| opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b).
+
+(* Finally, a state y is reachable from x if either there is a single move
+leading from x to y, or there is a safe state z such that z is reachable from x
+and there is a move leading from z to y *)
+
+inductive reachable : state → state → Prop ≝
+| one : ∀x,y.move x y → reachable x y
+| more : ∀x,z,y. \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6reachable x z → safe_state z → \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6move z y → reachable x y.
+
+(*
+\ 5h2 class="section"\ 6Automation\ 5/h2\ 6
+Remarkably, Matita is now able to solve the problem by itself, provided
+you allow automation to exploit more resources. The command /n/ is similar to
+//, where n is a measure of this complexity: in particular it is a bound to
+the depth of the expected proof tree (more precisely, to the number of nested
+applicative nodes). In this case, there is a solution in six moves, and we
+need a few more applications to handle reachability, and side conditions.
+The magic number to let automation work is, in this case, 9. *)
+
+lemma problem: reachable start end.
+normalize /9/ qed.
+
+(*
+\ 5h2 class="section"\ 6A complex interactive proof\ 5/h2\ 6
+Let us now try to derive the proof in a more interactive way. Of course, we
+expect to need several moves to transfer all items from a bank to the other, so
+we should start our proof by applying "more". Matita syntax for invoking the
+application of a property named foo is to write "@foo". In general, the philosophy
+of Matita is to describe each proof of a property P as a structured collection of
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining
+the way it is actually used (e.g. for introduction, rewriting, in an applicative
+step, and so on).
+
+- tinycals
+- implicit arguments
+*)
+
+lemma problem1: reachable start end.
+normalize @more
+(*
+ - multiple conjectures
+ - tinycals
+ *)
+ [ @(mk_state east west west east)
+ || //
+ | /2/ ]
+
+(* implicit arguments *)
+@(more ? (mk_state east west west west))
+/2/
+
+(* vectors of implicit arguments *)
+@(more … (move_wolf … ))
+
+(* focusing *)
+[4: @east] /2/
+
+(* Alternatively, we can directly instantiate the bank into the move. Let
+us complete the proof in this, very readable way. *)
+@(more … (move_goat west … )) /2/
+@(more … (move_cabbage ?? east … )) /2/
+@(more … (move_boat ??? west … )) /2/
+@one /2/ qed.
\ No newline at end of file
projects / helm.git / blobdiff