2 Regular Expressions Equivalence
5 include "tutorial/chapter10.ma".
7 (* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and
10 definition cofinal ≝ λS.λp:(pre S)×(pre S).
11 snd ?? (fst ?? p) = snd ?? (snd ?? p).
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. *)
17 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
18 \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
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]
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. *)
33 definition occ ≝ λS.λe1,e2:pre S.
34 unique_append ? (occur S (|fst ?? e1|)) (occur S (|fst ?? e2|)).
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〉.
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 //]
46 (* The following is a stronger version of equiv_sem, relative to characters
47 occurring the given regular expressions. *)
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
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.
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.
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]
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).
77 (* We define an elimination principle for lists working on the tail, that we
78 be used in the sequel *)
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 //
87 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
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
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
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
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.
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.
125 Here is the extremely simple algorithm: *)
127 let rec bisim S l n (frontier,visited: list ?) on n ≝
129 [ O ⇒ 〈false,visited〉 (* assert false *)
132 [ nil ⇒ 〈true,visited〉
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)
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.
146 The following results explicitly state the behaviour of bisim is the general
147 case and in some relevant instances *)
149 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
150 bisim S l n frontier visited =
152 [ O ⇒ 〈false,visited〉 (* assert false *)
155 [ nil ⇒ 〈true,visited〉
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)
163 #S #l #n cases n // qed.
165 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
166 bisim S l O frontier visited = 〈false,visited〉.
167 #frontier #visited >unfold_bisim //
170 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
171 bisim Sig l (S m) [] visited = 〈true,visited〉.
172 #n #visisted >unfold_bisim //
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 //
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 //
189 (* In order to prove termination of bisim we must be able to effectively
190 enumerate all possible pres: *)
192 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
193 #b cases b normalize //
196 let rec pitem_enum S (i:re S) on i ≝
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)
206 lemma pitem_enum_complete : ∀S.∀i:pitem S.
207 memb (DeqItem S) i (pitem_enum S (|i|)) = true.
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)) //
216 definition pre_enum ≝ λS.λi:re S.
217 compose ??? (λi,b.〈i,b〉) ( pitem_enum S i) (true::false::[]).
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 //
225 definition space_enum ≝ λS.λi1,i2: re S.
226 compose ??? (λe1,e2.〈e1,e2〉) ( pre_enum S i1) (pre_enum S i2).
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〉))
233 definition all_reachable ≝ λS.λe1,e2:pre S.
234 λl: list (DeqProd (DeqProd ??) (DeqProd ??)).
236 ∀p. memb ? p l = true →
237 ∃w.(moves S w e1 = fst ?? p) ∧ (moves S w e2 = snd ?? p).
239 definition disjoint ≝ λS:DeqSet.λl1,l2.
240 ∀p:S. memb S p l1 = true → memb S p l2 = false.
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. *)
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
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]
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]
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
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
293 |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
294 |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
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
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 //
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 //
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. *)
319 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
320 (beqb (snd ?? (fst ?? p)) (snd ?? (snd ?? p)) = true).
322 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
323 memb ? x l1 = true → sublist ? (sons ? l x) l2.
325 lemma bisim_complete:
326 ∀S,l,n.∀frontier,visited,visited_res:list ?.
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.
332 [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
334 [(* case empty frontier *)
335 -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
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 //
353 |@memb_append_l2 @memb_cons //
355 |(* the only thing left to prove is the sub_sons invariant *)
356 #x #membx cases (orb_true_l … membx)
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 //|//]
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
372 |#H2 @memb_append_l2 @memb_cons @H2
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. *)
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〉::[]) []).
390 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
391 fst ?? (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
393 [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
394 cut (equiv ? re1 re2 = 〈true,snd ?? (equiv ? re1 re2)〉)
396 cases (bisim_complete … Hcut)
397 [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
398 #Hbisim #Hsub @(bisim_to_sem … Hbisim)
400 |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
401 [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
403 |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
404 |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
410 definition eqbnat ≝ λn,m:nat. eqb n m.
412 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
413 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
416 definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
418 definition a ≝ s DeqNat O.
419 definition b ≝ s DeqNat (S O).
420 definition c ≝ s DeqNat (S (S O)).
422 definition exp1 ≝ ((a·b)^*·a).
423 definition exp2 ≝ a·(b·a)^*.
424 definition exp4 ≝ (b·a)^*.
426 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
427 definition exp7 ≝ a · a^* · b^*.
429 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
430 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
432 example ex1 : fst ?? (equiv ? (exp8+exp9) exp9) = true.