X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Fmoves.ma;h=c8c3b3478fc865cf53bcd034110e8b2a05fcc9f4;hb=1ca3d131ce61d857ebf691169e85ddb81250fd4e;hp=f4da274a6beecbf4b9feeda9d6172ebbde65d330;hpb=2fef56731b0d38913967105495b96754e327efab;p=helm.git

diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index f4da274a6..c8c3b3478 100644
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -15,12 +15,25 @@
 include "re/re.ma".
 include "basics/lists/listb.ma".
 
+(* 
+Moves
+
+We now define the move operation, that corresponds to the advancement of the 
+state in response to the processing of an input character a. The intuition is 
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must 
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
+*)
+
 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  match E with
-  [ pz ⇒ 〈 `∅, false 〉
-  | pe ⇒ 〈 ϵ, false 〉
-  | ps y ⇒ 〈 `y, false 〉
-  | pp y ⇒ 〈 `y, x == y 〉
+  [ pz ⇒ 〈 pz ?, false 〉
+  | pe ⇒ 〈 pe ? , false 〉
+  | ps y ⇒ 〈 ps ? y, false 〉
+  | pp y ⇒ 〈 ps ? y, x == y 〉
   | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2) 
   | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
   | pk e ⇒ (move ? x e)^⊛ ].
@@ -67,10 +80,24 @@ theorem move_ok:
     [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
     |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
     ]
-  |#i1 #i2 #HI1 #HI2 #w >move_cat
-   @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
-   @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r 
+  |#i1 #i2 #HI1 #HI2 #w 
+   (* lhs = w∈\sem{move S a (i1·i2)} *)
+   >move_cat
+   (* lhs = w∈\sem{move S a i1}⊙\sem{move S a i2} *)
+   @iff_trans[|@sem_odot] >same_kernel 
+   (* lhs = w∈\sem{move S a i1}·\sem{|i2|} ∨ a∈\sem{move S a i2} *)
+   (* now we work on the rhs, that is
+      rhs = a::w1∈\sem{i1·i2} *)
+   >sem_cat_w
+   (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
+   @iff_trans[||@(iff_or_l … (HI2 w))] 
+   (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
+   @iff_or_r
+   (* we are left to prove that 
+     w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
+     we use deriv_middot on the rhs *)
    @iff_trans[||@iff_sym @deriv_middot //]
+   (* w∈\sem{move S a i1}·\sem{|i2|} ↔ w∈(deriv S \sem{i1} a) · \sem{|i2|} *)
    @cat_ext_l @HI1
   |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w 
    @iff_trans[|@sem_oplus] 
@@ -82,7 +109,7 @@ theorem move_ok:
   ]
 qed.
     
-notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}.
 let rec moves (S : DeqSet) w e on w : pre S ≝
  match w with
   [ nil ⇒ e
@@ -122,10 +149,6 @@ theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
  ]
 qed.
 
-(* lemma not_true_to_false: ∀b.b≠true → b =false.
-#b * cases b // #H @False_ind /2/ 
-qed. *)
-
 (************************ pit state ***************************)
 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
 
@@ -180,9 +203,13 @@ qed.
 (* bisimulation *)
 definition cofinal ≝ λS.λp:(pre S)×(pre S). 
   \snd (\fst p) = \snd (\snd p).
-  
+
+(* As a corollary of decidable_sem, we have that two expressions
+e1 and e2 are equivalent iff for any word w the states reachable 
+through w are cofinal. *)
+
 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. 
-  \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+  \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
 #S #e1 #e2 % 
 [#same_sem #w 
   cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2)) 
@@ -192,6 +219,11 @@ theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
 qed.
 
+(* This does not directly imply decidability: we have no bound over the
+length of w; moreover, so far, we made no assumption over the cardinality 
+of S. Instead of requiring S to be finite, we may restrict the analysis
+to characters occurring in the given pres. *)
+
 definition occ ≝ λS.λe1,e2:pre S. 
   unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
 
@@ -205,12 +237,23 @@ cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
  //
 qed.
 
+(* The following is a stronger version of equiv_sem, relative to characters
+occurring the given regular expressions. *)
+
 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
-→ \sem{e1}=1\sem{e2}.
+→ \sem{e1}≐\sem{e2}.
 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H 
 qed.
 
+(* 
+We say that a list of pairs of pres is a bisimulation if it is closed
+w.r.t. moves, and all its members are cofinal.
+*)
+
+(* the sons of p w.r.t a list of symbols l are all states reachable from p 
+with a move in l *)
+
 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S). 
  map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
 
@@ -225,8 +268,10 @@ qed.
 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
   ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
 
+(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+
 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. 
-  is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+  is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}≐\sem{e2}.
 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ 
 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
 lapply Hsub @(list_elim_left … w) [//]
@@ -237,7 +282,31 @@ lapply Hsub @(list_elim_left … w) [//]
   ]
 qed.
 
-(* the algorithm *)
+(* This is already an interesting result: checking if l is a bisimulation 
+is decidable, hence we could generate l with some untrusted piece of code 
+and then run a (boolean version of) is_bisim to check that it is actually 
+a bisimulation. 
+However, in order to prove that equivalence of regular expressions
+is decidable we must prove that we can always effectively build such a list 
+(or find a counterexample).
+The idea is that the list we are interested in is just the set of 
+all pair of pres reachable from the initial pair via some
+sequence of moves. 
+
+The algorithm for computing reachable nodes in graph is a very 
+traditional one. We split nodes in two disjoint lists: a list of 
+visited nodes and a frontier, composed by all nodes connected
+to a node in visited but not visited already. At each step we select a node 
+a from the frontier, compute its sons, add a to the set of 
+visited nodes and the (not already visited) sons to the frontier. 
+
+Instead of fist computing reachable nodes and then performing the 
+bisimilarity test we can directly integrate it in the algorithm:
+the set of visited nodes is closed by construction w.r.t. reachability,
+so we have just to check cofinality for any node we add to visited.
+
+Here is the extremely simple algorithm: *)
+
 let rec bisim S l n (frontier,visited: list ?) on n ≝
   match n with 
   [ O ⇒ 〈false,visited〉 (* assert false *)
@@ -267,7 +336,15 @@ lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
     ]
   ].
 #S #l #n cases n // qed.
-  
+
+(* The integer n is an upper bound to the number of recursive call, 
+equal to the dimension of the graph. It returns a pair composed
+by a boolean and a the set of visited nodes; the boolean is true
+if and only if all visited nodes are cofinal. 
+
+The following results explicitly state the behaviour of bisim is the general
+case and in some relevant instances *)
+ 
 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
   bisim S l O frontier visited = 〈false,visited〉.
 #frontier #visited >unfold_bisim // 
@@ -296,6 +373,9 @@ lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 #b cases b normalize //
 qed.
 
+(* In order to prove termination of bisim we must be able to effectively 
+enumerate all possible pres: *)
+
 let rec pitem_enum S (i:re S) on i ≝
   match i with
   [ z ⇒ [pz S]
@@ -333,6 +413,11 @@ lemma space_enum_complete : ∀S.∀e1,e2: pre S.
 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
 // qed.
 
+(* We are ready to prove that bisim is correct; we use the invariant 
+that at each call of bisim the two lists visited and frontier only contain 
+nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose 
+to meet a pair which is not cofinal. *)
+
 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
 uniqueb ? l = true ∧ 
   ∀p. memb ? p l = true → 
@@ -341,7 +426,7 @@ uniqueb ? l = true ∧
 definition disjoint ≝ λS:DeqSet.λl1,l2.
   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
         
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → 
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}≐\sem{e2} → 
  ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
  |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
  all_reachable S e1 e2 visited →  
@@ -391,6 +476,10 @@ definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). 
 memb ? x l1 = true → sublist ? (sons ? l x) l2. 
 
+(* For completeness, we use the invariant that all the nodes in visited are cofinal, 
+and the sons of visited are either in visited or in the frontier; since
+at the end frontier is empty, visited is hence a bisimulation. *)
+
 lemma bisim_complete: 
  ∀S,l,n.∀frontier,visited,visited_res:list ?.
  all_true S visited →
@@ -453,7 +542,7 @@ definition equiv ≝ λSig.λre1,re2:re Sig.
   (bisim ? sig n [〈e1,e2〉] []).
 
 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
-   \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+   \fst (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
 #Sig #re1 #re2 %
   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
@@ -488,6 +577,25 @@ definition exp1 ≝ ((a·b)^*·a).
 definition exp2 ≝ a·(b·a)^*.
 definition exp4 ≝ (b·a)^*.
 
+definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
+
+example 
+  moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
+normalize // 
+qed.
+
+example 
+  moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
+normalize // qed.
+
+example 
+  moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
+normalize // qed.
+
+example 
+  moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
+normalize // qed.
+
 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
 definition exp7 ≝ a · a^* · b^*.
 
@@ -497,9 +605,78 @@ definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
 normalize // qed.
 
+definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
+definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
+
+example ex2 : \fst (equiv ? (exp10+exp11) exp11) = false.
+normalize // qed.
+
+definition exp12 ≝
+  (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^* ).
+  
+example ex3 : \fst (equiv ? (exp12+exp11) exp11) = true.
+normalize // qed.
+
+let rec raw (n:nat) ≝
+  match n with
+  [ O ⇒ a
+  | S p ⇒ a · (raw p)
+  ].
+
+let rec alln (n:nat) ≝
+  match n with
+  [O ⇒ ϵ
+  |S m ⇒ raw m + alln m
+  ].
+
+definition testA ≝ λx,y,z,b.
+  let e1 ≝ raw x in
+  let e2 ≝ raw y in
+  let e3 ≝ (raw z) · a^* in
+  let e4 ≝ (e1 + e2)^* in
+  \fst (equiv ? (e3+e4) e4) = b.
+  
+example ex4 : testA 2 4 7 true.
+normalize // qed.
 
+example ex5 : testA 3 4 10 false.
+normalize // qed.
 
+example ex6 : testA 3 4 11 true.
+normalize // qed.
 
+example ex7 : testA 4 5 18 false.
+normalize // qed.
 
+example ex8 : testA 4 5 19 true.
+normalize // qed.
 
+example ex9 : testA 4 6 22 false.
+normalize // qed.
 
+example ex10 : testA 4 6 23 true.
+normalize // qed.
+
+definition testB ≝ λn,b.
+  \fst (equiv ? ((alln n)·((raw n)^* )) a^* ) = b.
+
+example ex11 : testB 6 true.
+normalize // qed.
+
+example ex12 : testB 8 true.
+normalize // qed.
+
+example ex13 : testB 10 true.
+normalize // qed.
+
+example ex14 : testB 12 true.
+normalize // qed.
+
+example ex15 : testB 14 true.
+normalize // qed.
+
+example ex16 : testB 16 true.
+normalize // qed.
+
+example ex17 : testB 18 true.
+normalize // qed.