matita/matita/lib/tutorial/chapter7.ma

   1 (*
   2 Regular Expressions
   3
   4 We shall apply all the previous machinery to the study of regular languages
   5 and the constructions of the associated finite automata. *)
   6
   7 include "tutorial/chapter6.ma".
   8
   9 (* The type re of regular expressions over an alphabet $S$ is the smallest
  10 collection of objects generated by the following constructors: *)
  11
  12 inductive re (S: DeqSet) : Type[0] ≝
  13    z: re S                (* empty: ∅ *)
  14  | e: re S                (* epsilon: ϵ *)
  15  | s: S → re S            (* symbol: a *)
  16  | c: re S → re S → re S  (* concatenation: e1 · e2 *)
  17  | o: re S → re S → re S  (* plus: e1 + e2 *)
  18  | k: re S → re S.        (* kleene's star: e* *)
  19
  20 interpretation "re epsilon" 'epsilon = (e ?).
  21 interpretation "re or" 'plus a b = (o ? a b).
  22 interpretation "re cat" 'middot a b = (c ? a b).
  23 interpretation "re star" 'star a = (k ? a).
  24
  25 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
  26 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
  27 interpretation "atom" 'ps a = (s ? a).
  28
  29 notation "`∅" non associative with precedence 90 for @{ 'empty }.
  30 interpretation "empty" 'empty = (z ?).
  31
  32 (* The language sem{e} associated with the regular expression e is inductively
  33 defined by the following function: *)
  34
  35 let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
  36 match r with
  37 [ z ⇒ ∅
  38 | e ⇒ {ϵ}
  39 | s x ⇒ { (x::[]) }
  40 | c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
  41 | o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
  42 | k r1 ⇒ (in_l ? r1) ^*].
  43
  44 notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
  45 interpretation "in_l" 'in_l E = (in_l ? E).
  46 interpretation "in_l mem" 'mem w l = (in_l ? l w).
  47
  48 lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
  49 // qed.
  50
  51
  52 (*
  53 Pointed Regular expressions
  54
  55 We now introduce pointed regular expressions, that are the main tool we shall
  56 use for the construction of the automaton.
  57 A pointed regular expression is just a regular expression internally labelled
  58 with some additional points. Intuitively, points mark the positions inside the
  59 regular expression which have been reached after reading some prefix of
  60 the input string, or better the positions where the processing of the remaining
  61 string has to be started. Each pointed expression for $e$ represents a state of
  62 the {\em deterministic} automaton associated with $e$; since we obviously have
  63 only a finite number of possible labellings, the number of states of the automaton
  64 is finite.
  65
  66 Pointed regular expressions provide the tool for an algebraic revisitation of
  67 McNaughton and Yamada's algorithm for position automata, making the proof of its
  68 correctness, that is far from trivial, particularly clear and simple. In particular,
  69 pointed expressions offer an appealing alternative to Brzozowski's derivatives,
  70 avoiding their weakest point, namely the fact of being forced to quotient derivatives
  71 w.r.t. a suitable notion of equivalence in order to get a finite number of states
  72 (that is not essential for recognizing strings, but is crucial for comparing regular
  73 expressions).
  74
  75 Our main data structure is the notion of pointed item, that is meant whose purpose
  76 is to encode a set of positions inside a regular expression.
  77 The idea of formalizing pointers inside a data type by means of a labelled version
  78 of the data type itself is probably one of the first, major lessons learned in the
  79 formalization of the metatheory of programming languages. For our purposes, it is
  80 enough to mark positions preceding individual characters, so we shall have two kinds
  81 of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
  82
  83 inductive pitem (S: DeqSet) : Type[0] ≝
  84    pz: pitem S                       (* empty *)
  85  | pe: pitem S                       (* epsilon *)
  86  | ps: S → pitem S                   (* symbol *)
  87  | pp: S → pitem S                   (* pointed sysmbol *)
  88  | pc: pitem S → pitem S → pitem S   (* concatenation *)
  89  | po: pitem S → pitem S → pitem S   (* plus *)
  90  | pk: pitem S → pitem S.            (* kleene's star *)
  91
  92 (* A pointed regular expression (pre) is just a pointed item with an additional
  93 boolean, that must be understood as the possibility to have a trailing point at
  94 the end of the expression. As we shall see, pointed regular expressions can be
  95 understood as states of a DFA, and the boolean indicates if
  96 the state is final or not. *)
  97
  98 definition pre ≝ λS.pitem S × bool.
  99
 100 interpretation "pitem star" 'star a = (pk ? a).
 101 interpretation "pitem or" 'plus a b = (po ? a b).
 102 interpretation "pitem cat" 'middot a b = (pc ? a b).
 103 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
 104 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
 105 interpretation "pitem pp" 'pp a = (pp ? a).
 106 interpretation "pitem ps" 'ps a = (ps ? a).
 107 interpretation "pitem epsilon" 'epsilon = (pe ?).
 108 interpretation "pitem empty" 'empty = (pz ?).
 109
 110 (* The carrier $|i|$ of an item i is the regular expression obtained from i by
 111 removing all the points. Similarly, the carrier of a pointed regular expression
 112 is the carrier of its item. *)
 113
 114 let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
 115  match l with
 116   [ pz ⇒ z ? (* `∅ *)
 117   | pe ⇒ ϵ
 118   | ps x ⇒ `x
 119   | pp x ⇒ `x
 120   | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
 121   | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
 122   | pk E ⇒ (forget ? E)^* ].
 123
 124 (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
 125 interpretation "forget" 'norm a = (forget ? a).
 126
 127 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
 128 // qed.
 129
 130 lemma erase_plus : ∀S.∀i1,i2:pitem S.
 131   |i1 + i2| = |i1| + |i2|.
 132 // qed.
 133
 134 lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
 135 // qed.
 136
 137 (*
 138 Comparing items and pres
 139
 140 Items and pres are very concrete datatypes: they can be effectively compared,
 141 and enumerated. In particular, we can define a boolean equality beqitem and a proof
 142 beqitem_true that it refects propositional equality, enriching the set (pitem S)
 143 to a DeqSet. *)
 144
 145 let rec beqitem S (i1,i2: pitem S) on i1 ≝
 146   match i1 with
 147   [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
 148   | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
 149   | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
 150   | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
 151   | po i11 i12 ⇒ match i2 with
 152     [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
 153     | _ ⇒ false]
 154   | pc i11 i12 ⇒ match i2 with
 155     [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
 156     | _ ⇒ false]
 157   | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
 158   ].
 159
 160 lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
 161 #S #i1 elim i1
 162   [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 163   |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 164   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 165     [>(\P H) // | @(\b (refl …))]
 166   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 167     [>(\P H) // | @(\b (refl …))]
 168   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 169    normalize #H destruct
 170     [cases (true_or_false (beqitem S i11 i21)) #H1
 171       [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
 172       |>H1 in H; normalize #abs @False_ind /2/
 173       ]
 174     |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
 175     ]
 176   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 177    normalize #H destruct
 178     [cases (true_or_false (beqitem S i11 i21)) #H1
 179       [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
 180       |>H1 in H; normalize #abs @False_ind /2/
 181       ]
 182     |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
 183     ]
 184   |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
 185    normalize #H destruct
 186     [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
 187   ]
 188 qed.
 189
 190 definition DeqItem ≝ λS.
 191   mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
 192
 193 (* We also add a couple of unification hints to allow the type inference system
 194 to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
 195 equality function of a DeqSet. *)
 196
 197 unification hint  0 ≔ S;
 198     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 199 (* ---------------------------------------- *) ⊢
 200     pitem S ≡ carr X.
 201
 202 unification hint  0 ≔ S,i1,i2;
 203     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 204 (* ---------------------------------------- *) ⊢
 205     beqitem S i1 i2 ≡ eqb X i1 i2.
 206
 207 (*
 208 Semantics of pointed regular expressions
 209
 210 The intuitive semantic of a point is to mark the position where
 211 we should start reading the regular expression. The language associated
 212 to a pre is the union of the languages associated with its points. *)
 213
 214 let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
 215 match r with
 216 [ pz ⇒ ∅
 217 | pe ⇒ ∅
 218 | ps _ ⇒ ∅
 219 | pp x ⇒ { (x::[]) }
 220 | pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
 221 | po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
 222 | pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^*  ].
 223
 224 interpretation "in_pl" 'in_l E = (in_pl ? E).
 225 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 226
 227 definition in_prl ≝ λS : DeqSet.λp:pre S.
 228   if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
 229
 230 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 231 interpretation "in_prl" 'in_l E = (in_prl ? E).
 232
 233 (* The following, trivial lemmas are only meant for rewriting purposes. *)
 234
 235 lemma sem_pre_true : ∀S.∀i:pitem S.
 236   \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
 237 // qed.
 238
 239 lemma sem_pre_false : ∀S.∀i:pitem S.
 240   \sem{〈i,false〉} = \sem{i}.
 241 // qed.
 242
 243 lemma sem_cat: ∀S.∀i1,i2:pitem S.
 244   \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
 245 // qed.
 246
 247 lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
 248   \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
 249 // qed.
 250
 251 lemma sem_plus: ∀S.∀i1,i2:pitem S.
 252   \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
 253 // qed.
 254
 255 lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
 256   \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
 257 // qed.
 258
 259 lemma sem_star : ∀S.∀i:pitem S.
 260   \sem{i^*} = \sem{i} · \sem{|i|}^*.
 261 // qed.
 262
 263 lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 264   \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
 265 // qed.
 266
 267 (* Below are a few, simple, semantic properties of items. In particular:
 268 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 269 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
 270 - minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
 271 - minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
 272 The first property is proved by a simple induction on $i$; the other
 273 results are easy corollaries. We need an auxiliary lemma first. *)
 274
 275 lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
 276 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
 277
 278 lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
 279 #S #e elim e normalize /2/
 280   [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
 281    >(append_eq_nil …H…) /2/
 282   |#r1 #r2 #n1 #n2 % * /2/
 283   |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
 284   ]
 285 qed.
 286
 287 lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
 288 #S * #i #b cases b // normalize #H @False_ind /2/
 289 qed.
 290
 291 lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
 292 #S * #i #b #btrue normalize in btrue; >btrue %2 //
 293 qed.
 294
 295 lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
 296 #S #i #w %
 297   [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
 298   |* //
 299   ]
 300 qed.
 301
 302 lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
 303 #S * #i *
 304   [>sem_pre_true normalize in ⊢ (??%?); #w %
 305     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
 306   |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
 307   ]
 308 qed.