weblib/tutorial/chapter1.ma

   1
   2 (*
   3 In a system like Matita's very few things are built-in: not even booleans or logical connectives.
   4 The main philosophy od the system is to let you define your own data-types and functions using a powerful computational
   5 mechanism based on the declaration of inductive types.
   6
   7 Let us start this tutorial with a simple example based on the following well known problem.
   8
   9 \ 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 only one place available
  10 on his boat. Furthermore, the goat will eat the cabbage if they are left alone on the same bank, and similarly
  11 the wolf will eat the goat. The problem consists in bringing all three item safely across the river.
  12
  13 Our first data type defines the two banks of the river, which we will call east and west. It is a simple
  14 example of enumerated type, defined by explicitly declaring all its elements. The type itself is called
  15 "bank".
  16
  17 *)
  18
  19 include "basics/pts.ma".
  20
  21 inductive bank: Type[0] ≝
  22 | east : bank
  23 | west : bank.
  24
  25 (* We can now define a simple function computing, for each bank of the river,
  26 the opposite one *)
  27
  28 definition opposite ≝ λs.
  29 match s with
  30   [ east ⇒ west
  31   | west ⇒ east
  32   ].
  33
  34 lemma east_to_west : change_side east = west.
  35 // qed.
  36
  37 lemma west_to_east : change_side west = east.
  38 // qed.
  39
  40 lemma change_twice : ∀x. change_side (change_side x) = x.
  41 * //
  42 qed.
  43
  44 inductive item: Type[0] ≝
  45 | goat : item
  46 | wolf : item
  47 | cabbage: item
  48 | boat : item.
  49
  50 (* definition state ≝ item → side. *)
  51
  52 record state : Type[0] ≝
  53   {goat_pos : side;
  54    wolf_pos : side;
  55    cabbage_pos: side;
  56    boat_pos : side}.
  57
  58 definition state_of_item ≝ λs,i.
  59 match i with
  60 [ goat ⇒  goat_pos s
  61 | wolf ⇒  wolf_pos s
  62 | cabbage ⇒  cabbage_pos s
  63 | boat ⇒  boat_pos s].
  64
  65 (*
  66 definition is_movable ≝ λs,i.
  67   state_of_item s i = state_of_item s boat.
  68
  69 record movable_item (s:state) : Type[0] ≝
  70   {elem : item;
  71    mov : is_movable s elem}. *)
  72
  73 definition start :state ≝
  74   mk_state east east east east.
  75
  76 (* slow
  77 inductive move : state → state → Type[0] ≝
  78 | move_goat: ∀g,w,c.
  79   move (mk_state (change_side g) w c (change_side g)) (mk_state g w c g)
  80 | move_wolf: ∀g,w,c.
  81   move (mk_state g (change_side w) c (change_side w)) (mk_state g w c w)
  82 | move_cabbage: ∀g,w,c.
  83   move (mk_state g w (change_side c) (change_side c)) (mk_state g w c c)
  84 | move_boat: ∀g,w,c,b.
  85   move (mk_state g w c (change_side b)) (mk_state g w c b).
  86 *)
  87
  88 (*  this is working well *)
  89 inductive move : state → state → Type[0] ≝
  90 | move_goat: ∀g,w,c.
  91   move (mk_state g w c g) (mk_state (change_side g) w c (change_side g))
  92 | move_wolf: ∀g,w,c.
  93   move (mk_state g w c w) (mk_state g (change_side w) c (change_side w))
  94 | move_cabbage: ∀g,w,c.
  95   move (mk_state g w c c) (mk_state g w (change_side c) (change_side c))
  96 | move_boat: ∀g,w,c,b.
  97   move (mk_state g w c b) (mk_state g w c (change_side b)).
  98
  99
 100 (* this is working
 101 inductive move : state → state → Type[0] ≝
 102 | move_goat: ∀g,g1,w,c. change_side g = g1 →
 103   move (mk_state g w c g) (mk_state g1 w c g1)
 104 | move_wolf: ∀g,w,w1,c. change_side w = w1 →
 105   move (mk_state g w c w) (mk_state g w1 c w1)
 106 | move_cabbage: ∀g,w,c,c1. change_side c = c1 →
 107   move (mk_state g w c c) (mk_state g w c1 c1)
 108 | move_boat: ∀g,w,c,b,b1. change_side b = b1 →
 109   move (mk_state g w c b) (mk_state g w c b1)
 110 .*)
 111
 112 (*
 113 inductive move : state →state → Type[0] ≝
 114 | move_goat: ∀s.∀h:is_movable s goat. move s (mk_state (change_side (goat_pos s)) (wolf_pos s)
 115   (cabbage_pos s) (change_side (boat_pos s)))
 116 | move_wolf: ∀s.∀h:is_movable s wolf. move s (mk_state (goat_pos s) (change_side (wolf_pos s))
 117   (cabbage_pos s) (change_side (boat_pos s)))
 118 | move_cabbage: ∀s.∀h:is_movable s cabbage. move s (mk_state (goat_pos s) (wolf_pos s)
 119   (change_side (cabbage_pos s)) (change_side (boat_pos s)))
 120 | move_boat: ∀s.move s (mk_state (goat_pos s) (wolf_pos s)
 121   (cabbage_pos s) (change_side (boat_pos s))).
 122 *)
 123
 124 (*
 125 definition legal_state ≝ λs.
 126   goat_pos s = boat_pos s ∨
 127   (goat_pos s = change_side (cabbage_pos s) ∧
 128    goat_pos s = change_side (wolf_pos s)). *)
 129
 130 inductive legal_state : state → Prop ≝
 131 | with_boat : ∀g,w,c.legal_state (mk_state g w c g)
 132 | opposite_side : ∀g,b.
 133     legal_state (mk_state g (change_side g) (change_side g) b).
 134
 135 inductive reachable : state → state → Prop ≝
 136 | one : ∀s1,s2.move s1 s2 → reachable s1 s2
 137 | more : ∀s1,s2,s3. reachable s1 s2 → legal_state s2 → move s2 s3 →
 138   reachable s1 s3.
 139
 140 definition end ≝ mk_state west west west west.
 141 definition second ≝ mk_state west east east west.
 142 definition third ≝ mk_state west east east east.
 143 definition fourth ≝ mk_state west west east west.
 144 definition fifth ≝ mk_state east west east east.
 145 definition sixth ≝ mk_state east west west west.
 146 definition seventh ≝ mk_state east west west east.
 147
 148 lemma problem: reachable start end.
 149 normalize /8/ qed.
 150
 151 lemma problem: reachable start end.
 152 normalize
 153 @more [4: @move_goat || 3: //]
 154 @more [4: @move_boat || 3: //]
 155 @more [4: @move_wolf || 3: //]
 156 @more [4: @move_goat || 3: //]
 157 @more [4: @move_cabbage || 3: //]
 158 @more [4: @move_boat || 3: //]
 159 @one //
 160 qed.
 161
 162
 163 (*
 164 definition move_item ≝ λs.λi:movable_item s.
 165 match (elem ? i) with
 166 [ goat ⇒ mk_state (change_side (goat_pos s)) (wolf_pos s)
 167   (cabbage_pos s) (change_side (boat_pos s))
 168 | wolf ⇒ mk_state (goat_pos s) (change_side (wolf_pos s))
 169   (cabbage_pos s) (change_side (boat_pos s))
 170 | cabbage ⇒ mk_state (goat_pos s) (wolf_pos s)
 171   (change_side (cabbage_pos s)) (change_side (boat_pos s))
 172 | boat ⇒ mk_state (goat_pos s) (wolf_pos s)
 173   (cabbage_pos s) (change_side (boat_pos s))
 174 ].
 175
 176 definition legal_state ≝ λs.
 177   cabbage_pos s = goat_pos s ∨
 178   goat_pos s = wolf_pos s → goat_pos s = boat_pos s.
 179
 180 definition legal_step ≝ λs1,s2.
 181   ∃i.move_item s1 i = s2.
 182
 183 inductive reachable : state → state → Prop ≝
 184 | nil : ∀s.reachable s s
 185 | step : ∀s1,s2,s3. legal_step s1 s2 → legal_state s2 → reachable s2 s3 →
 186   reachable s1 s3.
 187
 188 definition second ≝ mk_state west east east west.
 189 definition end ≝ mk_state west west west west.
 190
 191 lemma goat_move: ∀s.legal_step s (mk_state (change_side (goat_pos s)) (wolf_pos s)
 192   (cabbage_pos s) (change_side (boat_pos s))).
 193
 194 lemma problem: reachable start second.
 195 @step [| @ex_intro  // [| @move_goat ] // | //]
 196
 197   [|| @move_goat //| //
 198   |normalize