weblib/tutorial/chapter7.ma

   1 (* We shall apply all the previous machinery to the study of regular languages
   2 and the constructions of the associated finite automata. *)
   3
   4 include "tutorial/chapter6.ma".
   5
   6 (* The type re of regular expressions over an alphabet $S$ is the smallest
   7 collection of objects generated by the following constructors: *)
   8
   9 inductive re (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
  10    z: re S                (* empty: ∅ *)
  11  | e: re S                (* epsilon: ϵ *)
  12  | s: S → re S            (* symbol: a *)
  13  | c: re S → re S → re S  (* concatenation: e1 · e2 *)
  14  | o: re S → re S → re S  (* plus: e1 + e2 *)
  15  | k: re S → re S.        (* kleene's star: e* *)
  16
  17 interpretation "re epsilon" 'epsilon = (e ?).
  18 interpretation "re or" 'plus a b = (o ? a b).
  19 interpretation "re cat" 'middot a b = (c ? a b).
  20 interpretation "re star" 'star a = (k ? a).
  21
  22 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
  23 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
  24 interpretation "atom" 'ps a = (s ? a).
  25
  26 notation "`∅" non associative with precedence 90 for @{ 'empty }.
  27 interpretation "empty" 'empty = (z ?).
  28
  29 (* The language $sem{e}$ associated with the regular expression e is inductively
  30 defined by the following function: *)
  31
  32 let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
  33 match r with
  34 [ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
  35 | e ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}
  36 | s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x]}
  37 | c r1 r2 ⇒ (in_l ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (in_l ? r2)
  38 | o r1 r2 ⇒ (in_l ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_l ? r2)
  39 | k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*].
  40
  41 notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
  42 interpretation "in_l" 'in_l E = (in_l ? E).
  43 interpretation "in_l mem" 'mem w l = (in_l ? l w).
  44
  45 lemma rsem_star : ∀S.∀r: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S. \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
  46 // qed.
  47
  48
  49 (* We now introduce pointed regular expressions, that are the main tool we shall
  50 use for the construction of the automaton.
  51 A pointed regular expression is just a regular expression internally labelled
  52 with some additional points. Intuitively, points mark the positions inside the
  53 regular expression which have been reached after reading some prefix of
  54 the input string, or better the positions where the processing of the remaining
  55 string has to be started. Each pointed expression for $e$ represents a state of
  56 the {\em deterministic} automaton associated with $e$; since we obviously have
  57 only a finite number of possible labellings, the number of states of the automaton
  58 is finite.
  59
  60 Pointed regular expressions provide the tool for an algebraic revisitation of
  61 McNaughton and Yamada's algorithm for position automata, making the proof of its
  62 correctness, that is far from trivial, particularly clear and simple. In particular,
  63 pointed expressions offer an appealing alternative to Brzozowski's derivatives,
  64 avoiding their weakest point, namely the fact of being forced to quotient derivatives
  65 w.r.t. a suitable notion of equivalence in order to get a finite number of states
  66 (that is not essential for recognizing strings, but is crucial for comparing regular
  67 expressions).
  68
  69 Our main data structure is the notion of pointed item, that is meant whose purpose
  70 is to encode a set of positions inside a regular expression.
  71 The idea of formalizing pointers inside a data type by means of a labelled version
  72 of the data type itself is probably one of the first, major lessons learned in the
  73 formalization of the metatheory of programming languages. For our purposes, it is
  74 enough to mark positions preceding individual characters, so we shall have two kinds
  75 of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
  76
  77 inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
  78    pz: pitem S                       (* empty *)
  79  | pe: pitem S                       (* epsilon *)
  80  | ps: S → pitem S                   (* symbol *)
  81  | pp: S → pitem S                   (* pointed sysmbol *)
  82  | pc: pitem S → pitem S → pitem S   (* concatenation *)
  83  | po: pitem S → pitem S → pitem S   (* plus *)
  84  | pk: pitem S → pitem S.            (* kleene's star *)
  85
  86 (* A pointed regular expression (pre) is just a pointed item with an additional
  87 boolean, that must be understood as the possibility to have a trailing point at
  88 the end of the expression. As we shall see, pointed regular expressions can be
  89 understood as states of a DFA, and the boolean indicates if
  90 the state is final or not. *)
  91
  92 definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
  93
  94 interpretation "pitem star" 'star a = (pk ? a).
  95 interpretation "pitem or" 'plus a b = (po ? a b).
  96 interpretation "pitem cat" 'middot a b = (pc ? a b).
  97 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
  98 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
  99 interpretation "pitem pp" 'pp a = (pp ? a).
 100 interpretation "pitem ps" 'ps a = (ps ? a).
 101 interpretation "pitem epsilon" 'epsilon = (pe ?).
 102 interpretation "pitem empty" 'empty = (pz ?).
 103
 104 (* The carrier $|i|$ of an item i is the regular expression obtained from i by
 105 removing all the points. Similarly, the carrier of a pointed regular expression
 106 is the carrier of its item. *)
 107
 108 let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
 109  match l with
 110   [ pz ⇒ `∅
 111   | pe ⇒ ϵ
 112   | ps x ⇒ `x
 113   | pp x ⇒ `x
 114   | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
 115   | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
 116   | pk E ⇒ (forget ? E)^* ].
 117
 118 (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
 119 interpretation "forget" 'norm a = (forget ? a).
 120
 121 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
 122 // qed.
 123
 124 lemma erase_plus : ∀S.∀i1,i2:pitem S.
 125   |i1 + i2| = |i1| + |i2|.
 126 // qed.
 127
 128 lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
 129 // qed.
 130
 131 (* Items and pres are a very concrete datatype: they can be effectively compared,
 132 and enumerated. In particular, we can define a boolean equality beqitem and
 133 \vebeqitem_true+ enriching the set \verb+(pitem S)+
 134 to a \verb+DeqSet+. boolean equality *)
 135 let rec beqitem S (i1,i2: pitem S) on i1 ≝
 136   match i1 with
 137   [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
 138   | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
 139   | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
 140   | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
 141   | po i11 i12 ⇒ match i2 with
 142     [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
 143     | _ ⇒ false]
 144   | pc i11 i12 ⇒ match i2 with
 145     [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
 146     | _ ⇒ false]
 147   | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
 148   ].
 149
 150 lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
 151 #S #i1 elim i1
 152   [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 153   |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 154   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 155     [>(\P H) // | @(\b (refl …))]
 156   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 157     [>(\P H) // | @(\b (refl …))]
 158   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 159    normalize #H destruct
 160     [cases (true_or_false (beqitem S i11 i21)) #H1
 161       [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
 162       |>H1 in H; normalize #abs @False_ind /2/
 163       ]
 164     |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
 165     ]
 166   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 167    normalize #H destruct
 168     [cases (true_or_false (beqitem S i11 i21)) #H1
 169       [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
 170       |>H1 in H; normalize #abs @False_ind /2/
 171       ]
 172     |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
 173     ]
 174   |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
 175    normalize #H destruct
 176     [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
 177   ]
 178 qed.
 179
 180 definition DeqItem ≝ λS.
 181   mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
 182
 183 unification hint  0 ≔ S;
 184     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 185 (* ---------------------------------------- *) ⊢
 186     pitem S ≡ carr X.
 187
 188 unification hint  0 ≔ S,i1,i2;
 189     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 190 (* ---------------------------------------- *) ⊢
 191     beqitem S i1 i2 ≡ eqb X i1 i2.
 192
 193 (* semantics *)
 194
 195 let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
 196 match r with
 197 [ pz ⇒ ∅
 198 | pe ⇒ ∅
 199 | ps _ ⇒ ∅
 200 | pp x ⇒ { [x] }
 201 | pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
 202 | po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
 203 | pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^*  ].
 204
 205 interpretation "in_pl" 'in_l E = (in_pl ? E).
 206 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 207
 208 definition in_prl ≝ λS : DeqSet.λp:pre S.
 209   if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
 210
 211 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 212 interpretation "in_prl" 'in_l E = (in_prl ? E).
 213
 214 lemma sem_pre_true : ∀S.∀i:pitem S.
 215   \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
 216 // qed.
 217
 218 lemma sem_pre_false : ∀S.∀i:pitem S.
 219   \sem{〈i,false〉} = \sem{i}.
 220 // qed.
 221
 222 lemma sem_cat: ∀S.∀i1,i2:pitem S.
 223   \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
 224 // qed.
 225
 226 lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
 227   \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
 228 // qed.
 229
 230 lemma sem_plus: ∀S.∀i1,i2:pitem S.
 231   \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
 232 // qed.
 233
 234 lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
 235   \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
 236 // qed.
 237
 238 lemma sem_star : ∀S.∀i:pitem S.
 239   \sem{i^*} = \sem{i} · \sem{|i|}^*.
 240 // qed.
 241
 242 lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 243   \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
 244 // qed.
 245
 246 lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
 247 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
 248
 249 lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
 250 #S #e elim e normalize /2/
 251   [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
 252    >(append_eq_nil …H…) /2/
 253   |#r1 #r2 #n1 #n2 % * /2/
 254   |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
 255   ]
 256 qed.
 257
 258 (* lemma 12 *)
 259 lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
 260 #S * #i #b cases b // normalize #H @False_ind /2/
 261 qed.
 262
 263 lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
 264 #S * #i #b #btrue normalize in btrue; >btrue %2 //
 265 qed.
 266
 267 lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
 268 #S #i #w %
 269   [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
 270   |* //
 271   ]
 272 qed.
 273
 274 lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
 275 #S * #i *
 276   [>sem_pre_true normalize in ⊢ (??%?); #w %
 277     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
 278   |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
 279   ]
 280 qed.
 281
 282 definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
 283 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 284 interpretation "oplus" 'oplus a b = (lo ? a b).
 285
 286 lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
 287 // qed.
 288
 289 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
 290   match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
 291
 292 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
 293 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
 294
 295 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
 296   A = B → A =1 B.
 297 #S #A #B #H >H /2/ qed.
 298
 299 lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
 300   \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
 301 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
 302 >sem_pre_true >sem_cat >sem_pre_true /2/
 303 qed.
 304
 305 definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
 306   match e1 with
 307   [ mk_Prod i1 b1 ⇒ match b1 with
 308     [ true ⇒ (i1 ◃ (bcast ? i2))
 309     | false ⇒ 〈i1 · i2,false〉
 310     ]
 311   ].
 312
 313 notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
 314 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
 315
 316 notation "•" non associative with precedence 60 for @{eclose ?}.
 317
 318 let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
 319  match i with
 320   [ pz ⇒ 〈 `∅, false 〉
 321   | pe ⇒ 〈 ϵ,  true 〉
 322   | ps x ⇒ 〈 `.x, false〉
 323   | pp x ⇒ 〈 `.x, false 〉
 324   | po i1 i2 ⇒ •i1 ⊕ •i2
 325   | pc i1 i2 ⇒ •i1 ▹ i2
 326   | pk i ⇒ 〈(\fst (•i))^*,true〉].
 327
 328 notation "• x" non associative with precedence 60 for @{'eclose $x}.
 329 interpretation "eclose" 'eclose x = (eclose ? x).
 330
 331 lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
 332   •(i1 + i2) = •i1 ⊕ •i2.
 333 // qed.
 334
 335 lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
 336   •(i1 · i2) = •i1 ▹ i2.
 337 // qed.
 338
 339 lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
 340   •i^* = 〈(\fst(•i))^*,true〉.
 341 // qed.
 342
 343 definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
 344   match e with
 345   [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
 346
 347 definition preclose ≝ λS. lift S (eclose S).
 348 interpretation "preclose" 'eclose x = (preclose ? x).
 349
 350 (* theorem 16: 2 *)
 351 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
 352   \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
 353 #S * #i1 #b1 * #i2 #b2 #w %
 354   [cases b1 cases b2 normalize /2/ * /3/ * /3/
 355   |cases b1 cases b2 normalize /2/ * /3/ * /3/
 356   ]
 357 qed.
 358
 359 lemma odot_true :
 360   ∀S.∀i1,i2:pitem S.
 361   〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
 362 // qed.
 363
 364 lemma odot_true_bis :
 365   ∀S.∀i1,i2:pitem S.
 366   〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
 367 #S #i1 #i2 normalize cases (•i2) // qed.
 368
 369 lemma odot_false:
 370   ∀S.∀i1,i2:pitem S.
 371   〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
 372 // qed.
 373
 374 lemma LcatE : ∀S.∀e1,e2:pitem S.
 375   \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
 376 // qed.
 377
 378 lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
 379 #S #i elim i //
 380   [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
 381     cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
 382   | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
 383     cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
 384   | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
 385   ]
 386 qed.
 387
 388 (*
 389 lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
 390   \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
 391 /2/ qed.
 392 *)
 393
 394 (* theorem 16: 1 → 3 *)
 395 lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
 396    \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
 397    \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 398 #S * #i1 #b1 #i2 cases b1
 399   [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
 400   |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
 401    >erase_bull @eqP_trans [|@(eqP_union_l … H)]
 402     @eqP_trans [|@eqP_union_l[|@union_comm ]]
 403     @eqP_trans [|@eqP_sym @union_assoc ] /3/
 404   ]
 405 qed.
 406
 407 lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
 408  \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
 409 #S #e #i #A #seme
 410 @eqP_trans [|@minus_eps_pre]
 411 @eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
 412 @eqP_trans [||@distribute_substract]
 413 @eqP_substract_r //
 414 qed.
 415
 416 (* theorem 16: 1 *)
 417 theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
 418 #S #e elim e
 419   [#w normalize % [/2/ | * //]
 420   |/2/
 421   |#x normalize #w % [ /2/ | * [@False_ind | //]]
 422   |#x normalize #w % [ /2/ | * // ]
 423   |#i1 #i2 #IH1 #IH2 >eclose_dot
 424    @eqP_trans [|@odot_dot_aux //] >sem_cat
 425    @eqP_trans
 426      [|@eqP_union_r
 427        [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
 428    @eqP_trans [|@union_assoc]
 429    @eqP_trans [||@eqP_sym @union_assoc]
 430    @eqP_union_l //
 431   |#i1 #i2 #IH1 #IH2 >eclose_plus
 432    @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
 433    @eqP_trans [|@(eqP_union_l … IH2)]
 434    @eqP_trans [|@eqP_sym @union_assoc]
 435    @eqP_trans [||@union_assoc] @eqP_union_r
 436    @eqP_trans [||@eqP_sym @union_assoc]
 437    @eqP_trans [||@eqP_union_l [|@union_comm]]
 438    @eqP_trans [||@union_assoc] /2/
 439   |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
 440    @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
 441    @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
 442    @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
 443    @eqP_sym @star_fix_eps
 444   ]
 445 qed.
 446
 447 (* blank item *)
 448 let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
 449  match i with
 450   [ z ⇒ `∅
 451   | e ⇒ ϵ
 452   | s y ⇒ `y
 453   | o e1 e2 ⇒ (blank S e1) + (blank S e2)
 454   | c e1 e2 ⇒ (blank S e1) · (blank S e2)
 455   | k e ⇒ (blank S e)^* ].
 456
 457 lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
 458 #S #e elim e normalize //
 459 qed.
 460
 461 lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
 462 #S #e elim e
 463   [1,2:@eq_to_ex_eq //
 464   |#s @eq_to_ex_eq //
 465   |#e1 #e2 #Hind1 #Hind2 >sem_cat
 466    @eqP_trans [||@(union_empty_r … ∅)]
 467    @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
 468    @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
 469   |#e1 #e2 #Hind1 #Hind2 >sem_plus
 470    @eqP_trans [||@(union_empty_r … ∅)]
 471    @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
 472   |#e #Hind >sem_star
 473    @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
 474   ]
 475 qed.
 476
 477 theorem re_embedding: ∀S.∀e:re S.
 478   \sem{•(blank S e)} =1 \sem{e}.
 479 #S #e @eqP_trans [|@sem_bull] >forget_blank
 480 @eqP_trans [|@eqP_union_r [|@sem_blank]]
 481 @eqP_trans [|@union_comm] @union_empty_r.
 482 qed.
 483
 484 (* lefted operations *)
 485 definition lifted_cat ≝ λS:DeqSet.λe:pre S.
 486   lift S (pre_concat_l S eclose e).
 487
 488 notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
 489
 490 interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
 491
 492 lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
 493   〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
 494 #S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
 495 qed.
 496
 497 lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
 498   〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
 499 //
 500 qed.
 501
 502 lemma erase_odot:∀S.∀e1,e2:pre S.
 503   |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
 504 #S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
 505 qed.
 506
 507 definition lk ≝ λS:DeqSet.λe:pre S.
 508   match e with
 509   [ mk_Prod i1 b1 ⇒
 510     match b1 with
 511     [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
 512     |false ⇒ 〈i1^*,false〉
 513     ]
 514   ].
 515
 516 (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
 517 interpretation "lk" 'lk a = (lk ? a).
 518 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 519
 520
 521 lemma ostar_true: ∀S.∀i:pitem S.
 522   〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
 523 // qed.
 524
 525 lemma ostar_false: ∀S.∀i:pitem S.
 526   〈i,false〉^⊛ = 〈i^*, false〉.
 527 // qed.
 528
 529 lemma erase_ostar: ∀S.∀e:pre S.
 530   |\fst (e^⊛)| = |\fst e|^*.
 531 #S * #i * // qed.
 532
 533 lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
 534   \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
 535 #S #e1 #i
 536 cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
 537 #H >H cases (e1 ▹ i) #i1 #b1 cases b1
 538   [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
 539    @eqP_union_l /2/
 540   |/2/
 541   ]
 542 qed.
 543
 544 lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
 545   e1 ⊙ 〈i,false〉 = e1 ▹ i.
 546 #S #e1 #i
 547 cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
 548 cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
 549 qed.
 550
 551 lemma sem_odot:
 552   ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
 553 #S #e1 * #i2 *
 554   [>sem_pre_true
 555    @eqP_trans [|@sem_odot_true]
 556    @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
 557   |>sem_pre_false >eq_odot_false @odot_dot_aux //
 558   ]
 559 qed.
 560
 561 (* theorem 16: 4 *)
 562 theorem sem_ostar: ∀S.∀e:pre S.
 563   \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
 564 #S * #i #b cases b
 565   [>sem_pre_true >sem_pre_true >sem_star >erase_bull
 566    @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
 567    @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
 568    @eqP_trans [||@eqP_sym @distr_cat_r]
 569    @eqP_trans [|@union_assoc] @eqP_union_l
 570    @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
 571   |>sem_pre_false >sem_pre_false >sem_star /2/
 572   ]
 573 qed.