From 2fef56731b0d38913967105495b96754e327efab Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 3 Jan 2012 16:16:45 +0000 Subject: [PATCH] Complete version --- matita/matita/lib/re/lang.ma | 4 + matita/matita/lib/re/moves.ma | 545 +++++++++++++--------------------- matita/matita/lib/re/re.ma | 248 +++++++++++----- 3 files changed, 379 insertions(+), 418 deletions(-) diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma index c1b894a7d..172693924 100644 --- a/matita/matita/lib/re/lang.ma +++ b/matita/matita/lib/re/lang.ma @@ -53,6 +53,10 @@ lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. cases (H w2) /6/ qed. +lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅. +#S #A #w % [|*] * #w1 * #w2 * * #_ * +qed. + lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. (A ∪ B) · C =1 A · C ∪ B · C. #S #A #B #C #w % diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index c260a6d40..f4da274a6 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -67,7 +67,7 @@ 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 >(sem_cat S i1 i2) >move_cat + |#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 @iff_trans[||@iff_sym @deriv_middot //] @@ -86,7 +86,7 @@ notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. let rec moves (S : DeqSet) w e on w : pre S ≝ match w with [ nil ⇒ e - | cons x w' ⇒ w' ↦* (move S x (\fst e))]. + | cons x w' ⇒ w' ↦* (move S x (\fst e))]. lemma moves_empty: ∀S:DeqSet.∀e:pre S. moves ? [ ] e = e. @@ -96,6 +96,11 @@ lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. moves ? (a::w) e = moves ? w (move S a (\fst e)). // qed. +lemma moves_left : ∀S,a,w,e. + moves S (w@[a]) e = move S a (\fst (moves S w e)). +#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons // +qed. + lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. iff ((a::w) ∈ e) ((a::w) ∈ \fst e). #S #a #w * #i #b cases b normalize @@ -108,7 +113,7 @@ lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S. qed. theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. - (\snd (moves ? w e) = true) ↔ \sem{e} w. + (\snd (moves ? w e) = true) ↔ \sem{e} w. #S #w elim w [* #i #b >moves_empty cases b % /2/ |#a #w1 #Hind #e >moves_cons @@ -117,12 +122,67 @@ theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. ] qed. -lemma not_true_to_false: ∀b.b≠true → b =false. +(* 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〉. + +let rec occur (S: DeqSet) (i: re S) on i ≝ + match i with + [ z ⇒ [ ] + | e ⇒ [ ] + | s y ⇒ [y] + | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) + | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) + | k e ⇒ occur S e]. + +lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true → + move S a i = pit_pre S i. +#S #a #i elim i // + [#x normalize cases (a==x) normalize // #H @False_ind /2/ + |#i1 #i2 #Hind1 #Hind2 #H >move_cat + >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //] + >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] // + |#i1 #i2 #Hind1 #Hind2 #H >move_plus + >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //] + >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] // + |#i #Hind #H >move_star >Hind // + ] +qed. + +lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. +#S #a #i elim i // + [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // + |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // + |#i #Hind >move_star >Hind // + ] qed. +lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. +#S #w #i elim w // #a #tl >moves_cons // +qed. + +lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) → + moves S w e = pit_pre S (\fst e). +#S #w elim w + [#e * #H @False_ind @H normalize #a #abs @False_ind /2/ + |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|)))) + [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) + @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb) + [#H2 >(\P H2) // |#H2 @H1 //] + |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ + ] + ] +qed. + +(* bisimulation *) +definition cofinal ≝ λS.λp:(pre S)×(pre S). + \snd (\fst p) = \snd (\snd p). + theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. - iff (\sem{e1} =1 \sem{e2}) (∀w.\snd (moves ? w e1) = \snd (moves ? w e2)). + \sem{e1} =1 \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)) @@ -132,79 +192,24 @@ theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. |#H #w1 @iff_trans [||@decidable_sem] moves_cons >moves_cons // -qed. - -definition in_moves ≝ λS:DeqSet.λw.λe:pre S. \snd(w ↦* e). - -(* -coinductive equiv (S:DeqSet) : pre S → pre S → Prop ≝ - mk_equiv: - ∀e1,e2: pre S. - \snd e1 = \snd e2 → - (∀x. equiv S (move ? x (\fst e1)) (move ? x (\fst e2))) → - equiv S e1 e2. -*) - -let rec beqitem S (i1,i2: pitem S) on i1 ≝ - match i1 with - [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false] - | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false] - | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false] - | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false] - | po i11 i12 ⇒ match i2 with - [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 - | _ ⇒ false] - | pc i11 i12 ⇒ match i2 with - [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 - | _ ⇒ false] - | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false] - ]. +definition occ ≝ λS.λe1,e2:pre S. + unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)). -lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). -#S #i1 elim i1 - [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct - |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct - |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct - [>(\P H) // | @(\b (refl …))] - |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct - [>(\P H) // | @(\b (refl …))] - |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % - normalize #H destruct - [cases (true_or_false (beqitem S i11 i21)) #H1 - [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H - |>H1 in H; normalize #abs @False_ind /2/ - ] - |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // - ] - |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % - normalize #H destruct - [cases (true_or_false (beqitem S i11 i21)) #H1 - [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H - |>H1 in H; normalize #abs @False_ind /2/ - ] - |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // - ] - |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] % - normalize #H destruct - [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //] - ] -qed. +lemma occ_enough: ∀S.∀e1,e2:pre S. +(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉) + →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉. +#S #e1 #e2 #H #w +cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H + >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //] + >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //] + // +qed. -definition DeqItem ≝ λS. - mk_DeqSet (pitem S) (beqitem S) (beqitem_true S). - -unification hint 0 ≔ S; - X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) -(* ---------------------------------------- *) ⊢ - pitem S ≡ carr X. - -unification hint 0 ≔ S,i1,i2; - X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) -(* ---------------------------------------- *) ⊢ - beqitem S i1 i2 ≡ eqb X i1 i2. +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}. +#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H +qed. 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. @@ -214,11 +219,25 @@ lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true move ? a (\fst (\snd q)) = \snd p). #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/] #a #tl #Hind #p #q #H cases (orb_true_l … H) -H - [#H @(ex_intro … a) <(proj1 … (eqb_true …)H) /2/ - |#H @Hind @H + [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H] +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). + +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}. +#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) [//] +#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?))) + [#x #Hx @Hsub @memb_append_l1 // + |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa + @(memb_map … occa) ] qed. +(* the algorithm *) let rec bisim S l n (frontier,visited: list ?) on n ≝ match n with [ O ⇒ 〈false,visited〉 (* assert false *) @@ -272,61 +291,11 @@ beqb (\snd (\fst p)) (\snd (\snd p)) = false → bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉. #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // qed. - -definition visited_inv ≝ λS.λe1,e2:pre S.λvisited: list ?. -uniqueb ? visited = true ∧ - ∀p. memb ? p visited = true → - (∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p)) ∧ - (beqb (\snd (\fst p)) (\snd (\snd p)) = true). - -definition frontier_inv ≝ λS.λfrontier,visited. -uniqueb ? frontier = true ∧ -∀p:(pre S)×(pre S). memb ? p frontier = true → - memb ? p visited = false ∧ - ∃p1.((memb ? p1 visited = true) ∧ - (∃a. move ? a (\fst (\fst p1)) = \fst p ∧ - move ? a (\fst (\snd p1)) = \snd p)). - -(* lemma andb_true: ∀b1,b2:bool. - (b1 ∧ b2) = true → (b1 = true) ∧ (b2 = true). -#b1 #b2 cases b1 normalize #H [>H /2/ |@False_ind /2/]. -qed. - -lemma andb_true_r: ∀b1,b2:bool. - (b1 = true) ∧ (b2 = true) → (b1 ∧ b2) = true. -#b1 #b2 cases b1 normalize * // -qed. *) lemma notb_eq_true_l: ∀b. notb b = true → b = false. #b cases b normalize // qed. -(* -lemma notb_eq_true_r: ∀b. b = false → notb b = true. -#b cases b normalize // -qed. - -lemma notb_eq_false_l:∀b. notb b = false → b = true. -#b cases b normalize // -qed. - -lemma notb_eq_false_r:∀b. b = true → notb b = false. -#b cases b normalize // -qed. *) - -(* include "arithmetics/exp.ma". *) - -let rec pos S (i:re S) on i ≝ - match i with - [ z ⇒ 0 - | e ⇒ 0 - | s y ⇒ 1 - | o i1 i2 ⇒ pos S i1 + pos S i2 - | c i1 i2 ⇒ pos S i1 + pos S i2 - | k i ⇒ pos S i - ]. - - let rec pitem_enum S (i:re S) on i ≝ match i with [ z ⇒ [pz S] @@ -364,15 +333,20 @@ lemma space_enum_complete : ∀S.∀e1,e2: pre S. #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉)) // qed. -definition visited_inv_1 ≝ λS.λe1,e2:pre S.λvisited: list ?. -uniqueb ? visited = true ∧ - ∀p. memb ? p visited = true → +definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?. +uniqueb ? l = true ∧ + ∀p. memb ? p l = true → ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p). - -lemma bisim_ok1: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → - ∀l,n.∀frontier,visited:list (*(space S) *) ((pre S)×(pre S)). + +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} → + ∀l,n.∀frontier,visited:list ((pre S)×(pre S)). |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→ - visited_inv_1 S e1 e2 visited → frontier_inv S frontier visited → + all_reachable S e1 e2 visited → + all_reachable S e1 e2 frontier → + disjoint ? frontier visited → \fst (bisim S l n frontier visited) = true. #Sig #e1 #e2 #same #l #n elim n [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs) @@ -381,65 +355,55 @@ lemma bisim_ok1: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → [|* #H1 #H2

same_kernel_moves // |#m #HI * [#visited #vinv #finv >bisim_end //] - #p #front_tl #visited #Hn * #u_visited #vinv * #u_frontier #finv - cases (finv p (memb_hd …)) #Hp * #p2 * #visited_p2 - * #a * #movea1 #movea2 - cut (∃w.(moves Sig w e1 = \fst p) ∧ (moves Sig w e2 = \snd p)) - [cases (vinv … visited_p2) -vinv #w1 * #mw1 #mw2 - @(ex_intro … (w1@[a])) % //] - -movea2 -movea1 -a -visited_p2 -p2 #reachp + #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier + #disjoint + cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p)) + [@(r_frontier … (memb_hd … ))] #rp cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true) - [cases reachp #w * #move_e1 #move_e2 (bisim_step_true … ptest) @HI -HI [Hp whd in ⊢ (??%?); //] - #p1 #H (cases (orb_true_l … H)) - [#eqp <(\P eqp) // - |#visited_p1 @(vinv … visited_p1) - ] + |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); // + |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited] + ] |whd % [@unique_append_unique @(andb_true_r … u_frontier)] @unique_append_elim #q #H - [% - [@notb_eq_true_l @(filter_true … H) - |@(ex_intro … p) % [@memb_hd|@(memb_sons … (memb_filter_memb … H))] - ] - |cases (finv q ?) [|@memb_cons //] - #nvq * #p1 * #Hp1 #reach % - [cut ((p==q) = false) [|#Hpq whd in ⊢ (??%?); >Hpq @nvq] - cases (andb_true … u_frontier) #notp #_ - @(not_memb_to_not_eq … H) @notb_eq_true_l @notp - |cases (proj2 … (finv q ?)) - [#p1 * #Hp1 #reach @(ex_intro … p1) % // @memb_cons // - |@memb_cons // - ] - ] - ] - ] - ] -qed. + [cases (memb_sons … (memb_filter_memb … H)) -H + #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a])) + >moves_left >moves_left >mw1 >mw2 >m1 >m2 % // + |@r_frontier @memb_cons // + ] + |@unique_append_elim #q #H + [@injective_notb @(filter_true … H) + |cut ((q==p) = false) + [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //] + cases (andb_true … u_frontier) #notp #_ @(\bf ?) + @(not_to_not … not_eq_true_false) #eqqp H // + ] + ] + ] +qed. definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true → (beqb (\snd (\fst p)) (\snd (\snd p)) = true). -definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).∀a:S. -memb ? x l1 = true → memb S a l = true → - memb ? 〈move ? a (\fst (\fst x)), move ? a (\fst (\snd x))〉 l2 = true. +definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). +memb ? x l1 = true → sublist ? (sons ? l x) l2. -lemma reachable_bisim: +lemma bisim_complete: ∀S,l,n.∀frontier,visited,visited_res:list ?. all_true S visited → sub_sons S l visited (frontier@visited) → - bisim S l n frontier visited = 〈true,visited_res〉 → - (sub_sons S l visited_res visited_res ∧ - sublist ? visited visited_res ∧ - all_true S visited_res). + bisim S l n frontier visited = 〈true,visited_res〉 → + is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res. #S #l #n elim n [#fron #vis #vis_res #_ #_ >bisim_never #H destruct |#m #Hind * [(* case empty frontier *) -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?); - #H1 destruct % // % // #p /2 by / + #H1 destruct % #p + [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1] |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd)))) [|(* case head of the frontier is non ok (absurd) *) #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct] @@ -447,37 +411,31 @@ lemma reachable_bisim: #H #tl #visited #visited_res #allv >(bisim_step_true … H) (* new_visited = hd::visited are all ok *) cut (all_true S (hd::visited)) - [#p #H1 cases (orb_true_l … H1) [#eqp <(\P eqp) @H |@allv]] + [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]] (* we now exploit the induction hypothesis *) - #allh #subH #bisim cases (Hind … allh … bisim) -Hind - [* #H1 #H2 #H3 % // % // #p #H4 @H2 @memb_cons //] - (* the only thing left to prove is the sub_sons invariant *) - #x #a #membx #memba - cases (orb_true_l … membx) + #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind + [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp + [cases (orb_true_l … membp) -membp #membp + [@memb_append_l2 >(\P membp) @memb_hd + |@memb_append_l1 @sublist_unique_append_l2 // + ] + |@memb_append_l2 @memb_cons // + ] + |(* the only thing left to prove is the sub_sons invariant *) + #x #membx cases (orb_true_l … membx) [(* case x = hd *) - #eqhdx >(proj1 … (eqb_true …) eqhdx) - (* xa is the son of x w.r.t. a; we must distinguish the case xa + #eqhdx <(\P eqhdx) #xa #membxa + (* xa is a son of x; we must distinguish the case xa was already visited form the case xa is new *) - letin xa ≝ 〈move S a (\fst (\fst x)), move S a (\fst (\snd x))〉 cases (true_or_false … (memb ? xa (x::visited))) [(* xa visited - trivial *) #membxa @memb_append_l2 // |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l - [>membxa // - |(* this can be probably improved *) - generalize in match memba; -memba elim l - [whd in ⊢ (??%?→?); #abs @False_ind /2/ - |#b #others #Hind #memba cases (orb_true_l … memba) #H - [>(proj1 … (eqb_true …) H) @memb_hd - |@memb_cons @Hind // - ] - ] - ] + [>membxa //|//] ] |(* case x in visited *) - #H1 letin xa ≝ 〈move S a (\fst (\fst x)), move S a (\fst (\snd x))〉 - cases (memb_append … (subH x a H1 memba)) + #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa)) [#H2 (cases (orb_true_l … H2)) - [#H3 @memb_append_l2 >(proj1 … (eqb_true …) H3) @memb_hd + [#H3 @memb_append_l2 <(\P H3) @memb_hd |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3 ] |#H2 @memb_append_l2 @memb_cons @H2 @@ -487,163 +445,60 @@ lemma reachable_bisim: ] qed. -(* pit state *) -let rec blank_item (S: DeqSet) (i: re S) on i :pitem S ≝ - match i with - [ z ⇒ `∅ - | e ⇒ ϵ - | s y ⇒ `y - | o e1 e2 ⇒ (blank_item S e1) + (blank_item S e2) - | c e1 e2 ⇒ (blank_item S e1) · (blank_item S e2) - | k e ⇒ (blank_item S e)^* ]. - -definition pit_pre ≝ λS.λi.〈blank_item S (|i|), false〉. - -let rec occur (S: DeqSet) (i: re S) on i ≝ - match i with - [ z ⇒ [ ] - | e ⇒ [ ] - | s y ⇒ [y] - | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) - | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) - | k e ⇒ occur S e]. - -axiom memb_single: ∀S,a,x. memb S a [x] = true → a = x. - -axiom tech: ∀b. b ≠ true → b = false. -axiom tech2: ∀b. b = false → b ≠ true. - -lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) = false → - move S a i = pit_pre S i. -#S #a #i elim i // - [#x cases (true_or_false (a==x)) - [#H >(proj1 …(eqb_true …) H) whd in ⊢ ((??%?)→?); - >(proj2 …(eqb_true …) (refl …)) whd in ⊢ ((??%?)→?); #abs @False_ind /2/ - |#H normalize >H // +definition equiv ≝ λSig.λre1,re2:re Sig. + let e1 ≝ •(blank ? re1) in + let e2 ≝ •(blank ? re2) in + let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in + let sig ≝ (occ Sig e1 e2) in + (bisim ? sig n [〈e1,e2〉] []). + +theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig. + \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \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)〉) + [(memb_single … H) @(ex_intro … ϵ) /2/ + |#p #_ normalize // ] - |#i1 #i2 #Hind1 #Hind2 #H >move_cat >Hind1 [2:@tech - @(not_to_not … (tech2 … H)) #H1 @sublist_unique_append_l1 //] - >Hind2 [2:@tech @(not_to_not … (tech2 … H)) #H1 @sublist_unique_append_l2 //] - // - |#i1 #i2 #Hind1 #Hind2 #H >move_plus >Hind1 [2:@tech - @(not_to_not … (tech2 … H)) #H1 @sublist_unique_append_l1 //] - >Hind2 [2:@tech @(not_to_not … (tech2 … H)) #H1 @sublist_unique_append_l2 //] - // - |#i #Hind #H >move_star >Hind // @H ] qed. -lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. -#S #a #i elim i // - [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // - |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // - |#i #Hind >move_star >Hind // - ] -qed. +definition eqbnat ≝ λn,m:nat. eqb n m. -lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. -#S #w #i elim w // #a #tl >moves_cons // -qed. - -lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) → - moves S w e = pit_pre S (\fst e). -#S #w elim w - [(* orribile *) - #e * #H @False_ind @H normalize #a #abs @False_ind /2/ - |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|)))) - [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) - @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb) - [#H2 <(proj1 … (eqb_true …) H2) // |#H2 @H1 //] - |#Hfalse >moves_cons >not_occur_to_pit // - ] - ] +lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m. +#n #m % [@eqb_true_to_eq | @eq_to_eqb_true] qed. - -definition occ ≝ λS.λe1,e2:pre S. - unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)). -(* definition occS ≝ λS:DeqSet.λoccur. - PSig S (λx.memb S x occur = true). *) +definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true. + +definition a ≝ s DeqNat 0. +definition b ≝ s DeqNat 1. +definition c ≝ s DeqNat 2. + +definition exp1 ≝ ((a·b)^*·a). +definition exp2 ≝ a·(b·a)^*. +definition exp4 ≝ (b·a)^*. + +definition exp6 ≝ a·(a ·a ·b^* + b^* ). +definition exp7 ≝ a · a^* · b^*. + +definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ). +definition exp9 ≝ (a·a·a + a·a·a·a·a)^*. + +example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true. +normalize // qed. -lemma occ_enough: ∀S.∀e1,e2:pre S. -(∀w.(sublist S w (occ S e1 e2))→ - (beqb (\snd (moves S w e1)) (\snd (moves ? w e2))) = true) \to -∀w.(beqb (\snd (moves S w e1)) (\snd (moves ? w e2))) = true. -#S #e1 #e2 #H #w -cut (sublist S w (occ S e1 e2) ∨ ¬(sublist S w (occ S e1 e2))) -[elim w - [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/ - |#a #tl * #subtl - [cases (true_or_false (memb S a (occ S e1 e2))) #memba - [%1 whd #x #membx cases (orb_true_l … membx) - [#eqax <(proj1 … (eqb_true …) eqax) // - |@subtl - ] - |%2 @(not_to_not … (tech2 … memba)) #H1 @H1 @memb_hd - ] - |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons // - ] - ] -|* [@H] - #H >to_pit - [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //] - >to_pit - [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //] - // -] -qed. -lemma bisim_char: ∀S.∀e1,e2:pre S. -(∀w.(beqb (\snd (moves S w e1)) (\snd (moves ? w e2))) = true) → -\sem{e1}=1\sem{e2}. -#S #e1 #e2 #H @(proj2 … (equiv_sem …)) #w @(\P ?) @H -qed. -lemma bisim_ok2: ∀S.∀e1,e2:pre S. - (beqb (\snd e1) (\snd e2) = true) → ∀n. - \fst (bisim S (occ S e1 e2) n (sons S (occ S e1 e2) 〈e1,e2〉) [〈e1,e2〉]) = true → - \sem{e1}=1\sem{e2}. -#S #e1 #e2 #Hnil #n -letin rsig ≝ (occ S e1 e2) -letin frontier ≝ (sons S rsig 〈e1,e2〉) -letin visited_res ≝ (\snd (bisim S rsig n frontier [〈e1,e2〉])) -#bisim_true -cut (bisim S rsig n frontier [〈e1,e2〉] = 〈true,visited_res〉) - [moves_empty >moves_empty moves_cons >moves_cons - @(Hind ? 〈?,?〉) [#x #H4 @Hsub @memb_cons //] - @(H1 〈?,?〉) [@visp| @Hsub @memb_hd]] #all_reach -@bisim_char @occ_enough -#w #Hsub @(H3 〈?,?〉) @(all_reach w Hsub 〈?,?〉) @H2 // -qed. - -(* -definition tt ≝ ps Bin true. -definition ff ≝ ps Bin false. -definition eps ≝ pe Bin. -definition exp1 ≝ (ff + tt · ff). -definition exp2 ≝ ff · (eps + tt). - -definition exp3 ≝ move Bin true (\fst (•exp1)). -definition exp4 ≝ move Bin true (\fst (•exp2)). -definition exp5 ≝ move Bin false (\fst (•exp1)). -definition exp6 ≝ move Bin false (\fst (•exp2)). *) diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma index 3f58c2c48..5894af561 100644 --- a/matita/matita/lib/re/re.ma +++ b/matita/matita/lib/re/re.ma @@ -82,10 +82,81 @@ let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝ | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2) | po E1 E2 ⇒ (forget ? E1) + (forget ? E2) | pk E ⇒ (forget ? E)^* ]. - + (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*) interpretation "forget" 'norm a = (forget ? a). +lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|). +// qed. + +lemma erase_plus : ∀S.∀i1,i2:pitem S. + |i1 + i2| = |i1| + |i2|. +// qed. + +lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. +// qed. + +(* boolean equality *) +let rec beqitem S (i1,i2: pitem S) on i1 ≝ + match i1 with + [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false] + | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false] + | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false] + | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false] + | po i11 i12 ⇒ match i2 with + [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 + | _ ⇒ false] + | pc i11 i12 ⇒ match i2 with + [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 + | _ ⇒ false] + | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false] + ]. + +lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). +#S #i1 elim i1 + [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct + |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct + |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct + [>(\P H) // | @(\b (refl …))] + |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct + [>(\P H) // | @(\b (refl …))] + |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % + normalize #H destruct + [cases (true_or_false (beqitem S i11 i21)) #H1 + [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H + |>H1 in H; normalize #abs @False_ind /2/ + ] + |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // + ] + |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % + normalize #H destruct + [cases (true_or_false (beqitem S i11 i21)) #H1 + [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H + |>H1 in H; normalize #abs @False_ind /2/ + ] + |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // + ] + |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] % + normalize #H destruct + [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //] + ] +qed. + +definition DeqItem ≝ λS. + mk_DeqSet (pitem S) (beqitem S) (beqitem_true S). + +unification hint 0 ≔ S; + X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) +(* ---------------------------------------- *) ⊢ + pitem S ≡ carr X. + +unification hint 0 ≔ S,i1,i2; + X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) +(* ---------------------------------------- *) ⊢ + beqitem S i1 i2 ≡ eqb X i1 i2. + +(* semantics *) + let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ match r with [ pz ⇒ ∅ @@ -158,6 +229,21 @@ lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e. #S * #i #b #btrue normalize in btrue; >btrue %2 // qed. +lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}. +#S #i #w % + [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) // + |* // + ] +qed. + +lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. +#S * #i * + [>sem_pre_true normalize in ⊢ (??%?); #w % + [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)] + |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ] + ] +qed. + definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). @@ -168,46 +254,29 @@ lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. -notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}. -interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e). +notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}. +interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e). lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. A = B → A =1 B. #S #A #B #H >H /2/ qed. lemma sem_pre_concat_r : ∀S,i.∀e:pre S. - \sem{i ◂ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. + \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] >sem_pre_true >sem_cat >sem_pre_true /2/ qed. -definition lc ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. +definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. match e1 with [ mk_Prod i1 b1 ⇒ match b1 with - [ true ⇒ (i1 ◂ (bcast ? i2)) + [ true ⇒ (i1 ◃ (bcast ? i2)) | false ⇒ 〈i1 · i2,false〉 ] ]. - -definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. - match e with - [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. -notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}. -interpretation "lc" 'lc op a b = (lc ? op a b). - -definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S. - match e with - [ mk_Prod i1 b1 ⇒ - match b1 with - [true ⇒ 〈(\fst (bcast ? i1))^*, true〉 - |false ⇒ 〈i1^*,false〉 - ] - ]. - -(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.*) -interpretation "lk" 'lk op a = (lk ? op a). -notation "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. +notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}. +interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b). notation "•" non associative with precedence 60 for @{eclose ?}. @@ -218,7 +287,7 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ | ps x ⇒ 〈 `.x, false〉 | pp x ⇒ 〈 `.x, false 〉 | po i1 i2 ⇒ •i1 ⊕ •i2 - | pc i1 i2 ⇒ •i1 ▸ i2 + | pc i1 i2 ⇒ •i1 ▹ i2 | pk i ⇒ 〈(\fst (•i))^*,true〉]. notation "• x" non associative with precedence 60 for @{'eclose $x}. @@ -229,15 +298,19 @@ lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. // qed. lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S. - •(i1 · i2) = •i1 ▸ i2. + •(i1 · i2) = •i1 ▹ i2. // qed. lemma eclose_star: ∀S:DeqSet.∀i:pitem S. •i^* = 〈(\fst(•i))^*,true〉. // qed. -definition reclose ≝ λS. lift S (eclose S). -interpretation "reclose" 'eclose x = (reclose ? x). +definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. + match e with + [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. + +definition preclose ≝ λS. lift S (eclose S). +interpretation "preclose" 'eclose x = (preclose ? x). (* theorem 16: 2 *) lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S. @@ -250,33 +323,23 @@ qed. lemma odot_true : ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ▸ i2 = i1 ◂ (•i2). + 〈i1,true〉 ▹ i2 = i1 ◃ (•i2). // qed. lemma odot_true_bis : ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. + 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. #S #i1 #i2 normalize cases (•i2) // qed. lemma odot_false: ∀S.∀i1,i2:pitem S. - 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉. + 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉. // qed. lemma LcatE : ∀S.∀e1,e2:pitem S. \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. // qed. -lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|). -// qed. - -lemma erase_plus : ∀S.∀i1,i2:pitem S. - |i1 + i2| = |i1| + |i2|. -// qed. - -lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. -// qed. - lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. #S #i elim i // [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot @@ -286,15 +349,17 @@ lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. | #i #IH >eclose_star >(erase_star … i) odot_false >sem_pre_false >sem_pre_false >sem_cat /2/ |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …)) @@ -303,33 +368,18 @@ lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S. @eqP_trans [|@eqP_sym @union_assoc ] /3/ ] qed. - -lemma sem_fst: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. -#S * #i * - [>sem_pre_true normalize in ⊢ (??%?); #w % - [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)] - |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ] - ] -qed. - -lemma item_eps: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}. -#S #i #w % - [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) // - |* // - ] -qed. -lemma sem_fst_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. +lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}). #S #e #i #A #seme -@eqP_trans [|@sem_fst] -@eqP_trans [||@eqP_union_r [|@eqP_sym @item_eps]] +@eqP_trans [|@minus_eps_pre] +@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]] @eqP_trans [||@distribute_substract] @eqP_substract_r // qed. (* theorem 16: 1 *) -theorem sem_bull: ∀S:DeqSet. ∀e:pitem S. \sem{•e} =1 \sem{e} ∪ \sem{|e|}. +theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}. #S #e elim e [#w normalize % [/2/ | * //] |/2/ @@ -352,15 +402,53 @@ theorem sem_bull: ∀S:DeqSet. ∀e:pitem S. \sem{•e} =1 \sem{e} ∪ \sem{|e| @eqP_trans [||@eqP_union_l [|@union_comm]] @eqP_trans [||@union_assoc] /2/ |#i #H >sem_pre_true >sem_star >erase_bull >sem_star - @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@sem_fst_aux //]]] + @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]] @eqP_trans [|@eqP_union_r [|@distr_cat_r]] @eqP_trans [|@union_assoc] @eqP_union_l >erase_star @eqP_sym @star_fix_eps ] qed. +(* blank item *) +let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝ + match i with + [ z ⇒ `∅ + | e ⇒ ϵ + | s y ⇒ `y + | o e1 e2 ⇒ (blank S e1) + (blank S e2) + | c e1 e2 ⇒ (blank S e1) · (blank S e2) + | k e ⇒ (blank S e)^* ]. + +lemma forget_blank: ∀S.∀e:re S.|blank S e| = e. +#S #e elim e normalize // +qed. + +lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅. +#S #e elim e + [1,2:@eq_to_ex_eq // + |#s @eq_to_ex_eq // + |#e1 #e2 #Hind1 #Hind2 >sem_cat + @eqP_trans [||@(union_empty_r … ∅)] + @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r + @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1 + |#e1 #e2 #Hind1 #Hind2 >sem_plus + @eqP_trans [||@(union_empty_r … ∅)] + @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1 + |#e #Hind >sem_star + @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind + ] +qed. + +theorem re_embedding: ∀S.∀e:re S. + \sem{•(blank S e)} =1 \sem{e}. +#S #e @eqP_trans [|@sem_bull] >forget_blank +@eqP_trans [|@eqP_union_r [|@sem_blank]] +@eqP_trans [|@union_comm] @union_empty_r. +qed. + +(* lefted operations *) definition lifted_cat ≝ λS:DeqSet.λe:pre S. - lift S (lc S eclose e). + lift S (pre_concat_l S eclose e). notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. @@ -381,6 +469,20 @@ lemma erase_odot:∀S.∀e1,e2:pre S. #S * #i1 * * #i2 #b2 // >odot_true_b // qed. +definition lk ≝ λS:DeqSet.λe:pre S. + match e with + [ mk_Prod i1 b1 ⇒ + match b1 with + [true ⇒ 〈(\fst (eclose ? i1))^*, true〉 + |false ⇒ 〈i1^*,false〉 + ] + ]. + +(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*) +interpretation "lk" 'lk a = (lk ? a). +notation "a^⊛" non associative with precedence 90 for @{'lk $a}. + + lemma ostar_true: ∀S.∀i:pitem S. 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉. // qed. @@ -394,10 +496,10 @@ lemma erase_ostar: ∀S.∀e:pre S. #S * #i * // qed. lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. - \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▸ i} ∪ { [ ] }. + \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }. #S #e1 #i -cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ true〉) [//] -#H >H cases (e1 ▸ i) #i1 #b1 cases b1 +cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//] +#H >H cases (e1 ▹ i) #i1 #b1 cases b1 [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc] @eqP_union_l /2/ |/2/ @@ -405,10 +507,10 @@ cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ true〉) [//] qed. lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i. - e1 ⊙ 〈i,false〉 = e1 ▸ i. + e1 ⊙ 〈i,false〉 = e1 ▹ i. #S #e1 #i -cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ false〉) [//] -cases (e1 ▸ i) #i1 #b1 cases b1 #H @H +cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//] +cases (e1 ▹ i) #i1 #b1 cases b1 #H @H qed. lemma sem_odot: @@ -426,7 +528,7 @@ theorem sem_ostar: ∀S.∀e:pre S. \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*. #S * #i #b cases b [>sem_pre_true >sem_pre_true >sem_star >erase_bull - @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@sem_fst_aux //]]] + @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]] @eqP_trans [|@eqP_union_r [|@distr_cat_r]] @eqP_trans [||@eqP_sym @distr_cat_r] @eqP_trans [|@union_assoc] @eqP_union_l @@ -434,4 +536,4 @@ theorem sem_ostar: ∀S.∀e:pre S. |>sem_pre_false >sem_pre_false >sem_star /2/ ] qed. - + -- 2.39.2