matita/matita/lib/tutorial/chapter10.ma

   1 (*
   2 Regular Expressions Equivalence
   3 *)
   4
   5 include "tutorial/chapter9.ma".
   6
   7 (* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and
   8 only if b_1 = b_2. *)
   9
  10 definition cofinal ≝ λS.λp:(pre S)×(pre S).
  11   \snd (\fst p) = \snd (\snd p).
  12
  13 (* As a corollary of decidable_sem, we have that two expressions
  14 e1 and e2 are equivalent iff for any word w the states reachable
  15 through w are cofinal. *)
  16
  17 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
  18   \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
  19 #S #e1 #e2 %
  20 [#same_sem #w
  21   cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
  22     [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
  23   #Hcut @Hcut @iff_trans [|@decidable_sem]
  24   @iff_trans [|@same_sem] @iff_sym @decidable_sem
  25 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
  26 qed.
  27
  28 (* This does not directly imply decidability: we have no bound over the
  29 length of w; moreover, so far, we made no assumption over the cardinality
  30 of S. Instead of requiring S to be finite, we may restrict the analysis
  31 to characters occurring in the given pres. *)
  32
  33 definition occ ≝ λS.λe1,e2:pre S.
  34   unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
  35
  36 lemma occ_enough: ∀S.∀e1,e2:pre S.
  37 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
  38  →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
  39 #S #e1 #e2 #H #w
  40 cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
  41  >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
  42  >to_pit [2: @(not_to_not … H) #H1 #a #memba  @sublist_unique_append_l2 @H1 //]
  43  //
  44 qed.
  45
  46 (* The following is a stronger version of equiv_sem, relative to characters
  47 occurring the given regular expressions. *)
  48
  49 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
  50 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
  51 → \sem{e1}=1\sem{e2}.
  52 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
  53 qed.
  54
  55 (*
  56 Bisimulations
  57
  58
  59 We say that a list of pairs of pres is a bisimulation if it is closed
  60 w.r.t. moves, and all its members are cofinal.
  61 *)
  62
  63 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
  64  map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
  65
  66 lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
  67   ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
  68       move ? a (\fst (\snd q)) = \snd p).
  69 #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
  70 #a #tl #Hind #p #q #H cases (orb_true_l … H) -H
  71   [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
  72 qed.
  73
  74 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
  75   ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
  76
  77 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
  78
  79 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
  80   is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
  81 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
  82 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
  83 lapply Hsub @(list_elim_left … w) [//]
  84 #a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
  85   [#x #Hx @Hsub @memb_append_l1 //
  86   |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
  87    @(memb_map … occa)
  88   ]
  89 qed.
  90
  91 (* This is already an interesting result: checking if l is a bisimulation
  92 is decidable, hence we could generate l with some untrusted piece of code
  93 and then run a (boolean version of) is_bisim to check that it is actually
  94 a bisimulation.
  95 However, in order to prove that equivalence of regular expressions
  96 is decidable we must prove that we can always effectively build such a list
  97 (or find a counterexample).
  98 The idea is that the list we are interested in is just the set of
  99 all pair of pres reachable from the initial pair via some
 100 sequence of moves.
 101
 102 The algorithm for computing reachable nodes in graph is a very
 103 traditional one. We split nodes in two disjoint lists: a list of
 104 visited nodes and a frontier, composed by all nodes connected
 105 to a node in visited but not visited already. At each step we select a node
 106 a from the frontier, compute its sons, add a to the set of
 107 visited nodes and the (not already visited) sons to the frontier.
 108
 109 Instead of fist computing reachable nodes and then performing the
 110 bisimilarity test we can directly integrate it in the algorithm:
 111 the set of visited nodes is closed by construction w.r.t. reachability,
 112 so we have just to check cofinality for any node we add to visited.
 113
 114 Here is the extremely simple algorithm: *)
 115
 116 let rec bisim S l n (frontier,visited: list ?) on n ≝
 117   match n with
 118   [ O ⇒ 〈false,visited〉 (* assert false *)
 119   | S m ⇒
 120     match frontier with
 121     [ nil ⇒ 〈true,visited〉
 122     | cons hd tl ⇒
 123       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
 124         bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
 125         (sons S l hd)) tl) (hd::visited)
 126       else 〈false,visited〉
 127     ]
 128   ].
 129
 130 (* The integer n is an upper bound to the number of recursive call,
 131 equal to the dimension of the graph. It returns a pair composed
 132 by a boolean and a the set of visited nodes; the boolean is true
 133 if and only if all visited nodes are cofinal.
 134
 135 The following results explicitly state the behaviour of bisim is the general
 136 case and in some relevant instances *)
 137
 138 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
 139   bisim S l n frontier visited =
 140   match n with
 141   [ O ⇒ 〈false,visited〉 (* assert false *)
 142   | S m ⇒
 143     match frontier with
 144     [ nil ⇒ 〈true,visited〉
 145     | cons hd tl ⇒
 146       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
 147         bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
 148           (sons S l hd)) tl) (hd::visited)
 149       else 〈false,visited〉
 150     ]
 151   ].
 152 #S #l #n cases n // qed.
 153
 154 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
 155   bisim S l O frontier visited = 〈false,visited〉.
 156 #frontier #visited >unfold_bisim //
 157 qed.
 158
 159 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
 160   bisim Sig l (S m) [] visited = 〈true,visited〉.
 161 #n #visisted >unfold_bisim //
 162 qed.
 163
 164 lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
 165 beqb (\snd (\fst p)) (\snd (\snd p)) = true →
 166   bisim Sig l (S m) (p::frontier) visited =
 167   bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
 168     (sons Sig l p)) frontier) (p::visited).
 169 #Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?);  >test //
 170 qed.
 171
 172 lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
 173 beqb (\snd (\fst p)) (\snd (\snd p)) = false →
 174   bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
 175 #Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?); >test //
 176 qed.
 177
 178 (* In order to prove termination of bisim we must be able to effectively
 179 enumerate all possible pres: *)
 180
 181 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 182 #b cases b normalize //
 183 qed. *)
 184
 185 let rec pitem_enum S (i:re S) on i ≝
 186   match i with
 187   [ z ⇒ (pz S)::[]
 188   | e ⇒ (pe S)::[]
 189   | s y ⇒ (ps S y)::(pp S y)::[]
 190   | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
 191   | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
 192   | k i ⇒ map ?? (pk S) (pitem_enum S i)
 193   ].
 194
 195 lemma pitem_enum_complete : ∀S.∀i:pitem S.
 196   memb (DeqItem S) i (pitem_enum S (|i|)) = true.
 197 #S #i elim i
 198   [1,2://
 199   |3,4:#c normalize >(\b (refl … c)) //
 200   |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
 201   |#i #Hind @(memb_map (DeqItem S)) //
 202   ]
 203 qed.
 204
 205 definition pre_enum ≝ λS.λi:re S.
 206   compose ??? (λi,b.〈i,b〉) ( pitem_enum S i) (true::false::[]).
 207
 208 lemma pre_enum_complete : ∀S.∀e:pre S.
 209   memb ? e (pre_enum S (|\fst e|)) = true.
 210 #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
 211 // cases b normalize //
 212 qed.
 213
 214 definition space_enum ≝ λS.λi1,i2: re S.
 215   compose ??? (λe1,e2.〈e1,e2〉) ( pre_enum S i1) (pre_enum S i2).
 216
 217 lemma space_enum_complete : ∀S.∀e1,e2: pre S.
 218   memb ? 〈e1,e2〉 ( space_enum S (|\fst e1|) (|\fst e2|)) = true.
 219 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
 220 // qed.
 221
 222 definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?.
 223 uniqueb ? l = true ∧
 224   ∀p. memb ? p l = true →
 225     ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
 226
 227 definition disjoint ≝ λS:DeqSet.λl1,l2.
 228   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
 229
 230 (* We are ready to prove that bisim is correct; we use the invariant
 231 that at each call of bisim the two lists visited and frontier only contain
 232 nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair
 233 which is not cofinal. *)
 234
 235 lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
 236  ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
 237  |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
 238  all_reachable S e1 e2 visited →
 239  all_reachable S e1 e2 frontier →
 240  disjoint ? frontier visited →
 241  \fst (bisim S l n frontier visited) = true.
 242 #Sig #e1 #e2 #same #l #n elim n
 243   [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
 244    @le_to_not_lt @sublist_length // * #e11 #e21 #membp
 245    cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
 246    [|* #H1 #H2 <H1 <H2 @space_enum_complete]
 247    cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
 248   |#m #HI * [#visited #vinv #finv >bisim_end //]
 249    #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
 250    #disjoint
 251    cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
 252     [@(r_frontier … (memb_hd … ))] #rp
 253    cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
 254     [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
 255      @(proj1 … (equiv_sem … )) @same] #ptest
 256    >(bisim_step_true … ptest) @HI -HI
 257      [<plus_n_Sm //
 258      |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
 259         |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
 260         ]
 261      |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
 262       @unique_append_elim #q #H
 263        [cases (memb_sons … (memb_filter_memb … H)) -H
 264         #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@(a::[])))
 265         >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
 266        |@r_frontier @memb_cons //
 267        ]
 268      |@unique_append_elim #q #H
 269        [@injective_notb @(memb_filter_true … H)
 270        |cut ((q==p) = false)
 271          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
 272         cases (andb_true … u_frontier) #notp #_ @(\bf ?)
 273         @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
 274        ]
 275      ]
 276    ]
 277 qed.
 278
 279 (* For completeness, we use the invariant that all the nodes in visited are cofinal,
 280 and the sons of visited are either in visited or in the frontier; since
 281 at the end frontier is empty, visited is hence a bisimulation. *)
 282
 283 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
 284   (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
 285
 286 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
 287 memb ? x l1 = true → sublist ? (sons ? l x) l2.
 288
 289 lemma bisim_complete:
 290  ∀S,l,n.∀frontier,visited,visited_res:list ?.
 291  all_true S visited →
 292  sub_sons S l visited (frontier@visited) →
 293  bisim S l n frontier visited = 〈true,visited_res〉 →
 294  is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
 295 #S #l #n elim n
 296   [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
 297   |#m #Hind *
 298     [(* case empty frontier *)
 299      -Hind #vis #vis_res #allv #H normalize in  ⊢ (%→?);
 300      #H1 destruct % #p
 301       [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
 302     |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
 303       [|(* case head of the frontier is non ok (absurd) *)
 304        #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
 305      (* frontier = hd:: tl and hd is ok *)
 306      #H #tl #visited #visited_res #allv >(bisim_step_true … H)
 307      (* new_visited = hd::visited are all ok *)
 308      cut (all_true S (hd::visited))
 309       [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
 310      (* we now exploit the induction hypothesis *)
 311      #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
 312       [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
 313         [cases (orb_true_l … membp) -membp #membp
 314           [@memb_append_l2 >(\P membp) @memb_hd
 315           |@memb_append_l1 @sublist_unique_append_l2 //
 316           ]
 317         |@memb_append_l2 @memb_cons //
 318         ]
 319       |(* the only thing left to prove is the sub_sons invariant *)
 320      #x #membx cases (orb_true_l … membx)
 321       [(* case x = hd *)
 322        #eqhdx <(\P eqhdx) #xa #membxa
 323        (* xa is a son of x; we must distinguish the case xa
 324         was already visited form the case xa is new *)
 325        cases (true_or_false … (memb ? xa (x::visited)))
 326         [(* xa visited - trivial *) #membxa @memb_append_l2 //
 327         |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
 328           [>membxa //|//]
 329         ]
 330       |(* case x in visited *)
 331        #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
 332         [#H2 (cases (orb_true_l … H2))
 333           [#H3 @memb_append_l2 <(\P H3) @memb_hd
 334           |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
 335           ]
 336         |#H2 @memb_append_l2 @memb_cons @H2
 337         ]
 338       ]
 339     ]
 340   ]
 341 qed.
 342
 343 (* We can now give the definition of the equivalence algorithm, and
 344 prove that two expressions are equivalente if and only if they define
 345 the same language. *)
 346
 347 definition equiv ≝ λSig.λre1,re2:re Sig.
 348   let e1 ≝ •(blank ? re1) in
 349   let e2 ≝ •(blank ? re2) in
 350   let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
 351   let sig ≝ (occ Sig e1 e2) in
 352   (bisim ? sig n (〈e1,e2〉::[]) []).
 353
 354 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
 355    \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
 356 #Sig #re1 #re2 %
 357   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
 358    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
 359      [<H //] #Hcut
 360    cases (bisim_complete … Hcut)
 361      [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
 362    #Hbisim #Hsub @(bisim_to_sem … Hbisim)
 363    @Hsub @memb_hd
 364   |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
 365     [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
 366     |//
 367     |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
 368     |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
 369     |#p #_ normalize //
 370     ]
 371   ]
 372 qed.
 373
 374 definition eqbnat ≝ λn,m:nat. eqb n m.
 375
 376 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
 377 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
 378 qed.
 379
 380 definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
 381
 382 definition a ≝ s DeqNat O.
 383 definition b ≝ s DeqNat (S O).
 384 definition c ≝ s DeqNat (S (S O)).
 385
 386 definition exp1 ≝ ((a·b)^*·a).
 387 definition exp2 ≝ a·(b·a)^*.
 388 definition exp4 ≝ (b·a)^*.
 389
 390 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
 391 definition exp7 ≝ a · a^* · b^*.
 392
 393 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
 394 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
 395
 396 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
 397 normalize // qed.