weblib/cicm2012/part1.ma

   1 (*
   2 \ 5h1\ 6Matita Interactive Tutorial\ 5/h1\ 6
   3 \ 5b\ 6The goat, the wolf and the cabbage\ 5/b\ 6
   4 A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
   5 is only one place available on his boat. Furthermore, the goat will eat the
   6 cabbage if they are left alone on the same bank, and similarly the wolf will eat
   7 the goat. The problem consists in bringing all three items safely across the
   8 river.
   9
  10 Our first data type defines the two banks of the river, which will be named east
  11 and west. It is a simple example of enumerated type, defined by explicitly
  12 declaring all its elements. The type itself is called "bank".
  13 Before giving its definition we "include" the file "logic.ma" that contains a
  14 few preliminary notions not worth discussing for the moment.
  15 *)
  16
  17 include "basics/logic.ma".
  18
  19 inductive bank: Type[0] ≝
  20 | east : bank
  21 | west : bank.
  22
  23 (* We can now define a simple function computing, for each bank of the river, the
  24 opposite one. *)
  25
  26 definition opposite ≝ λs.
  27 match s with
  28   [ east ⇒ west
  29   | west ⇒ east
  30   ].
  31
  32 (* The goal window. Computation. *)
  33 lemma east_to_west : opposite east = west.
  34 normalize
  35 // qed.
  36
  37 (* the computation step is not necessary *)
  38 lemma west_to_east : opposite west = east.
  39 // qed.
  40
  41 (* A slightly more complex problem consists in proving that opposite is idempotent *)
  42 lemma idempotent_opposite : ∀x. opposite (opposite x) = x.
  43 #b
  44 cases b
  45 // qed.
  46
  47 (*
  48 \ 5h2 class="section"\ 6Predicates\ 5/h2\ 6
  49 Instead of working with functions, it is sometimes convenient to work with
  50 predicates. For instance, instead of defining a function computing the opposite
  51 bank, we could declare a predicate stating when two banks are opposite to each
  52 other. Only two cases are possible, leading naturally to the following
  53 definition:
  54 *)
  55
  56 inductive opp : bank → bank → Prop ≝
  57 | east_west : opp east west
  58 | west_east : opp west east.
  59
  60 (* In precisely the same way as "bank" is the smallest type containing east and
  61 west, opp is the smallest predicate containing the two sub-cases east_west and
  62 weast_east. If you have some familiarity with Prolog, you may look at opp as the
  63 predicate defined by the two clauses - in this case, the two facts - ast_west and
  64 west_east.
  65
  66 Between opp and opposite we have the following relation:
  67     opp a b iff a = opposite b
  68 Let us prove it, starting from the left to right implication, first *)
  69
  70 lemma opp_to_opposite: ∀a,b. opp a b → a = opposite b.
  71 #a #b #oppab
  72 cases oppab // qed.
  73
  74 (*
  75 \ 5h2 class="section"\ 6Rewriting\ 5/h2\ 6
  76 Let us come to the opposite direction. *)
  77
  78 lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b.
  79 #a #b #eqa
  80 >eqa
  81 cases b // qed.
  82
  83 (*
  84 \ 5h2 class="section"\ 6Records\ 5/h2\ 6
  85 It is time to proceed with our formalization of the farmer's problem.
  86 A state of the system is defined by the position of four items: the goat, the
  87 wolf, the cabbage, and the boat. The simplest way to declare such a data type
  88 is to use a record.
  89 *)
  90
  91 record state : Type[0] ≝
  92   {goat_pos : bank;
  93    wolf_pos : bank;
  94    cabbage_pos: bank;
  95    boat_pos : bank}.
  96
  97 (* When you define a record named foo, the system automatically defines a record
  98 constructor named mk_foo. To construct a new record you pass as arguments to
  99 mk_foo the values of the record fields *)
 100
 101 definition start ≝ mk_state east east east east.
 102 definition end ≝ mk_state west west west west.
 103
 104 (* We must now define the possible moves. A natural way to do it is in the form
 105 of a relation (a binary predicate) over states.
 106
 107           g ⊥ g1
 108  ----------------------- (move_goat)
 109  (g,w,c,g) ↦ (g1,w,c,g1)
 110
 111           w ⊥ w1
 112  ----------------------- (move_wolf)
 113  (g,w,c,w) ↦ (g,w1,c,w1)
 114
 115           c ⊥ c1
 116  ----------------------- (move_cabbage)
 117  (g,w,c,c) ↦ (g,w,c1,c1)
 118
 119          b ⊥ b1
 120  ---------------------- (move_boat)
 121  (g,w,c,b) ↦ (g,w,c,b1)
 122
 123 *)
 124
 125 inductive move : state → state → Prop ≝
 126 | move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1)
 127   (* We can move the goat from a bank g to the opposite bank g1 if and only if the
 128      boat is on the same bank g of the goat and we move the boat along with it. *)
 129 | move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
 130 | move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
 131 | move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).
 132
 133 (* A state is safe if either the goat is on the same bank of the boat, or both
 134 the wolf and the cabbage are on the opposite bank of the goat. *)
 135
 136 inductive safe_state : state → Prop ≝
 137 | with_boat : ∀g,w,c.safe_state (mk_state g w c g)
 138 | opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b).
 139
 140 (* Finally, a state y is reachable from x if either there is a single move
 141 leading from x to y, or there is a safe state z such that z is reachable from x
 142 and there is a move leading from z to y *)
 143
 144 inductive reachable : state → state → Prop ≝
 145 | one : ∀x,y.move x y → reachable x y
 146 | 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.
 147
 148 (*
 149 \ 5h2 class="section"\ 6Automation\ 5/h2\ 6
 150 Remarkably, Matita is now able to solve the problem by itself, provided
 151 you allow automation to exploit more resources. The command /n/ is similar to
 152 //, where n is a measure of this complexity: in particular it is a bound to
 153 the depth of the expected proof tree (more precisely, to the number of nested
 154 applicative nodes). In this case, there is a solution in six moves, and we
 155 need a few more applications to handle reachability, and side conditions.
 156 The magic number to let automation work is, in this case, 9. *)
 157
 158 lemma problem: reachable start end.
 159 normalize /9/ qed.
 160
 161 (*
 162 \ 5h2 class="section"\ 6A complex interactive proof\ 5/h2\ 6
 163 Let us now try to derive the proof in a more interactive way. Of course, we
 164 expect to need several moves to transfer all items from a bank to the other, so
 165 we should start our proof by applying "more". Matita syntax for invoking the
 166 application of a property named foo is to write "@foo". In general, the philosophy
 167 of Matita is to describe each proof of a property P as a structured collection of
 168 objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining
 169 the way it is actually used (e.g. for introduction, rewriting, in an applicative
 170 step, and so on).
 171
 172 - tinycals
 173 - implicit arguments
 174 *)
 175
 176 lemma problem1: reachable start end.
 177 normalize @more
 178 (*
 179    - multiple conjectures
 180    - tinycals
 181  *)
 182   [  @(mk_state east west west east)
 183   || //
 184   | /2/ ]
 185
 186 (* implicit arguments *)
 187 @(more ? (mk_state east west west west))
 188 /2/
 189
 190 (* vectors of implicit arguments *)
 191 @(more … (move_wolf … ))
 192
 193 (* focusing *)
 194 [4: @east] /2/
 195
 196 (* Alternatively, we can directly instantiate the bank into the move. Let
 197 us complete the proof in this, very readable way. *)
 198 @(more … (move_goat west … )) /2/
 199 @(more … (move_cabbage ?? east … )) /2/
 200 @(more … (move_boat ??? west … )) /2/
 201 @one /2/ qed.