weblib/tutorial/chapter8.ma

   1 (*
   2 \ 5h1\ 6Broadcasting points\ 5/h1\ 6
   3 Intuitively, a regular expression e must be understood as a pointed expression with a single
   4 point in front of it. Since however we only allow points before symbols, we must broadcast
   5 this initial point inside e traversing all nullable subexpressions, that essentially corresponds
   6 to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
   7 its definition is the expected one: let us start discussing an example.
   8
   9 \ 5b\ 6Example\ 5/b\ 6
  10 Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the
  11 first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence
  12 reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in
  13 parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the
  14 star, and to traverse it, stopping in front of a; the second point just stops in front of b.
  15 No point reached that end of b^*a + b hence no further propagation is possible. In conclusion:
  16                •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
  17 *)
  18
  19 include "tutorial/chapter7.ma".
  20
  21 (* Broadcasting a point inside an item generates a pre, since the point could possibly reach
  22 the end of the expression.
  23 Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
  24 If we define
  25                  〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
  26 then, we just have •(i1+i2) = •(i1)⊕ •(i2).
  27 *)
  28
  29 include "tutorial/chapter7.ma".
  30
  31 definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
  32 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
  33 interpretation "oplus" 'oplus a b = (lo ? a b).
  34
  35 lemma lo_def: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b1,b2. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,b1〉\ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b2〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1\ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i2,b1\ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6b2〉.
  36 // qed.
  37
  38 (*
  39 Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2
  40 we should start broadcasting it inside i1 and then proceed into i2 if and only if a
  41 point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where
  42 e ▹ i is a general operation of concatenation between a pre and an item, defined by
  43 cases on the boolean in e:
  44
  45        〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
  46        〈i1,false〉 ▹ i2 = i1 · i2
  47 In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
  48         i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
  49 Let us come to the formalized definitions:
  50 *)
  51
  52 definition pre_concat_r ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λi:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
  53   match e with [ mk_Prod i1 b ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i1, b〉].
  54
  55 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
  56 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
  57
  58 lemma eq_to_ex_eq: ∀S.∀A,B:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
  59   A \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 B → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B.
  60 #S #A #B #H >H #x % // qed.
  61
  62 (* The behaviour of \triangleleft is summarized by the following, easy lemma: *)
  63
  64 lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
  65   \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
  66 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
  67 >sem_pre_true >sem_cat >sem_pre_true /2/
  68 qed.
  69
  70 (* The definition of $\bullet(-)$ (\verb+eclose+) and
  71 $\triangleright$ (\verb+pre_concat_l+) are mutually recursive.
  72 In this situation, a viable alternative that is usually simpler
  73 to reason about, is to abstract one of the two functions with respect
  74 to the other. We make the notation declarations explicit in this
  75 case, for the sake of clarity.
  76 *)
  77
  78 definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
  79   match e1 with
  80   [ mk_Prod i1 b1 ⇒ match b1 with
  81     [ true ⇒ (i1 ◃ (bcast ? i2))
  82     | false ⇒ 〈i1 · i2,false〉
  83     ]
  84   ].
  85
  86 notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
  87 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
  88
  89 (* We are ready to give the formal definition of the broadcasting operation. *)
  90
  91 notation "•" non associative with precedence 60 for @{eclose ?}.
  92
  93 let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
  94  match i with
  95   [ pz ⇒ 〈 `∅, false 〉
  96   | pe ⇒ 〈 ϵ,  true 〉
  97   | ps x ⇒ 〈 `.x, false〉
  98   | pp x ⇒ 〈 `.x, false 〉
  99   | po i1 i2 ⇒ •i1 ⊕ •i2
 100   | pc i1 i2 ⇒ •i1 ▹ i2
 101   | pk i ⇒ 〈(\fst (•i))^*,true〉].
 102
 103 notation "• x" non associative with precedence 60 for @{'eclose $x}.
 104 interpretation "eclose" 'eclose x = (eclose ? x).
 105
 106 (* Here are a few simple properties of •(-) *)
 107
 108 lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
 109   •(i1 + i2) = •i1 ⊕ •i2.
 110 // qed.
 111
 112 lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
 113   •(i1 · i2) = •i1 ▹ i2.
 114 // qed.
 115
 116 lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
 117   •i^* = 〈(\fst(•i))^*,true〉.
 118 // qed.
 119
 120 (* The definition of •(-) (eclose) can then be lifted from items to pres
 121 in the obvious way. *)
 122
 123 definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
 124   match e with
 125   [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
 126
 127 definition preclose ≝ λS. lift S (eclose S).
 128 interpretation "preclose" 'eclose x = (preclose ? x).
 129
 130 (* Obviously, broadcasting does not change the carrier of the item,
 131 as it is easily proved by structural induction. *)
 132
 133 lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
 134 #S #i elim i //
 135   [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
 136     cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
 137   | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
 138     cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
 139   | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
 140   ]
 141 qed.
 142
 143 (* We are now ready to state the main semantic properties of $\oplus,
 144 \triangleleft$ and $\bullet(-)$:
 145
 146 \begin{lstlisting}[language=grafite]
 147 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
 148   \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
 149 lemma sem_pcl : ∀S.∀e1:pre S.∀i2:pitem S.
 150   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 151 theorem sem_bullet: ∀S:DeqSet. ∀i:pitem S.
 152   \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
 153 \end{lstlisting}
 154 The proof of \verb+sem_oplus+ is straightforward. *)
 155
 156 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
 157   \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
 158 #S * #i1 #b1 * #i2 #b2 #w %
 159   [cases b1 cases b2 normalize /2/ * /3/ * /3/
 160   |cases b1 cases b2 normalize /2/ * /3/ * /3/
 161   ]
 162 qed.
 163
 164 (* For the others, we proceed as follow: we first prove the following
 165 auxiliary lemma, that assumes sem_bullet:
 166
 167 lemma sem_pcl_aux: ∀S.∀e1:pre S.∀i2:pitem S.
 168    \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
 169    \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 170
 171 Then, using the previous result, we prove sem_bullet by induction
 172 on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
 173
 174 lemma LcatE : ∀S.∀e1,e2:pitem S.
 175   \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
 176 // qed.
 177
 178 lemma sem_pcl_aux : ∀S.∀e1:pre S.∀i2:pitem S.
 179    \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
 180    \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 181 #S * #i1 #b1 #i2 cases b1
 182   [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
 183   |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
 184    >erase_bull @eqP_trans [|@(eqP_union_l … H)]
 185     @eqP_trans [|@eqP_union_l[|@union_comm ]]
 186     @eqP_trans [|@eqP_sym @union_assoc ] /3/
 187   ]
 188 qed.
 189
 190 lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
 191  \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
 192 #S #e #i #A #seme
 193 @eqP_trans [|@minus_eps_pre]
 194 @eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
 195 @eqP_trans [||@distribute_substract]
 196 @eqP_substract_r //
 197 qed.
 198
 199 (* theorem 16: 1 *)
 200 theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
 201 #S #e elim e
 202   [#w normalize % [/2/ | * //]
 203   |/2/
 204   |#x normalize #w % [ /2/ | * [@False_ind | //]]
 205   |#x normalize #w % [ /2/ | * // ]
 206   |#i1 #i2 #IH1 #IH2 >eclose_dot
 207    @eqP_trans [|@odot_dot_aux //] >sem_cat
 208    @eqP_trans
 209      [|@eqP_union_r
 210        [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
 211    @eqP_trans [|@union_assoc]
 212    @eqP_trans [||@eqP_sym @union_assoc]
 213    @eqP_union_l //
 214   |#i1 #i2 #IH1 #IH2 >eclose_plus
 215    @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
 216    @eqP_trans [|@(eqP_union_l … IH2)]
 217    @eqP_trans [|@eqP_sym @union_assoc]
 218    @eqP_trans [||@union_assoc] @eqP_union_r
 219    @eqP_trans [||@eqP_sym @union_assoc]
 220    @eqP_trans [||@eqP_union_l [|@union_comm]]
 221    @eqP_trans [||@union_assoc] /2/
 222   |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
 223    @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
 224    @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
 225    @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
 226    @eqP_sym @star_fix_eps
 227   ]
 228 qed.
 229
 230 (* blank item *)
 231 let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
 232  match i with
 233   [ z ⇒ `∅
 234   | e ⇒ ϵ
 235   | s y ⇒ `y
 236   | o e1 e2 ⇒ (blank S e1) + (blank S e2)
 237   | c e1 e2 ⇒ (blank S e1) · (blank S e2)
 238   | k e ⇒ (blank S e)^* ].
 239
 240 lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
 241 #S #e elim e normalize //
 242 qed.
 243
 244 lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
 245 #S #e elim e
 246   [1,2:@eq_to_ex_eq //
 247   |#s @eq_to_ex_eq //
 248   |#e1 #e2 #Hind1 #Hind2 >sem_cat
 249    @eqP_trans [||@(union_empty_r … ∅)]
 250    @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
 251    @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
 252   |#e1 #e2 #Hind1 #Hind2 >sem_plus
 253    @eqP_trans [||@(union_empty_r … ∅)]
 254    @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
 255   |#e #Hind >sem_star
 256    @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
 257   ]
 258 qed.
 259
 260 theorem re_embedding: ∀S.∀e:re S.
 261   \sem{•(blank S e)} =1 \sem{e}.
 262 #S #e @eqP_trans [|@sem_bull] >forget_blank
 263 @eqP_trans [|@eqP_union_r [|@sem_blank]]
 264 @eqP_trans [|@union_comm] @union_empty_r.
 265 qed.
 266
 267 (* lefted operations *)
 268 definition lifted_cat ≝ λS:DeqSet.λe:pre S.
 269   lift S (pre_concat_l S eclose e).
 270
 271 notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
 272
 273 interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
 274
 275 lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
 276   〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
 277 #S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
 278 qed.
 279
 280 lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
 281   〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
 282 //
 283 qed.
 284
 285 lemma erase_odot:∀S.∀e1,e2:pre S.
 286   |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
 287 #S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
 288 qed.
 289
 290 definition lk ≝ λS:DeqSet.λe:pre S.
 291   match e with
 292   [ mk_Prod i1 b1 ⇒
 293     match b1 with
 294     [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
 295     |false ⇒ 〈i1^*,false〉
 296     ]
 297   ].
 298
 299 (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
 300 interpretation "lk" 'lk a = (lk ? a).
 301 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 302
 303
 304 lemma ostar_true: ∀S.∀i:pitem S.
 305   〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
 306 // qed.
 307
 308 lemma ostar_false: ∀S.∀i:pitem S.
 309   〈i,false〉^⊛ = 〈i^*, false〉.
 310 // qed.
 311
 312 lemma erase_ostar: ∀S.∀e:pre S.
 313   |\fst (e^⊛)| = |\fst e|^*.
 314 #S * #i * // qed.
 315
 316 lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
 317   \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
 318 #S #e1 #i
 319 cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
 320 #H >H cases (e1 ▹ i) #i1 #b1 cases b1
 321   [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
 322    @eqP_union_l /2/
 323   |/2/
 324   ]
 325 qed.
 326
 327 lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
 328   e1 ⊙ 〈i,false〉 = e1 ▹ i.
 329 #S #e1 #i
 330 cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
 331 cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
 332 qed.
 333
 334 lemma sem_odot:
 335   ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
 336 #S #e1 * #i2 *
 337   [>sem_pre_true
 338    @eqP_trans [|@sem_odot_true]
 339    @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
 340   |>sem_pre_false >eq_odot_false @odot_dot_aux //
 341   ]
 342 qed.
 343
 344 (* theorem 16: 4 *)
 345 theorem sem_ostar: ∀S.∀e:pre S.
 346   \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
 347 #S * #i #b cases b
 348   [>sem_pre_true >sem_pre_true >sem_star >erase_bull
 349    @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
 350    @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
 351    @eqP_trans [||@eqP_sym @distr_cat_r]
 352    @eqP_trans [|@union_assoc] @eqP_union_l
 353    @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
 354   |>sem_pre_false >sem_pre_false >sem_star /2/
 355   ]
 356 qed.