weblib/tutorial/chapter1.ma

   1
   2 (*
   3 In a system like Matita's very few things are built-in: not even booleans or
   4 logical connectives. The main philosophy od the system is to let you define your
   5 own data-types and functions using a powerful computational mechanism based on
   6 the declaration of inductive types.
   7
   8 Let us start this tutorial with a simple example based on the following well known
   9 problem.
  10
  11 \ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6\ 5div class="paragraph"\ 6\ 5/div\ 6A farmer need to tranfer a goat, a wolf and a cabbage across a river, but there is
  12 only one place available on his boat. Furthermore, the goat will eat the cabbage if
  13 they are left alone on the same bank, and similarly the wolf will eat the goat.
  14 The problem consists in bringing all three item safely across the river.
  15
  16 Our first data type defines the two banks of the river, which we will call east and
  17 west. It is a simple example of enumerated type, defined by explicitly declaring all
  18 its elements. The type itself is called "bank".
  19 Before giving its definition we "include" the file "logic.ma" that contains a a few
  20 preliminary notions not worth discussing here.
  21 *)
  22
  23 include "basics/logic.ma".
  24
  25 inductive bank: Type[0] ≝
  26 | east : bank
  27 | west : bank.
  28
  29 (* We can now define a simple function computing, for each bank of the river,
  30 the opposite one. *)
  31
  32 definition opposite ≝ λs.
  33 match s with
  34   [ east ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
  35   | west ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6
  36   ].
  37
  38 (* Functions are live entities, and can be actually computed. To check this, let
  39 us state the property that the opposite bank of east is west; every lemma needs a
  40 name for further reference, and we call it "east_to_west". *)
  41
  42 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.
  43
  44 (* If you stop the execution here you will see a new window on the  right side
  45 of the screen: it is the goal window, providing a sequent like representation of
  46 the form
  47
  48 B1
  49 B2
  50 ....
  51 Bk
  52 -----------------------
  53 A
  54
  55 for each open goal remaining to be solved. A is the conclusion of the goal and
  56 B1, ..., Bk is its context, that is the set of current hypothesis and type
  57 declarations. In this case, we have only one goal, and its context is empty.
  58 The proof proceeds by typing commands to the system. In this case, we
  59 want to evaluate the function, that can be done by invoking the  "normalize"
  60 command:
  61 *)
  62
  63 normalize
  64
  65 (* By executing it - just type the advance command - you will see that the goal
  66 has changed to west = west, by reducing the subexpression (opposite east).
  67 You may use the retract bottom to undo the step, if you wish.
  68
  69 The new goal west = west is trivial: it is just a consequence of reflexivity.
  70 Such trivial steps can be just closed in Matita by typing a double slash.
  71 We complete the proof by the qed command, that instructs the system to store the
  72 lemma performing some bookkeeping operations.
  73 *)
  74
  75 // qed.
  76
  77 lemma west_to_east : change_side west = east.
  78 // qed.
  79
  80 lemma change_twice : ∀x. change_side (change_side x) = x.
  81 * //
  82 qed.
  83
  84 inductive item: Type[0] ≝
  85 | goat : item
  86 | wolf : item
  87 | cabbage: item
  88 | boat : item.
  89
  90 (* definition state ≝ item → side. *)
  91
  92 record state : Type[0] ≝
  93   {goat_pos : side;
  94    wolf_pos : side;
  95    cabbage_pos: side;
  96    boat_pos : side}.
  97
  98 definition state_of_item ≝ λs,i.
  99 match i with
 100 [ goat ⇒  goat_pos s
 101 | wolf ⇒  wolf_pos s
 102 | cabbage ⇒  cabbage_pos s
 103 | boat ⇒  boat_pos s].
 104
 105 (*
 106 definition is_movable ≝ λs,i.
 107   state_of_item s i = state_of_item s boat.
 108
 109 record movable_item (s:state) : Type[0] ≝
 110   {elem : item;
 111    mov : is_movable s elem}. *)
 112
 113 definition start :state ≝
 114   mk_state east east east east.
 115
 116 (* slow
 117 inductive move : state → state → Type[0] ≝
 118 | move_goat: ∀g,w,c.
 119   move (mk_state (change_side g) w c (change_side g)) (mk_state g w c g)
 120 | move_wolf: ∀g,w,c.
 121   move (mk_state g (change_side w) c (change_side w)) (mk_state g w c w)
 122 | move_cabbage: ∀g,w,c.
 123   move (mk_state g w (change_side c) (change_side c)) (mk_state g w c c)
 124 | move_boat: ∀g,w,c,b.
 125   move (mk_state g w c (change_side b)) (mk_state g w c b).
 126 *)
 127
 128 (*  this is working well *)
 129 inductive move : state → state → Type[0] ≝
 130 | move_goat: ∀g,w,c.
 131   move (mk_state g w c g) (mk_state (change_side g) w c (change_side g))
 132 | move_wolf: ∀g,w,c.
 133   move (mk_state g w c w) (mk_state g (change_side w) c (change_side w))
 134 | move_cabbage: ∀g,w,c.
 135   move (mk_state g w c c) (mk_state g w (change_side c) (change_side c))
 136 | move_boat: ∀g,w,c,b.
 137   move (mk_state g w c b) (mk_state g w c (change_side b)).
 138
 139
 140 (* this is working
 141 inductive move : state → state → Type[0] ≝
 142 | move_goat: ∀g,g1,w,c. change_side g = g1 →
 143   move (mk_state g w c g) (mk_state g1 w c g1)
 144 | move_wolf: ∀g,w,w1,c. change_side w = w1 →
 145   move (mk_state g w c w) (mk_state g w1 c w1)
 146 | move_cabbage: ∀g,w,c,c1. change_side c = c1 →
 147   move (mk_state g w c c) (mk_state g w c1 c1)
 148 | move_boat: ∀g,w,c,b,b1. change_side b = b1 →
 149   move (mk_state g w c b) (mk_state g w c b1)
 150 .*)
 151
 152 (*
 153 inductive move : state →state → Type[0] ≝
 154 | move_goat: ∀s.∀h:is_movable s goat. move s (mk_state (change_side (goat_pos s)) (wolf_pos s)
 155   (cabbage_pos s) (change_side (boat_pos s)))
 156 | move_wolf: ∀s.∀h:is_movable s wolf. move s (mk_state (goat_pos s) (change_side (wolf_pos s))
 157   (cabbage_pos s) (change_side (boat_pos s)))
 158 | move_cabbage: ∀s.∀h:is_movable s cabbage. move s (mk_state (goat_pos s) (wolf_pos s)
 159   (change_side (cabbage_pos s)) (change_side (boat_pos s)))
 160 | move_boat: ∀s.move s (mk_state (goat_pos s) (wolf_pos s)
 161   (cabbage_pos s) (change_side (boat_pos s))).
 162 *)
 163
 164 (*
 165 definition legal_state ≝ λs.
 166   goat_pos s = boat_pos s ∨
 167   (goat_pos s = change_side (cabbage_pos s) ∧
 168    goat_pos s = change_side (wolf_pos s)). *)
 169
 170 inductive legal_state : state → Prop ≝
 171 | with_boat : ∀g,w,c.legal_state (mk_state g w c g)
 172 | opposite_side : ∀g,b.
 173     legal_state (mk_state g (change_side g) (change_side g) b).
 174
 175 inductive reachable : state → state → Prop ≝
 176 | one : ∀s1,s2.move s1 s2 → reachable s1 s2
 177 | more : ∀s1,s2,s3. reachable s1 s2 → legal_state s2 → move s2 s3 →
 178   reachable s1 s3.
 179
 180 definition end ≝ mk_state west west west west.
 181 definition second ≝ mk_state west east east west.
 182 definition third ≝ mk_state west east east east.
 183 definition fourth ≝ mk_state west west east west.
 184 definition fifth ≝ mk_state east west east east.
 185 definition sixth ≝ mk_state east west west west.
 186 definition seventh ≝ mk_state east west west east.
 187
 188 lemma problem: reachable start end.
 189 normalize /8/ qed.
 190
 191 lemma problem: reachable start end.
 192 normalize
 193 @more [4: @move_goat || 3: //]
 194 @more [4: @move_boat || 3: //]
 195 @more [4: @move_wolf || 3: //]
 196 @more [4: @move_goat || 3: //]
 197 @more [4: @move_cabbage || 3: //]
 198 @more [4: @move_boat || 3: //]
 199 @one //
 200 qed.
 201
 202
 203 (*
 204 definition move_item ≝ λs.λi:movable_item s.
 205 match (elem ? i) with
 206 [ goat ⇒ mk_state (change_side (goat_pos s)) (wolf_pos s)
 207   (cabbage_pos s) (change_side (boat_pos s))
 208 | wolf ⇒ mk_state (goat_pos s) (change_side (wolf_pos s))
 209   (cabbage_pos s) (change_side (boat_pos s))
 210 | cabbage ⇒ mk_state (goat_pos s) (wolf_pos s)
 211   (change_side (cabbage_pos s)) (change_side (boat_pos s))
 212 | boat ⇒ mk_state (goat_pos s) (wolf_pos s)
 213   (cabbage_pos s) (change_side (boat_pos s))
 214 ].
 215
 216 definition legal_state ≝ λs.
 217   cabbage_pos s = goat_pos s ∨
 218   goat_pos s = wolf_pos s → goat_pos s = boat_pos s.
 219
 220 definition legal_step ≝ λs1,s2.
 221   ∃i.move_item s1 i = s2.
 222
 223 inductive reachable : state → state → Prop ≝
 224 | nil : ∀s.reachable s s
 225 | step : ∀s1,s2,s3. legal_step s1 s2 → legal_state s2 → reachable s2 s3 →
 226   reachable s1 s3.
 227
 228 definition second ≝ mk_state west east east west.
 229 definition end ≝ mk_state west west west west.
 230
 231 lemma goat_move: ∀s.legal_step s (mk_state (change_side (goat_pos s)) (wolf_pos s)
 232   (cabbage_pos s) (change_side (boat_pos s))).
 233
 234 lemma problem: reachable start second.
 235 @step [| @ex_intro  // [| @move_goat ] // | //]
 236
 237   [|| @move_goat //| //
 238   |normalize