matita/matita/lib/tutorial/chapter11.ma

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