matita/matita/lib/tutorial/chapter10.ma

   1 (*
   2 Moves
   3 We now define the move operation, that corresponds to the advancement of the
   4 state in response to the processing of an input character a. The intuition is
   5 clear: we have to look at points inside $e$ preceding the given character a,
   6 let the point traverse the character, and broadcast it. All other points must
   7 be removed.
   8
   9 We can give a particularly elegant definition in terms of the
  10 lifted operators of the previous section:
  11 *)
  12
  13 include "tutorial/chapter9.ma".
  14
  15 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  16  match E with
  17   [ pz ⇒ 〈 pz S, false 〉
  18   | pe ⇒ 〈 ϵ, false 〉
  19   | ps y ⇒ 〈 `y, false 〉
  20   | pp y ⇒ 〈 `y, x == y 〉
  21   | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
  22   | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
  23   | pk e ⇒ (move ? x e)^⊛ ].
  24
  25 lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
  26   move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
  27 // qed.
  28
  29 lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
  30   move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
  31 // qed.
  32
  33 lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
  34   move S x i^* = (move ? x i)^⊛.
  35 // qed.
  36
  37 (*
  38 Example. Let us consider the item
  39
  40                                (•a + ϵ)((•b)*•a + •b)b
  41
  42 and the two moves w.r.t. the characters a and b.
  43 For a, we have two possible positions (all other points gets erased); the innermost
  44 point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
  45 so
  46
  47       move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
  48
  49 For b, we have two positions too. The innermost point stops in front of the final b too,
  50 while the other point reaches the end of b* and must go back through b*a:
  51
  52       move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a +  ϵ)((•b)*•a + b)•b, false〉
  53
  54 *)
  55
  56 definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (fst … e).
  57
  58 lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.
  59   pmove ? x 〈i,b〉 = move ? x i.
  60 // qed.
  61
  62 lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b.
  63   a::l1 = b::l2 → a = b.
  64 #A #l1 #l2 #a #b #H destruct //
  65 qed.
  66
  67 (* Obviously, a move does not change the carrier of the item, as one can easily
  68 prove by induction on the item. *)
  69
  70 lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
  71   |fst … (move ? a i)| = |i|.
  72 #S #a #i elim i //
  73   [#i1 #i2 #H1 #H2 >move_cat >erase_odot //
  74   |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); //
  75   ]
  76 qed.
  77
  78 (* Here is our first, major result, stating the correctness of the
  79 move operation. The proof is a simple induction on i. *)
  80
  81 theorem move_ok:
  82  ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S.
  83    \sem{move ? a i} w ↔ \sem{i} (a::w).
  84 #S #a #i elim i
  85   [normalize /2/
  86   |normalize /2/
  87   |normalize /2/
  88   |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
  89     [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
  90     |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
  91     ]
  92   |#i1 #i2 #HI1 #HI2 #w >move_cat
  93    @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
  94    @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r
  95    @iff_trans[||@iff_sym @deriv_middot //]
  96    @cat_ext_l @HI1
  97   |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
  98    @iff_trans[|@sem_oplus]
  99    @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
 100   |#i1 #HI1 #w >move_star
 101    @iff_trans[|@sem_ostar] >same_kernel >sem_star_w
 102    @iff_trans[||@iff_sym @deriv_middot //]
 103    @cat_ext_l @HI1
 104   ]
 105 qed.
 106
 107 (* The move operation is generalized to strings in the obvious way. *)
 108
 109 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 110
 111 let rec moves (S : DeqSet) w e on w : pre S ≝
 112  match w with
 113   [ nil ⇒ e
 114   | cons x w' ⇒ w' ↦* (move S x (fst … e))].
 115
 116 lemma moves_empty: ∀S:DeqSet.∀e:pre S.
 117   moves ? [ ] e = e.
 118 // qed.
 119
 120 lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
 121   moves ? (a::w)  e = moves ? w (move S a (fst … e)).
 122 // qed.
 123
 124 lemma moves_left : ∀S,a,w,e.
 125   moves S (w@(a::[])) e = move S a (fst … (moves S w e)).
 126 #S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
 127 qed.
 128
 129 lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
 130   ((a::w) ∈ e) ↔ ((a::w) ∈ (fst (pitem S) bool e)).
 131 #S #a #w * #i #b cases b normalize
 132   [% /2/ * // #H destruct |% normalize /2/]
 133 qed.
 134
 135 lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
 136   |fst … (moves ? w e)| = |fst … e|.
 137 #S #w elim w //
 138 qed.
 139
 140 theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
 141    (snd … (moves ? w e) = true) ↔ \sem{e} w.
 142 #S #w elim w
 143  [* #i #b >moves_empty cases b % /2/
 144  |#a #w1 #Hind #e >moves_cons
 145   @iff_trans [||@iff_sym @not_epsilon_sem]
 146   @iff_trans [||@move_ok] @Hind
 147  ]
 148 qed.
 149
 150 (* It is now clear that we can build a DFA D_e for e by taking pre as states,
 151 and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
 152 final if and only if b is true. The fact that states in D_e are finite is obvious:
 153 in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
 154 e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
 155 whose finite nature only holds after a suitable quotient.
 156
 157 Let us discuss a couple of examples.
 158
 159 Example.
 160 Below is the DFA associated with the regular expression (ac+bc)*.
 161
 162 DFA for (ac+bc)
 163
 164 The graphical description of the automaton is the traditional one, with nodes for
 165 states and labelled arcs for transitions. Unreachable states are not shown.
 166 Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
 167 only if b is true, we may just label nodes with the item.
 168 The automaton is not minimal: it is easy to see that the two states corresponding to
 169 the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
 170 that they define the same language!). In fact, an important property of pres e is that
 171 each state has a clear semantics, given in terms of the specification e and not of the
 172 behaviour of the automaton. As a consequence, the construction of the automaton is not
 173 only direct, but also extremely intuitive and locally verifiable.
 174
 175 Let us consider a more complex case.
 176
 177 Example.
 178 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 179
 180 DFA for (a+ϵ)(b*a + b)b
 181
 182 Remarkably, this DFA is minimal, testifying the small number of states produced by our
 183 technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
 184 are final, while 8 and 9 are not).
 185
 186
 187 Move to pit
 188 .
 189
 190 We conclude this chapter with a few properties of the move opertions in relation
 191 with the pit state. *)
 192
 193 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
 194
 195 (* The following "occur" function compute the list of characters occurring in a
 196 given item i. We first define a special append function that appends two lists
 197 avoiding repetitions, and prove a few properties of it.
 198 *)
 199
 200 let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
 201   match l1 with
 202   [ nil ⇒ l2
 203   | cons a tl ⇒
 204      let r ≝ unique_append S tl l2 in
 205      if memb S a r then r else a::r
 206   ].
 207
 208 lemma memb_unique_append: ∀S,a,l1,l2.
 209 memb S a (unique_append S l1 l2) = true →
 210   memb S a l1= true ∨ memb S a l2 = true.
 211 #S #a #l1 elim l1 normalize [#l2 #H %2 //]
 212 #b #tl #Hind #l2 cases (true_or_false … (a==b)) #Hab >Hab normalize /2/
 213 cases (memb S b (unique_append S tl l2)) normalize
 214   [@Hind | >Hab normalize @Hind]
 215 qed.
 216
 217 lemma unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2.
 218 (∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
 219 ∀x. memb S x (unique_append S l1 l2) = true → P x.
 220 #S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx)
 221 /2/
 222 qed.
 223
 224 lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
 225   uniqueb S (unique_append S l1 l2) = true.
 226 #S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
 227 cases (true_or_false … (memb S a (unique_append S tl l2)))
 228 #H >H normalize [@Hind //] >H normalize @Hind //
 229 qed.
 230
 231 definition sublist ≝
 232   λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
 233
 234 lemma memb_exists: ∀S,a,l.memb S a l = true →
 235   ∃l1,l2.l=l1@(a::l2).
 236 #S #a #l elim l [normalize #abs @False_ind /2/]
 237 #b #tl #Hind #H cases (orb_true_l … H)
 238   [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
 239   |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
 240    @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
 241   ]
 242 qed.
 243
 244 lemma sublist_length: ∀S,l1,l2.
 245  uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
 246 #S #l1 elim l1 //
 247 #a #tl #Hind #l2 #unique #sub
 248 cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub normalize >(\b (refl … a)) //]
 249 * #l3 * #l4 #eql2 >eql2 >length_append normalize
 250 applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
 251 >eql2 in sub; #sub #x #membx
 252 cases (memb_append … (sub x (orb_true_r2 … membx)))
 253   [#membxl3 @memb_append_l1 //
 254   |#membxal4 cases (orb_true_l … membxal4)
 255     [#eqxa @False_ind lapply (andb_true_l … unique)
 256      <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
 257     ]
 258   ]
 259 qed.
 260
 261 lemma sublist_unique_append_l1:
 262   ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
 263 #S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
 264 #x #tl #Hind #l2 #a
 265 normalize cases (true_or_false … (a==x)) #eqax >eqax
 266 [<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
 267   [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
 268 |cases (memb S x (unique_append S tl l2)) normalize
 269   [/2/ |>eqax normalize /2/]
 270 ]
 271 qed.
 272
 273 lemma sublist_unique_append_l2:
 274   ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
 275 #S #l1 elim l1 [normalize //] #x #tl #Hind normalize
 276 #l2 #a cases (memb S x (unique_append S tl l2)) normalize
 277 [@Hind | cases (a==x) normalize // @Hind]
 278 qed.
 279
 280 lemma decidable_sublist:∀S,l1,l2.
 281   (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
 282 #S #l1 #l2 elim l1
 283   [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
 284   |#a #tl * #subtl
 285     [cases (true_or_false (memb S a l2)) #memba
 286       [%1 whd #x #membx cases (orb_true_l … membx)
 287         [#eqax >(\P eqax) // |@subtl]
 288       |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 normalize
 289        >(\b (refl … a)) //
 290       ]
 291     |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 normalize cases (x==a)
 292      normalize //
 293     ]
 294   ]
 295 qed.
 296
 297 let rec occur (S: DeqSet) (i: re S) on i ≝
 298   match i with
 299   [ z ⇒ [ ]
 300   | e ⇒ [ ]
 301   | s y ⇒ y::[]
 302   | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 303   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 304   | k e ⇒ occur S e].
 305
 306
 307
 308 (* If a symbol a does not occur in i, then move(i,a) gets to the
 309 pit state. *)
 310
 311 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
 312   move S a i  = pit_pre S i.
 313 #S #a #i elim i //
 314   [#x normalize cases (a==x) normalize // #H @False_ind /2/
 315   |#i1 #i2 #Hind1 #Hind2 #H >move_cat
 316    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 317    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 318   |#i1 #i2 #Hind1 #Hind2 #H >move_plus
 319    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 320    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 321   |#i #Hind #H >move_star >Hind //
 322   ]
 323 qed.
 324
 325 (* We cannot escape form the pit state. *)
 326
 327 lemma move_pit: ∀S,a,i. move S a (fst ?? (pit_pre S i)) = pit_pre S i.
 328 #S #a #i elim i //
 329   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
 330   |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
 331   |#i #Hind >move_star >Hind //
 332   ]
 333 qed.
 334
 335 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 336 #S #w #i elim w // #a #w1 #H normalize >move_pit @H
 337 qed.
 338
 339 (* If any character in w does not occur in i, then moves(i,w) gets
 340 to the pit state. *)
 341
 342 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|fst ?? e|)) →
 343  moves S w e = pit_pre S (fst ?? e).
 344 #S #w elim w
 345   [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
 346   |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|fst ?? e|))))
 347     [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
 348      @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
 349       [#H2 >(\P H2) // |#H2 @H1 //]
 350     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
 351     ]
 352   ]
 353 qed.