1 (* We shall apply all the previous machinery to the study of regular languages
2 and the constructions of the associated finite automata. *)
4 include "tutorial/chapter6.ma".
6 (* The type re of regular expressions over an alphabet $S$ is the smallest
7 collection of objects generated by the following constructors: *)
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* *)
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).
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).
26 notation "`∅" non associative with precedence 90 for @{ 'empty }.
27 interpretation "empty" 'empty = (z ?).
29 (* The language sem{e} associated with the regular expression e is inductively
30 defined by the following function: *)
32 let rec in_l (S :
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"
\ 6\ 5/span
\ 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\ 5span class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"
\ 6\ 5/span
\ 6 S → Prop ≝
34 [ z ⇒
\ 5a title="empty set" href="cic:/fakeuri.def(1)"
\ 6∅
\ 5/a
\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"
\ 6\ 5/span
\ 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\ 5span class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"
\ 6\ 5/span
\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6\ 5span class="error" title="Parse error: [term] expected after [sym[] (in [term])"
\ 6\ 5/span
\ 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*].
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).
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*.
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
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
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. *)
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 *)
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. *)
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.
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 ?).
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. *)
108 let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
114 | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
115 | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
116 | pk E ⇒ (forget ? E)^* ].
118 (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
119 interpretation "forget" 'norm a = (forget ? a).
121 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
124 lemma erase_plus : ∀S.∀i1,i2:pitem S.
125 |i1 + i2| = |i1| + |i2|.
128 lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
131 (* Items and pres are very concrete datatypes: they can be effectively compared,
132 and enumerated. In particular, we can define a boolean equality beqitem and a proof
133 beqitem_true that it refects propositional equality, enriching the set (pitem S)
136 let rec beqitem S (i1,i2: pitem S) on i1 ≝
138 [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
139 | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
140 | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
141 | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
142 | po i11 i12 ⇒ match i2 with
143 [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
145 | pc i11 i12 ⇒ match i2 with
146 [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
148 | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
151 lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
153 [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
154 |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
155 |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
156 [>(\P H) // | @(\b (refl …))]
157 |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
158 [>(\P H) // | @(\b (refl …))]
159 |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
160 normalize #H destruct
161 [cases (true_or_false (beqitem S i11 i21)) #H1
162 [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
163 |>H1 in H; normalize #abs @False_ind /2/
165 |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
167 |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
168 normalize #H destruct
169 [cases (true_or_false (beqitem S i11 i21)) #H1
170 [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
171 |>H1 in H; normalize #abs @False_ind /2/
173 |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
175 |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
176 normalize #H destruct
177 [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
181 definition DeqItem ≝ λS.
182 mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
184 (* We also add a couple of unification hints to allow the type inference system
185 to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
186 equality function of a DeqSet. *)
188 unification hint 0 ≔ S;
189 X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
190 (* ---------------------------------------- *) ⊢
193 unification hint 0 ≔ S,i1,i2;
194 X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
195 (* ---------------------------------------- *) ⊢
196 beqitem S i1 i2 ≡ eqb X i1 i2.
198 (* The intuitive semantic of a point is to mark the position where
199 we should start reading the regular expression. The language associated
200 to a pre is the union of the languages associated with its points. *)
202 let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
208 | pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
209 | po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
210 | pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
212 interpretation "in_pl" 'in_l E = (in_pl ? E).
213 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
215 definition in_prl ≝ λS : DeqSet.λp:pre S.
216 if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
218 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
219 interpretation "in_prl" 'in_l E = (in_prl ? E).
221 (* The following, trivial lemmas are only meant for rewriting purposes. *)
223 lemma sem_pre_true : ∀S.∀i:pitem S.
224 \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
227 lemma sem_pre_false : ∀S.∀i:pitem S.
228 \sem{〈i,false〉} = \sem{i}.
231 lemma sem_cat: ∀S.∀i1,i2:pitem S.
232 \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
235 lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
236 \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
239 lemma sem_plus: ∀S.∀i1,i2:pitem S.
240 \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
243 lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
244 \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
247 lemma sem_star : ∀S.∀i:pitem S.
248 \sem{i^*} = \sem{i} · \sem{|i|}^*.
251 lemma sem_star_w : ∀S.∀i:pitem S.∀w.
252 \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
255 (* Below are a few, simple, semantic properties of items. In particular:
256 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
257 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
258 - minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
259 - minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
260 The first property is proved by a simple induction on $i$; the other
261 results are easy corollaries. We need an auxiliary lemma first. *)
263 lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
264 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
266 lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
267 #S #e elim e normalize /2/
268 [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
269 >(append_eq_nil …H…) /2/
270 |#r1 #r2 #n1 #n2 % * /2/
271 |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
275 lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
276 #S * #i #b cases b // normalize #H @False_ind /2/
279 lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
280 #S * #i #b #btrue normalize in btrue; >btrue %2 //
283 lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
285 [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
290 lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
292 [>sem_pre_true normalize in ⊢ (??%?); #w %
293 [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
294 |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
298 definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
299 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
300 interpretation "oplus" 'oplus a b = (lo ? a b).
302 lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
305 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
306 match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
308 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
309 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
311 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
313 #S #A #B #H >H /2/ qed.
315 lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
316 \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
317 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
318 >sem_pre_true >sem_cat >sem_pre_true /2/
321 definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
323 [ mk_Prod i1 b1 ⇒ match b1 with
324 [ true ⇒ (i1 ◃ (bcast ? i2))
325 | false ⇒ 〈i1 · i2,false〉
329 notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
330 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
332 notation "•" non associative with precedence 60 for @{eclose ?}.
334 let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
338 | ps x ⇒ 〈 `.x, false〉
339 | pp x ⇒ 〈 `.x, false 〉
340 | po i1 i2 ⇒ •i1 ⊕ •i2
341 | pc i1 i2 ⇒ •i1 ▹ i2
342 | pk i ⇒ 〈(\fst (•i))^*,true〉].
344 notation "• x" non associative with precedence 60 for @{'eclose $x}.
345 interpretation "eclose" 'eclose x = (eclose ? x).
347 lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
348 •(i1 + i2) = •i1 ⊕ •i2.
351 lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
352 •(i1 · i2) = •i1 ▹ i2.
355 lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
356 •i^* = 〈(\fst(•i))^*,true〉.
359 definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
361 [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
363 definition preclose ≝ λS. lift S (eclose S).
364 interpretation "preclose" 'eclose x = (preclose ? x).
367 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
368 \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
369 #S * #i1 #b1 * #i2 #b2 #w %
370 [cases b1 cases b2 normalize /2/ * /3/ * /3/
371 |cases b1 cases b2 normalize /2/ * /3/ * /3/
377 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
380 lemma odot_true_bis :
382 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
383 #S #i1 #i2 normalize cases (•i2) // qed.
387 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
390 lemma LcatE : ∀S.∀e1,e2:pitem S.
391 \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
394 lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
396 [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
397 cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
398 | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
399 cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
400 | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
405 lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
406 \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
410 (* theorem 16: 1 → 3 *)
411 lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
412 \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
413 \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
414 #S * #i1 #b1 #i2 cases b1
415 [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
416 |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
417 >erase_bull @eqP_trans [|@(eqP_union_l … H)]
418 @eqP_trans [|@eqP_union_l[|@union_comm ]]
419 @eqP_trans [|@eqP_sym @union_assoc ] /3/
423 lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
424 \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
426 @eqP_trans [|@minus_eps_pre]
427 @eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
428 @eqP_trans [||@distribute_substract]
433 theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
435 [#w normalize % [/2/ | * //]
437 |#x normalize #w % [ /2/ | * [@False_ind | //]]
438 |#x normalize #w % [ /2/ | * // ]
439 |#i1 #i2 #IH1 #IH2 >eclose_dot
440 @eqP_trans [|@odot_dot_aux //] >sem_cat
443 [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
444 @eqP_trans [|@union_assoc]
445 @eqP_trans [||@eqP_sym @union_assoc]
447 |#i1 #i2 #IH1 #IH2 >eclose_plus
448 @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
449 @eqP_trans [|@(eqP_union_l … IH2)]
450 @eqP_trans [|@eqP_sym @union_assoc]
451 @eqP_trans [||@union_assoc] @eqP_union_r
452 @eqP_trans [||@eqP_sym @union_assoc]
453 @eqP_trans [||@eqP_union_l [|@union_comm]]
454 @eqP_trans [||@union_assoc] /2/
455 |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
456 @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
457 @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
458 @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
459 @eqP_sym @star_fix_eps
464 let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
469 | o e1 e2 ⇒ (blank S e1) + (blank S e2)
470 | c e1 e2 ⇒ (blank S e1) · (blank S e2)
471 | k e ⇒ (blank S e)^* ].
473 lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
474 #S #e elim e normalize //
477 lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
481 |#e1 #e2 #Hind1 #Hind2 >sem_cat
482 @eqP_trans [||@(union_empty_r … ∅)]
483 @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
484 @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
485 |#e1 #e2 #Hind1 #Hind2 >sem_plus
486 @eqP_trans [||@(union_empty_r … ∅)]
487 @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
489 @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
493 theorem re_embedding: ∀S.∀e:re S.
494 \sem{•(blank S e)} =1 \sem{e}.
495 #S #e @eqP_trans [|@sem_bull] >forget_blank
496 @eqP_trans [|@eqP_union_r [|@sem_blank]]
497 @eqP_trans [|@union_comm] @union_empty_r.
500 (* lefted operations *)
501 definition lifted_cat ≝ λS:DeqSet.λe:pre S.
502 lift S (pre_concat_l S eclose e).
504 notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
506 interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
508 lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
509 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
510 #S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
513 lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
514 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
518 lemma erase_odot:∀S.∀e1,e2:pre S.
519 |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
520 #S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
523 definition lk ≝ λS:DeqSet.λe:pre S.
527 [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
528 |false ⇒ 〈i1^*,false〉
532 (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
533 interpretation "lk" 'lk a = (lk ? a).
534 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
537 lemma ostar_true: ∀S.∀i:pitem S.
538 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
541 lemma ostar_false: ∀S.∀i:pitem S.
542 〈i,false〉^⊛ = 〈i^*, false〉.
545 lemma erase_ostar: ∀S.∀e:pre S.
546 |\fst (e^⊛)| = |\fst e|^*.
549 lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
550 \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
552 cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
553 #H >H cases (e1 ▹ i) #i1 #b1 cases b1
554 [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
560 lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
561 e1 ⊙ 〈i,false〉 = e1 ▹ i.
563 cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
564 cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
568 ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
571 @eqP_trans [|@sem_odot_true]
572 @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
573 |>sem_pre_false >eq_odot_false @odot_dot_aux //
578 theorem sem_ostar: ∀S.∀e:pre S.
579 \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
581 [>sem_pre_true >sem_pre_true >sem_star >erase_bull
582 @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
583 @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
584 @eqP_trans [||@eqP_sym @distr_cat_r]
585 @eqP_trans [|@union_assoc] @eqP_union_l
586 @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
587 |>sem_pre_false >sem_pre_false >sem_star /2/