From: Andrea Asperti Date: Thu, 15 Dec 2011 15:19:42 +0000 (+0000) Subject: Hints sui DeqSets X-Git-Tag: make_still_working~2003 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ed35234de6912d85cb216d61fb523e50449be0b;p=helm.git Hints sui DeqSets --- diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma index a0a5a938d..c1b894a7d 100644 --- a/matita/matita/lib/re/lang.ma +++ b/matita/matita/lib/re/lang.ma @@ -17,6 +17,7 @@ include "arithmetics/nat.ma". include "basics/lists/list.ma". include "basics/sets.ma". +include "basics/deqsets.ma". definition word ≝ λS:DeqSet.list S. @@ -58,6 +59,24 @@ lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] qed. +(* derivative *) + +definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w). + +lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → + deriv S (A·B) a =1 (deriv S A a) · B. +#S #A #B #a #noteps #w normalize % + [* #w1 cases w1 + [* #w2 * * #_ #Aeps @False_ind /2/ + |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct + #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % // + ] + |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1)) + @(ex_intro … w2) % // % normalize // + ] +qed. + +(* star properties *) lemma espilon_in_star: ∀S.∀A:word S → Prop. A^* ϵ. #S #A @(ex_intro … [ ]) normalize /2/ diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index 4967bf059..c260a6d40 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -64,38 +64,21 @@ theorem move_ok: |normalize /2/ |normalize /2/ |normalize #x #w cases (true_or_false (a==x)) #H >H normalize - [>(proj1 … (eqb_true …) H) % - [* // #bot @False_ind //| #H1 destruct /2/] - |% [#bot @False_ind // - | #H1 destruct @(absurd ((a==a)=true)) - [>(proj2 … (eqb_true …) (refl …)) // | /2/] - ] + [>(\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 @iff_trans[|@sem_odot] >same_kernel >sem_cat_w - @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r % - [* #w1 * #w2 * * #eqw #w1in #w2in @(ex_intro … (a::w1)) - @(ex_intro … w2) % // % normalize // cases (HI1 w1) /2/ - |* #w1 * #w2 * cases w1 - [* #_ #H @False_ind /2/ - |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in - @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/ - ] - ] + @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w @iff_trans[|@sem_oplus] @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //] |#i1 #HI1 #w >move_star - @iff_trans[|@sem_ostar] >same_kernel >sem_star_w % - [* #w1 * #w2 * * #eqw #w1in #w2in - @(ex_intro … (a::w1)) @(ex_intro … w2) % // % normalize // - cases (HI1 w1 ) /2/ - |* #w1 * #w2 * cases w1 - [* #_ #H @False_ind /2/ - |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in - @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/ - ] - ] + @iff_trans[|@sem_ostar] >same_kernel >sem_star_w + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 ] qed. @@ -165,18 +148,6 @@ coinductive equiv (S:DeqSet) : pre S → pre S → Prop ≝ equiv S e1 e2. *) -definition beqb ≝ λb1,b2. - match b1 with - [ true ⇒ b2 - | false ⇒ notb b2 - ]. - -lemma beqb_ok: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2). -#b1 #b2 cases b1 cases b2 normalize /2/ -qed. - -definition Bin ≝ mk_DeqSet bool beqb beqb_ok. - let rec beqitem S (i1,i2: pitem S) on i1 ≝ match i1 with [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false] @@ -192,27 +163,53 @@ let rec beqitem S (i1,i2: pitem S) on i1 ≝ | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false] ]. -axiom beqitem_ok: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). +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_ok S). - -definition beqpre ≝ λS:DeqSet.λe1,e2:pre S. - beqitem S (\fst e1) (\fst e2) ∧ beqb (\snd e1) (\snd e2). - -definition beqpairs ≝ λS:DeqSet.λp1,p2:(pre S)×(pre S). - beqpre S (\fst p1) (\fst p2) ∧ beqpre S (\snd p1) (\snd p2). + mk_DeqSet (pitem S) (beqitem S) (beqitem_true S). -axiom beqpairs_ok: ∀S,p1,p2. iff (beqpairs S p1 p2 = true) (p1 = p2). - -definition space ≝ λS.mk_DeqSet ((pre S)×(pre S)) (beqpairs S) (beqpairs_ok S). - -(* (sons S l p) computes all sons of p relative to characters in l *) +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. -definition sons ≝ λS:DeqSet.λl:list S.λp:space S. +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. -lemma memb_sons: ∀S,l,p,q. memb (space S) p (sons S l q) = true → +lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true → ∃a.(move ? a (\fst (\fst q)) = \fst p ∧ move ? a (\fst (\snd q)) = \snd p). #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/] @@ -222,7 +219,7 @@ lemma memb_sons: ∀S,l,p,q. memb (space S) p (sons S l q) = true → ] qed. -let rec bisim S l n (frontier,visited: list (space S)) on n ≝ +let rec bisim S l n (frontier,visited: list ?) on n ≝ match n with [ O ⇒ 〈false,visited〉 (* assert false *) | S m ⇒ @@ -236,7 +233,7 @@ let rec bisim S l n (frontier,visited: list (space S)) on n ≝ ] ]. -lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list (space S). +lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. bisim S l n frontier visited = match n with [ O ⇒ 〈false,visited〉 (* assert false *) @@ -252,39 +249,39 @@ lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list (space S). ]. #S #l #n cases n // qed. -lemma bisim_never: ∀S,l.∀frontier,visited: list (space S). +lemma bisim_never: ∀S,l.∀frontier,visited: list ?. bisim S l O frontier visited = 〈false,visited〉. #frontier #visited >unfold_bisim // qed. -lemma bisim_end: ∀Sig,l,m.∀visited: list (space Sig). +lemma bisim_end: ∀Sig,l,m.∀visited: list ?. bisim Sig l (S m) [] visited = 〈true,visited〉. #n #visisted >unfold_bisim // qed. -lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list (space Sig). +lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?. beqb (\snd (\fst p)) (\snd (\snd p)) = true → bisim Sig l (S m) (p::frontier) visited = - bisim Sig l m (unique_append ? (filter ? (λx.notb(memb (space Sig) x (p::visited))) + bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited))) (sons Sig l p)) frontier) (p::visited). #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // qed. -lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list (space Sig). +lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?. 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 (space S). +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: list (space S). +definition frontier_inv ≝ λS.λfrontier,visited. uniqueb ? frontier = true ∧ -∀p. memb ? p 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 ∧ @@ -339,91 +336,98 @@ let rec pitem_enum S (i:re S) on i ≝ | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2) | k i ⇒ map ?? (pk S) (pitem_enum S i) ]. - -(* axiom pitem_enum_complete: ∀S:DeqSet.∀i: pitem S. - memb ((pitem S)×(pitem S)) i (pitem_enum ? (forget ? i)) = true. *) -(* -#i elim i - [// - |// - |* // - |* // - |#i1 #i2 #Hind1 #Hind2 @memb_compose // - |#i1 #i2 #Hind1 #Hind2 @memb_compose // - | -*) + +lemma pitem_enum_complete : ∀S.∀i:pitem S. + memb (DeqItem S) i (pitem_enum S (|i|)) = true. +#S #i elim i + [1,2:// + |3,4:#c normalize >(\b (refl … c)) // + |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) // + |#i #Hind @(memb_map (DeqItem S)) // + ] +qed. definition pre_enum ≝ λS.λi:re S. compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false]. + +lemma pre_enum_complete : ∀S.∀e:pre S. + memb ? e (pre_enum S (|\fst e|)) = true. +#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉)) +// cases b normalize // +qed. definition space_enum ≝ λS.λi1,i2:re S. - compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i1). + compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2). -axiom space_enum_complete : ∀S.∀e1,e2: pre S. - memb (space S) 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true. +lemma space_enum_complete : ∀S.∀e1,e2: pre S. + memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true. +#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 → + ∃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). + ∀l,n.∀frontier,visited:list (*(space S) *) ((pre S)×(pre S)). |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→ - visited_inv S e1 e2 visited → frontier_inv S frontier visited → + visited_inv_1 S e1 e2 visited → frontier_inv S 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) @le_to_not_lt @sublist_length // * #e11 #e21 #membp cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst 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 + * #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])) /2/] + [cases (vinv … visited_p2) -vinv #w1 * #mw1 #mw2 + @(ex_intro … (w1@[a])) % //] -movea2 -movea1 -a -visited_p2 -p2 #reachp 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 <(proj1 … (eqb_true (space Sig) ? p1) eqp) % // + @(\b ?) @(proj1 … (equiv_sem … )) @same] #ptest + >(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 % [@unique_append_unique @(andb_true_r … u_frontier)] - @unique_append_elim #q #H - [% - [@notb_eq_true_l @(filter_true … H) - |@(ex_intro … p) % // - @(memb_sons … (memb_filter_memb … H)) + |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 // ] - |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. -definition all_true ≝ λS.λl.∀p. memb (space S) p l = true → +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,a. -memb (space S) x l1 = true → memb S a l = true → - memb (space S) 〈move ? a (\fst (\fst x)), move ? a (\fst (\snd x))〉 l2 = 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. lemma reachable_bisim: - ∀S,l,n.∀frontier,visited,visited_res:list (space S). + ∀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〉 → @@ -435,7 +439,7 @@ lemma reachable_bisim: |#m #Hind * [(* case empty frontier *) -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?); - #H1 destruct % // % // #p /2/ + #H1 destruct % // % // #p /2 by / |#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] @@ -443,8 +447,7 @@ 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 #H cases (orb_true_l … H) - [#eqp <(proj1 … (eqb_true …) eqp) // |@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 //] @@ -456,7 +459,7 @@ lemma reachable_bisim: (* xa is the son of x w.r.t. a; 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 (space S) xa (x::visited))) + 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 // @@ -593,7 +596,7 @@ 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 @(proj1 …(beqb_ok …)) @H +#S #e1 #e2 #H @(proj2 … (equiv_sem …)) #w @(\P ?) @H qed. lemma bisim_ok2: ∀S.∀e1,e2:pre S. @@ -620,16 +623,17 @@ cut (sub_sons S rsig [〈e1,e2〉] (frontier@[〈e1,e2〉])) ] ] #init cases (reachable_bisim … allH init … H) * #H1 #H2 #H3 -cut (∀w.sublist ? w (occ S e1 e2)→∀p.memb (space S) p visited_res = true → - memb (space S) 〈moves ? w (\fst p), moves ? w (\snd p)〉 visited_res = true) - [#w elim w [//] +cut (∀w.sublist ? w (occ S e1 e2)→∀p.memb ? p visited_res = true → + memb ? 〈moves ? w (\fst p), moves ? w (\snd p)〉 visited_res = true) + [#w elim w [#_ #p #H4 >moves_empty >moves_empty moves_cons >moves_cons @(Hind ? 〈?,?〉) [#x #H4 @Hsub @memb_cons //] - @(H1 〈?,?〉) // @Hsub @memb_hd] #all_reach + @(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. @@ -639,7 +643,7 @@ 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)). +definition exp6 ≝ move Bin false (\fst (•exp2)). *)