1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
16 include "basics/lists/listb.ma".
21 We now define the move operation, that corresponds to the advancement of the
22 state in response to the processing of an input character a. The intuition is
23 clear: we have to look at points inside $e$ preceding the given character a,
24 let the point traverse the character, and broadcast it. All other points must
27 We can give a particularly elegant definition in terms of the
28 lifted operators of the previous section:
31 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
35 | ps y ⇒ 〈 `y, false 〉
36 | pp y ⇒ 〈 `y, x == y 〉
37 | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
38 | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
39 | pk e ⇒ (move ? x e)^⊛ ].
41 lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
42 move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
45 lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
46 move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
49 lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
50 move S x i^* = (move ? x i)^⊛.
53 definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
55 lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.
56 pmove ? x 〈i,b〉 = move ? x i.
59 lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b.
60 a::l1 = b::l2 → a = b.
61 #A #l1 #l2 #a #b #H destruct //
64 lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
65 |\fst (move ? a i)| = |i|.
67 [#i1 #i2 >move_cat #H1 #H2 whd in ⊢ (???%); <H1 <H2 //
68 |#i1 #i2 >move_plus #H1 #H2 whd in ⊢ (???%); <H1 <H2 //
73 ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S.
74 \sem{move ? a i} w ↔ \sem{i} (a::w).
79 |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
80 [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
81 |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
84 (* lhs = w∈\sem{move S a (i1·i2)} *)
86 (* lhs = w∈\sem{move S a i1}⊙\sem{move S a i2} *)
87 @iff_trans[|@sem_odot] >same_kernel
88 (* lhs = w∈\sem{move S a i1}·\sem{|i2|} ∨ a∈\sem{move S a i2} *)
89 (* now we work on the rhs, that is
90 rhs = a::w1∈\sem{i1·i2} *)
92 (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
93 @iff_trans[||@(iff_or_l … (HI2 w))]
94 (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
97 (* we are left to prove that
98 w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
99 we use deriv_middot on the rhs *)
100 @iff_trans[||@iff_sym @deriv_middot //]
101 (* w∈\sem{move S a i1}·\sem{|i2|} ↔ w∈(deriv S \sem{i1} a) · \sem{|i2|} *)
103 |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
104 @iff_trans[|@sem_oplus]
105 @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
106 |#i1 #HI1 #w >move_star
107 @iff_trans[|@sem_ostar] >same_kernel >sem_star_w
108 @iff_trans[||@iff_sym @deriv_middot //]
113 notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}.
114 let rec moves (S : DeqSet) w e on w : pre S ≝
117 | cons x w' ⇒ w' ↦* (move S x (\fst e))].
119 lemma moves_empty: ∀S:DeqSet.∀e:pre S.
123 lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
124 moves ? (a::w) e = moves ? w (move S a (\fst e)).
127 lemma moves_left : ∀S,a,w,e.
128 moves S (w@[a]) e = move S a (\fst (moves S w e)).
129 #S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
132 lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
133 iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
134 #S #a #w * #i #b cases b normalize
135 [% /2/ * // #H destruct |% normalize /2/]
138 lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
139 |\fst (moves ? w e)| = |\fst e|.
143 theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
144 (\snd (moves ? w e) = true) ↔ \sem{e} w.
146 [* #i #b >moves_empty cases b % /2/
147 |#a #w1 #Hind #e >moves_cons
148 check not_epsilon_sem
149 @iff_trans [||@iff_sym @not_epsilon_sem]
150 @iff_trans [||@move_ok] @Hind
154 (************************ pit state ***************************)
155 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
157 let rec occur (S: DeqSet) (i: re S) on i ≝
162 | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
163 | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
166 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
167 move S a i = pit_pre S i.
169 [#x normalize cases (a==x) normalize // #H @False_ind /2/
170 |#i1 #i2 #Hind1 #Hind2 #H >move_cat
171 >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
172 >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
173 |#i1 #i2 #Hind1 #Hind2 #H >move_plus
174 >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
175 >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
176 |#i #Hind #H >move_star >Hind //
180 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
182 [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
183 |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
184 |#i #Hind >move_star >Hind //
188 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
189 #S #w #i elim w // #a #tl >moves_cons //
192 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
193 moves S w e = pit_pre S (\fst e).
195 [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
196 |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
197 [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
198 @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
199 [#H2 >(\P H2) // |#H2 @H1 //]
200 |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
206 definition cofinal ≝ λS.λp:(pre S)×(pre S).
207 \snd (\fst p) = \snd (\snd p).
209 (* As a corollary of decidable_sem, we have that two expressions
210 e1 and e2 are equivalent iff for any word w the states reachable
211 through w are cofinal. *)
213 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
214 \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
217 cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
218 [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
219 #Hcut @Hcut @iff_trans [|@decidable_sem]
220 @iff_trans [|@same_sem] @iff_sym @decidable_sem
221 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
224 (* This does not directly imply decidability: we have no bound over the
225 length of w; moreover, so far, we made no assumption over the cardinality
226 of S. Instead of requiring S to be finite, we may restrict the analysis
227 to characters occurring in the given pres. *)
229 definition occ ≝ λS.λe1,e2:pre S.
230 unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
232 lemma occ_enough: ∀S.∀e1,e2:pre S.
233 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
234 →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
236 cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
237 >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
238 >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //]
242 (* The following is a stronger version of equiv_sem, relative to characters
243 occurring the given regular expressions. *)
245 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
246 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
248 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
252 We say that a list of pairs of pres is a bisimulation if it is closed
253 w.r.t. moves, and all its members are cofinal.
256 (* the sons of p w.r.t a list of symbols l are all states reachable from p
259 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
260 map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
262 lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
263 ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
264 move ? a (\fst (\snd q)) = \snd p).
265 #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
266 #a #tl #Hind #p #q #H cases (orb_true_l … H) -H
267 [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
270 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
271 ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
273 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
275 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
276 is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}≐\sem{e2}.
277 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
278 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
279 lapply Hsub @(list_elim_left … w) [//]
280 #a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
281 [#x #Hx @Hsub @memb_append_l1 //
282 |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
287 (* This is already an interesting result: checking if l is a bisimulation
288 is decidable, hence we could generate l with some untrusted piece of code
289 and then run a (boolean version of) is_bisim to check that it is actually
291 However, in order to prove that equivalence of regular expressions
292 is decidable we must prove that we can always effectively build such a list
293 (or find a counterexample).
294 The idea is that the list we are interested in is just the set of
295 all pair of pres reachable from the initial pair via some
298 The algorithm for computing reachable nodes in graph is a very
299 traditional one. We split nodes in two disjoint lists: a list of
300 visited nodes and a frontier, composed by all nodes connected
301 to a node in visited but not visited already. At each step we select a node
302 a from the frontier, compute its sons, add a to the set of
303 visited nodes and the (not already visited) sons to the frontier.
305 Instead of fist computing reachable nodes and then performing the
306 bisimilarity test we can directly integrate it in the algorithm:
307 the set of visited nodes is closed by construction w.r.t. reachability,
308 so we have just to check cofinality for any node we add to visited.
310 Here is the extremely simple algorithm: *)
312 let rec bisim S l n (frontier,visited: list ?) on n ≝
314 [ O ⇒ 〈false,visited〉 (* assert false *)
317 [ nil ⇒ 〈true,visited〉
319 if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
320 bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
321 (sons S l hd)) tl) (hd::visited)
326 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
327 bisim S l n frontier visited =
329 [ O ⇒ 〈false,visited〉 (* assert false *)
332 [ nil ⇒ 〈true,visited〉
334 if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
335 bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
336 (sons S l hd)) tl) (hd::visited)
340 #S #l #n cases n // qed.
342 (* The integer n is an upper bound to the number of recursive call,
343 equal to the dimension of the graph. It returns a pair composed
344 by a boolean and a the set of visited nodes; the boolean is true
345 if and only if all visited nodes are cofinal.
347 The following results explicitly state the behaviour of bisim is the general
348 case and in some relevant instances *)
350 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
351 bisim S l O frontier visited = 〈false,visited〉.
352 #frontier #visited >unfold_bisim //
355 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
356 bisim Sig l (S m) [] visited = 〈true,visited〉.
357 #n #visisted >unfold_bisim //
360 lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
361 beqb (\snd (\fst p)) (\snd (\snd p)) = true →
362 bisim Sig l (S m) (p::frontier) visited =
363 bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
364 (sons Sig l p)) frontier) (p::visited).
365 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
368 lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
369 beqb (\snd (\fst p)) (\snd (\snd p)) = false →
370 bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
371 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
374 lemma notb_eq_true_l: ∀b. notb b = true → b = false.
375 #b cases b normalize //
378 (* In order to prove termination of bisim we must be able to effectively
379 enumerate all possible pres: *)
381 let rec pitem_enum S (i:re S) on i ≝
385 | s y ⇒ [ps S y; pp S y]
386 | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
387 | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
388 | k i ⇒ map ?? (pk S) (pitem_enum S i)
391 lemma pitem_enum_complete : ∀S.∀i:pitem S.
392 memb (DeqItem S) i (pitem_enum S (|i|)) = true.
395 |3,4:#c normalize >(\b (refl … c)) //
396 |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
397 |#i #Hind @(memb_map (DeqItem S)) //
401 definition pre_enum ≝ λS.λi:re S.
402 compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
404 lemma pre_enum_complete : ∀S.∀e:pre S.
405 memb ? e (pre_enum S (|\fst e|)) = true.
406 #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
407 // cases b normalize //
410 definition space_enum ≝ λS.λi1,i2:re S.
411 compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
413 lemma space_enum_complete : ∀S.∀e1,e2: pre S.
414 memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
415 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
418 (* We are ready to prove that bisim is correct; we use the invariant
419 that at each call of bisim the two lists visited and frontier only contain
420 nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose
421 to meet a pair which is not cofinal. *)
423 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
425 ∀p. memb ? p l = true →
426 ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
428 definition disjoint ≝ λS:DeqSet.λl1,l2.
429 ∀p:S. memb S p l1 = true → memb S p l2 = false.
431 lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}≐\sem{e2} →
432 ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
433 |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
434 all_reachable S e1 e2 visited →
435 all_reachable S e1 e2 frontier →
436 disjoint ? frontier visited →
437 \fst (bisim S l n frontier visited) = true.
438 #Sig #e1 #e2 #same #l #n elim n
439 [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
440 @le_to_not_lt @sublist_length // * #e11 #e21 #membp
441 cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
442 [|* #H1 #H2 <H1 <H2 @space_enum_complete]
443 cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
444 |#m #HI * [#visited #vinv #finv >bisim_end //]
445 #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
447 cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
448 [@(r_frontier … (memb_hd … ))] #rp
449 cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
450 [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
451 @(proj1 … (equiv_sem … )) @same] #ptest
452 >(bisim_step_true … ptest) @HI -HI
454 |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
455 |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
457 |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
458 @unique_append_elim #q #H
459 [cases (memb_sons … (memb_filter_memb … H)) -H
460 #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
461 >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
462 |@r_frontier @memb_cons //
464 |@unique_append_elim #q #H
465 [@injective_notb @(filter_true … H)
466 |cut ((q==p) = false)
467 [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
468 cases (andb_true … u_frontier) #notp #_ @(\bf ?)
469 @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
475 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
476 (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
478 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
479 memb ? x l1 = true → sublist ? (sons ? l x) l2.
481 (* For completeness, we use the invariant that all the nodes in visited are cofinal,
482 and the sons of visited are either in visited or in the frontier; since
483 at the end frontier is empty, visited is hence a bisimulation. *)
485 lemma bisim_complete:
486 ∀S,l,n.∀frontier,visited,visited_res:list ?.
488 sub_sons S l visited (frontier@visited) →
489 bisim S l n frontier visited = 〈true,visited_res〉 →
490 is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
492 [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
494 [(* case empty frontier *)
495 -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
497 [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
498 |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
499 [|(* case head of the frontier is non ok (absurd) *)
500 #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
501 (* frontier = hd:: tl and hd is ok *)
502 #H #tl #visited #visited_res #allv >(bisim_step_true … H)
503 (* new_visited = hd::visited are all ok *)
504 cut (all_true S (hd::visited))
505 [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
506 (* we now exploit the induction hypothesis *)
507 #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
508 [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
509 [cases (orb_true_l … membp) -membp #membp
510 [@memb_append_l2 >(\P membp) @memb_hd
511 |@memb_append_l1 @sublist_unique_append_l2 //
513 |@memb_append_l2 @memb_cons //
515 |(* the only thing left to prove is the sub_sons invariant *)
516 #x #membx cases (orb_true_l … membx)
518 #eqhdx <(\P eqhdx) #xa #membxa
519 (* xa is a son of x; we must distinguish the case xa
520 was already visited form the case xa is new *)
521 cases (true_or_false … (memb ? xa (x::visited)))
522 [(* xa visited - trivial *) #membxa @memb_append_l2 //
523 |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
526 |(* case x in visited *)
527 #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
528 [#H2 (cases (orb_true_l … H2))
529 [#H3 @memb_append_l2 <(\P H3) @memb_hd
530 |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
532 |#H2 @memb_append_l2 @memb_cons @H2
539 definition equiv ≝ λSig.λre1,re2:re Sig.
540 let e1 ≝ •(blank ? re1) in
541 let e2 ≝ •(blank ? re2) in
542 let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
543 let sig ≝ (occ Sig e1 e2) in
544 (bisim ? sig n [〈e1,e2〉] []).
546 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
547 \fst (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
549 [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
550 cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
552 cases (bisim_complete … Hcut)
553 [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
554 #Hbisim #Hsub @(bisim_to_sem … Hbisim)
556 |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
557 [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
559 |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
560 |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
566 definition eqbnat ≝ λn,m:nat. eqb n m.
568 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
569 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
572 definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
574 definition a ≝ s DeqNat 0.
575 definition b ≝ s DeqNat 1.
576 definition c ≝ s DeqNat 2.
578 definition exp1 ≝ ((a·b)^*·a).
579 definition exp2 ≝ a·(b·a)^*.
580 definition exp4 ≝ (b·a)^*.
582 definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
585 moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
590 moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
594 moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
598 moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
601 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
602 definition exp7 ≝ a · a^* · b^*.
604 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
605 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
607 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
610 definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
611 definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
613 example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.