]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/re/moves.ma
sqrt.ma
[helm.git] / matita / matita / lib / re / moves.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "re/re.ma".
16 include "basics/lists/listb.ma".
17
18 (* 
19 Moves
20
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 
25 be removed.
26
27 We can give a particularly elegant definition in terms of the
28 lifted operators of the previous section:
29 *)
30
31 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
32  match E with
33   [ pz ⇒ 〈 pz ?, false 〉
34   | pe ⇒ 〈 pe ? , false 〉
35   | ps y ⇒ 〈 ps ? y, false 〉
36   | pp y ⇒ 〈 ps ? 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)^⊛ ].
40   
41 lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
42   move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
43 // qed.
44
45 lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
46   move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
47 // qed.
48
49 lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
50   move S x i^* = (move ? x i)^⊛.
51 // qed.
52
53 definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
54
55 lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b. 
56   pmove ? x 〈i,b〉 = move ? x i.
57 // qed.
58
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 //
62 qed. 
63
64 lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
65   |\fst (move ? a i)| = |i|.
66 #S #a #i elim i //
67   [#i1 #i2 >move_cat #H1 #H2 whd in ⊢ (???%); <H1 <H2 //
68   |#i1 #i2 >move_plus #H1 #H2 whd in ⊢ (???%); <H1 <H2 //
69   ]
70 qed.
71
72 theorem move_ok:
73  ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S. 
74    \sem{move ? a i} w ↔ \sem{i} (a::w).
75 #S #a #i elim i 
76   [normalize /2/
77   |normalize /2/
78   |normalize /2/
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 //]
82     ]
83   |#i1 #i2 #HI1 #HI2 #w 
84    (* lhs = w∈\sem{move S a (i1·i2)} *)
85    >move_cat
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} *)
91    >sem_cat_w
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} *)
95    @iff_or_r
96    (* we are left to prove that 
97      w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
98      we use deriv_middot on the rhs *)
99    @iff_trans[||@iff_sym @deriv_middot //]
100    (* w∈\sem{move S a i1}·\sem{|i2|} ↔ w∈(deriv S \sem{i1} a) · \sem{|i2|} *)
101    @cat_ext_l @HI1
102   |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w 
103    @iff_trans[|@sem_oplus] 
104    @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
105   |#i1 #HI1 #w >move_star 
106    @iff_trans[|@sem_ostar] >same_kernel >sem_star_w 
107    @iff_trans[||@iff_sym @deriv_middot //]
108    @cat_ext_l @HI1
109   ]
110 qed.
111     
112 notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}.
113 let rec moves (S : DeqSet) w e on w : pre S ≝
114  match w with
115   [ nil ⇒ e
116   | cons x w' ⇒ w' ↦* (move S x (\fst e))]. 
117
118 lemma moves_empty: ∀S:DeqSet.∀e:pre S. 
119   moves ? [ ] e = e.
120 // qed.
121
122 lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. 
123   moves ? (a::w)  e = moves ? w (move S a (\fst e)).
124 // qed.
125
126 lemma moves_left : ∀S,a,w,e. 
127   moves S (w@[a]) e = move S a (\fst (moves S w e)). 
128 #S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
129 qed.
130
131 lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. 
132   iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
133 #S #a #w * #i #b cases b normalize 
134   [% /2/ * // #H destruct |% normalize /2/]
135 qed.
136
137 lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
138   |\fst (moves ? w e)| = |\fst e|.
139 #S #w elim w //
140 qed.
141
142 theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. 
143    (\snd (moves ? w e) = true) ↔ \sem{e} w.
144 #S #w elim w 
145  [* #i #b >moves_empty cases b % /2/
146  |#a #w1 #Hind #e >moves_cons
147   @iff_trans [||@iff_sym @not_epsilon_sem]
148   @iff_trans [||@move_ok] @Hind
149  ]
150 qed.
151
152 (************************ pit state ***************************)
153 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
154
155 let rec occur (S: DeqSet) (i: re S) on i ≝  
156   match i with
157   [ z ⇒ [ ]
158   | e ⇒ [ ]
159   | s y ⇒ [y]
160   | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
161   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
162   | k e ⇒ occur S e].
163
164 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
165   move S a i  = pit_pre S i.
166 #S #a #i elim i //
167   [#x normalize cases (a==x) normalize // #H @False_ind /2/
168   |#i1 #i2 #Hind1 #Hind2 #H >move_cat 
169    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
170    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
171   |#i1 #i2 #Hind1 #Hind2 #H >move_plus 
172    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
173    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
174   |#i #Hind #H >move_star >Hind // 
175   ]
176 qed.
177
178 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
179 #S #a #i elim i //
180   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
181   |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // 
182   |#i #Hind >move_star >Hind //
183   ]
184 qed. 
185
186 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
187 #S #w #i elim w // #a #tl >moves_cons // 
188 qed. 
189  
190 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
191  moves S w e = pit_pre S (\fst e).
192 #S #w elim w
193   [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
194   |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
195     [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) 
196      @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
197       [#H2 >(\P H2) // |#H2 @H1 //]
198     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
199     ]
200   ]
201 qed.
202
203 (* bisimulation *)
204 definition cofinal ≝ λS.λp:(pre S)×(pre S). 
205   \snd (\fst p) = \snd (\snd p).
206
207 (* As a corollary of decidable_sem, we have that two expressions
208 e1 and e2 are equivalent iff for any word w the states reachable 
209 through w are cofinal. *)
210
211 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. 
212   \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
213 #S #e1 #e2 % 
214 [#same_sem #w 
215   cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2)) 
216     [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
217   #Hcut @Hcut @iff_trans [|@decidable_sem] 
218   @iff_trans [|@same_sem] @iff_sym @decidable_sem
219 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
220 qed.
221
222 (* This does not directly imply decidability: we have no bound over the
223 length of w; moreover, so far, we made no assumption over the cardinality 
224 of S. Instead of requiring S to be finite, we may restrict the analysis
225 to characters occurring in the given pres. *)
226
227 definition occ ≝ λS.λe1,e2:pre S. 
228   unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
229
230 lemma occ_enough: ∀S.∀e1,e2:pre S.
231 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
232  →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
233 #S #e1 #e2 #H #w
234 cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
235  >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
236  >to_pit [2: @(not_to_not … H) #H1 #a #memba  @sublist_unique_append_l2 @H1 //]
237  //
238 qed.
239
240 (* The following is a stronger version of equiv_sem, relative to characters
241 occurring the given regular expressions. *)
242
243 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
244 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
245 → \sem{e1}≐\sem{e2}.
246 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H 
247 qed.
248
249 (* 
250 We say that a list of pairs of pres is a bisimulation if it is closed
251 w.r.t. moves, and all its members are cofinal.
252 *)
253
254 (* the sons of p w.r.t a list of symbols l are all states reachable from p 
255 with a move in l *)
256
257 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S). 
258  map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
259
260 lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
261   ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
262       move ? a (\fst (\snd q)) = \snd p).
263 #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/] 
264 #a #tl #Hind #p #q #H cases (orb_true_l … H) -H
265   [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
266 qed.
267
268 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
269   ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
270
271 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
272
273 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. 
274   is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}≐\sem{e2}.
275 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ 
276 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
277 lapply Hsub @(list_elim_left … w) [//]
278 #a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
279   [#x #Hx @Hsub @memb_append_l1 //
280   |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa 
281    @(memb_map … occa)
282   ]
283 qed.
284
285 (* This is already an interesting result: checking if l is a bisimulation 
286 is decidable, hence we could generate l with some untrusted piece of code 
287 and then run a (boolean version of) is_bisim to check that it is actually 
288 a bisimulation. 
289 However, in order to prove that equivalence of regular expressions
290 is decidable we must prove that we can always effectively build such a list 
291 (or find a counterexample).
292 The idea is that the list we are interested in is just the set of 
293 all pair of pres reachable from the initial pair via some
294 sequence of moves. 
295
296 The algorithm for computing reachable nodes in graph is a very 
297 traditional one. We split nodes in two disjoint lists: a list of 
298 visited nodes and a frontier, composed by all nodes connected
299 to a node in visited but not visited already. At each step we select a node 
300 a from the frontier, compute its sons, add a to the set of 
301 visited nodes and the (not already visited) sons to the frontier. 
302
303 Instead of fist computing reachable nodes and then performing the 
304 bisimilarity test we can directly integrate it in the algorithm:
305 the set of visited nodes is closed by construction w.r.t. reachability,
306 so we have just to check cofinality for any node we add to visited.
307
308 Here is the extremely simple algorithm: *)
309
310 let rec bisim S l n (frontier,visited: list ?) on n ≝
311   match n with 
312   [ O ⇒ 〈false,visited〉 (* assert false *)
313   | S m ⇒ 
314     match frontier with
315     [ nil ⇒ 〈true,visited〉
316     | cons hd tl ⇒
317       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
318         bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited))) 
319         (sons S l hd)) tl) (hd::visited)
320       else 〈false,visited〉
321     ]
322   ].
323   
324 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
325   bisim S l n frontier visited =
326   match n with 
327   [ O ⇒ 〈false,visited〉 (* assert false *)
328   | S m ⇒ 
329     match frontier with
330     [ nil ⇒ 〈true,visited〉
331     | cons hd tl ⇒
332       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
333         bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) 
334           (sons S l hd)) tl) (hd::visited)
335       else 〈false,visited〉
336     ]
337   ].
338 #S #l #n cases n // qed.
339
340 (* The integer n is an upper bound to the number of recursive call, 
341 equal to the dimension of the graph. It returns a pair composed
342 by a boolean and a the set of visited nodes; the boolean is true
343 if and only if all visited nodes are cofinal. 
344
345 The following results explicitly state the behaviour of bisim is the general
346 case and in some relevant instances *)
347  
348 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
349   bisim S l O frontier visited = 〈false,visited〉.
350 #frontier #visited >unfold_bisim // 
351 qed.
352
353 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
354   bisim Sig l (S m) [] visited = 〈true,visited〉.
355 #n #visisted >unfold_bisim // 
356 qed.
357
358 lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
359 beqb (\snd (\fst p)) (\snd (\snd p)) = true →
360   bisim Sig l (S m) (p::frontier) visited = 
361   bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited))) 
362     (sons Sig l p)) frontier) (p::visited).
363 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // 
364 qed.
365
366 lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
367 beqb (\snd (\fst p)) (\snd (\snd p)) = false →
368   bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
369 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // 
370 qed.
371
372 lemma notb_eq_true_l: ∀b. notb b = true → b = false.
373 #b cases b normalize //
374 qed.
375
376 (* In order to prove termination of bisim we must be able to effectively 
377 enumerate all possible pres: *)
378
379 let rec pitem_enum S (i:re S) on i ≝
380   match i with
381   [ z ⇒ [pz S]
382   | e ⇒ [pe S]
383   | s y ⇒ [ps S y; pp S y]
384   | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
385   | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
386   | k i ⇒ map ?? (pk S) (pitem_enum S i)
387   ].
388   
389 lemma pitem_enum_complete : ∀S.∀i:pitem S.
390   memb (DeqItem S) i (pitem_enum S (|i|)) = true.
391 #S #i elim i 
392   [1,2://
393   |3,4:#c normalize >(\b (refl … c)) //
394   |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
395   |#i #Hind @(memb_map (DeqItem S)) //
396   ]
397 qed.
398
399 definition pre_enum ≝ λS.λi:re S.
400   compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
401   
402 lemma pre_enum_complete : ∀S.∀e:pre S.
403   memb ? e (pre_enum S (|\fst e|)) = true.
404 #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
405 // cases b normalize //
406 qed.
407  
408 definition space_enum ≝ λS.λi1,i2:re S.
409   compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
410
411 lemma space_enum_complete : ∀S.∀e1,e2: pre S.
412   memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
413 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
414 // qed.
415
416 (* We are ready to prove that bisim is correct; we use the invariant 
417 that at each call of bisim the two lists visited and frontier only contain 
418 nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose 
419 to meet a pair which is not cofinal. *)
420
421 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
422 uniqueb ? l = true ∧ 
423   ∀p. memb ? p l = true → 
424     ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p). 
425
426 definition disjoint ≝ λS:DeqSet.λl1,l2.
427   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
428         
429 lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}≐\sem{e2} → 
430  ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
431  |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
432  all_reachable S e1 e2 visited →  
433  all_reachable S e1 e2 frontier →
434  disjoint ? frontier visited →
435  \fst (bisim S l n frontier visited) = true.
436 #Sig #e1 #e2 #same #l #n elim n 
437   [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
438    @le_to_not_lt @sublist_length // * #e11 #e21 #membp 
439    cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
440    [|* #H1 #H2 <H1 <H2 @space_enum_complete]
441    cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //    
442   |#m #HI * [#visited #vinv #finv >bisim_end //]
443    #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier 
444    #disjoint
445    cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p)) 
446     [@(r_frontier … (memb_hd … ))] #rp
447    cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
448     [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?) 
449      @(proj1 … (equiv_sem … )) @same] #ptest 
450    >(bisim_step_true … ptest) @HI -HI 
451      [<plus_n_Sm //
452      |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
453         |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
454         ]
455      |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
456       @unique_append_elim #q #H
457        [cases (memb_sons … (memb_filter_memb … H)) -H
458         #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
459         >moves_left >moves_left >mw1 >mw2 >m1 >m2 % // 
460        |@r_frontier @memb_cons //
461        ]
462      |@unique_append_elim #q #H
463        [@injective_notb @(filter_true … H)
464        |cut ((q==p) = false) 
465          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
466         cases (andb_true … u_frontier) #notp #_ @(\bf ?) 
467         @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
468        ]
469      ]
470    ]  
471 qed.     
472
473 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true → 
474   (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
475
476 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). 
477 memb ? x l1 = true → sublist ? (sons ? l x) l2. 
478
479 (* For completeness, we use the invariant that all the nodes in visited are cofinal, 
480 and the sons of visited are either in visited or in the frontier; since
481 at the end frontier is empty, visited is hence a bisimulation. *)
482
483 lemma bisim_complete: 
484  ∀S,l,n.∀frontier,visited,visited_res:list ?.
485  all_true S visited →
486  sub_sons S l visited (frontier@visited) →
487  bisim S l n frontier visited = 〈true,visited_res〉 →
488  is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res. 
489 #S #l #n elim n
490   [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
491   |#m #Hind * 
492     [(* case empty frontier *)
493      -Hind #vis #vis_res #allv #H normalize in  ⊢ (%→?);
494      #H1 destruct % #p 
495       [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
496     |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
497       [|(* case head of the frontier is non ok (absurd) *)
498        #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
499      (* frontier = hd:: tl and hd is ok *)
500      #H #tl #visited #visited_res #allv >(bisim_step_true … H)
501      (* new_visited = hd::visited are all ok *)
502      cut (all_true S (hd::visited)) 
503       [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
504      (* we now exploit the induction hypothesis *)
505      #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
506       [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
507         [cases (orb_true_l … membp) -membp #membp
508           [@memb_append_l2 >(\P membp) @memb_hd
509           |@memb_append_l1 @sublist_unique_append_l2 // 
510           ]
511         |@memb_append_l2 @memb_cons //
512         ] 
513       |(* the only thing left to prove is the sub_sons invariant *)  
514      #x #membx cases (orb_true_l … membx)
515       [(* case x = hd *) 
516        #eqhdx <(\P eqhdx) #xa #membxa
517        (* xa is a son of x; we must distinguish the case xa 
518         was already visited form the case xa is new *)
519        cases (true_or_false … (memb ? xa (x::visited)))
520         [(* xa visited - trivial *) #membxa @memb_append_l2 //
521         |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
522           [>membxa //|//]
523         ]
524       |(* case x in visited *)
525        #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))  
526         [#H2 (cases (orb_true_l … H2)) 
527           [#H3 @memb_append_l2 <(\P H3) @memb_hd
528           |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
529           ]
530         |#H2 @memb_append_l2 @memb_cons @H2
531         ]
532       ]
533     ]
534   ]
535 qed.
536
537 definition equiv ≝ λSig.λre1,re2:re Sig. 
538   let e1 ≝ •(blank ? re1) in
539   let e2 ≝ •(blank ? re2) in
540   let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
541   let sig ≝ (occ Sig e1 e2) in
542   (bisim ? sig n [〈e1,e2〉] []).
543
544 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
545    \fst (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
546 #Sig #re1 #re2 %
547   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
548    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
549      [<H //] #Hcut
550    cases (bisim_complete … Hcut) 
551      [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/] 
552    #Hbisim #Hsub @(bisim_to_sem … Hbisim) 
553    @Hsub @memb_hd
554   |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2))) 
555     [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
556     |// 
557     |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/  
558     |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
559     |#p #_ normalize //
560     ]
561   ]
562 qed.
563
564 definition eqbnat ≝ λn,m:nat. eqb n m.
565
566 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
567 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
568 qed.
569
570 definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
571
572 definition a ≝ s DeqNat 0.
573 definition b ≝ s DeqNat 1.
574 definition c ≝ s DeqNat 2.
575
576 definition exp1 ≝ ((a·b)^*·a).
577 definition exp2 ≝ a·(b·a)^*.
578 definition exp4 ≝ (b·a)^*.
579
580 definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
581
582 example 
583   moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
584 normalize // 
585 qed.
586
587 example 
588   moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
589 normalize // qed.
590
591 example 
592   moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
593 normalize // qed.
594
595 example 
596   moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
597 normalize // qed.
598
599 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
600 definition exp7 ≝ a · a^* · b^*.
601
602 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
603 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
604
605 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
606 normalize // qed.
607
608 definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
609 definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
610
611 example ex2 : \fst (equiv ? (exp10+exp11) exp11) = false.
612 normalize // qed.
613
614 definition exp12 ≝
615   (a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a^* ).
616   
617 example ex3 : \fst (equiv ? (exp12+exp11) exp11) = true.
618 normalize // qed.
619
620 let rec raw (n:nat) ≝
621   match n with
622   [ O ⇒ a
623   | S p ⇒ a · (raw p)
624   ].
625
626 let rec alln (n:nat) ≝
627   match n with
628   [O ⇒ ϵ
629   |S m ⇒ raw m + alln m
630   ].
631
632 definition testA ≝ λx,y,z,b.
633   let e1 ≝ raw x in
634   let e2 ≝ raw y in
635   let e3 ≝ (raw z) · a^* in
636   let e4 ≝ (e1 + e2)^* in
637   \fst (equiv ? (e3+e4) e4) = b.
638   
639 example ex4 : testA 2 4 7 true.
640 normalize // qed.
641
642 example ex5 : testA 3 4 10 false.
643 normalize // qed.
644
645 example ex6 : testA 3 4 11 true.
646 normalize // qed.
647
648 example ex7 : testA 4 5 18 false.
649 normalize // qed.
650
651 example ex8 : testA 4 5 19 true.
652 normalize // qed.
653
654 example ex9 : testA 4 6 22 false.
655 normalize // qed.
656
657 example ex10 : testA 4 6 23 true.
658 normalize // qed.
659
660 definition testB ≝ λn,b.
661   \fst (equiv ? ((alln n)·((raw n)^* )) a^* ) = b.
662
663 example ex11 : testB 6 true.
664 normalize // qed.
665
666 example ex12 : testB 8 true.
667 normalize // qed.
668
669 example ex13 : testB 10 true.
670 normalize // qed.
671
672 example ex14 : testB 12 true.
673 normalize // qed.
674
675 example ex15 : testB 14 true.
676 normalize // qed.
677
678 example ex16 : testB 16 true.
679 normalize // qed.
680
681 example ex17 : testB 18 true.
682 normalize // qed.