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 function compute the list of characters occurring in a given
 196 item i. *)
 197
 198 let rec occur (S: DeqSet) (i: re S) on i ≝
 199   match i with
 200   [ z ⇒ [ ]
 201   | e ⇒ [ ]
 202   | s y ⇒ y::[]
 203   | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 204   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 205   | k e ⇒ occur S e].
 206
 207 (* If a symbol a does not occur in i, then move(i,a) gets to the
 208 pit state. *)
 209
 210 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
 211   move S a i  = pit_pre S i.
 212 #S #a #i elim i //
 213   [#x normalize cases (a==x) normalize // #H @False_ind /2/
 214   |#i1 #i2 #Hind1 #Hind2 #H >move_cat
 215    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 216    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 217   |#i1 #i2 #Hind1 #Hind2 #H >move_plus
 218    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 219    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 220   |#i #Hind #H >move_star >Hind //
 221   ]
 222 qed.
 223
 224 (* We cannot escape form the pit state. *)
 225
 226 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 227 #S #a #i elim i //
 228   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
 229   |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
 230   |#i #Hind >move_star >Hind //
 231   ]
 232 qed.
 233
 234 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 235 #S #w #i elim w //
 236 qed.
 237
 238 (* If any character in w does not occur in i, then moves(i,w) gets
 239 to the pit state. *)
 240
 241 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
 242  moves S w e = pit_pre S (\fst e).
 243 #S #w elim w
 244   [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
 245   |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
 246     [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
 247      @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
 248       [#H2 >(\P H2) // |#H2 @H1 //]
 249     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
 250     ]
 251   ]
 252 qed.