From: matitaweb Date: Fri, 2 Mar 2012 09:02:13 +0000 (+0000) Subject: Splitted chapter 7 X-Git-Tag: make_still_working~1919 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c65aeeb22bdc7bf289e5db108c358b199773c857;p=helm.git Splitted chapter 7 --- diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma index da90566e8..b9a35a8ad 100644 --- a/weblib/tutorial/chapter7.ma +++ b/weblib/tutorial/chapter7.ma @@ -1,4 +1,5 @@ -(* We shall apply all the previous machinery to the study of regular languages +(*

Regular Expressions

+We shall apply all the previous machinery to the study of regular languages and the constructions of the associated finite automata. *) include "tutorial/chapter6.ma". @@ -46,7 +47,8 @@ lemma rsem_star : ∀S.∀r: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1 // qed. -(* We now introduce pointed regular expressions, that are the main tool we shall +(*

Pointed Regular expressions

+We now introduce pointed regular expressions, that are the main tool we shall use for the construction of the automaton. A pointed regular expression is just a regular expression internally labelled with some additional points. Intuitively, points mark the positions inside the @@ -128,7 +130,8 @@ lemma erase_plus : ∀S.∀i1,i2:pitem S. lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. // qed. -(* Items and pres are very concrete datatypes: they can be effectively compared, +(*

Comparing items and pres

+Items and pres are very concrete datatypes: they can be effectively compared, and enumerated. In particular, we can define a boolean equality beqitem and a proof beqitem_true that it refects propositional equality, enriching the set (pitem S) to a DeqSet. *) @@ -195,7 +198,8 @@ unification hint 0 ≔ S,i1,i2; (* ---------------------------------------- *) ⊢ beqitem S i1 i2 ≡ eqb X i1 i2. -(* The intuitive semantic of a point is to mark the position where +(*

Semantics of pointed regular expression

+The intuitive semantic of a point is to mark the position where we should start reading the regular expression. The language associated to a pre is the union of the languages associated with its points. *) @@ -295,295 +299,3 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. ] 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). - -lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. -// qed. - -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 @{'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}. -#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] ->sem_pre_true >sem_cat >sem_pre_true /2/ -qed. - -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)) - | false ⇒ 〈i1 · i2,false〉 - ] - ]. - -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 ?}. - -let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ - match i with - [ pz ⇒ 〈 `∅, false 〉 - | pe ⇒ 〈 ϵ, true 〉 - | ps x ⇒ 〈 `.x, false〉 - | pp x ⇒ 〈 `.x, false 〉 - | po i1 i2 ⇒ •i1 ⊕ •i2 - | pc i1 i2 ⇒ •i1 ▹ i2 - | pk i ⇒ 〈(\fst (•i))^*,true〉]. - -notation "• x" non associative with precedence 60 for @{'eclose $x}. -interpretation "eclose" 'eclose x = (eclose ? x). - -lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. - •(i1 + i2) = •i1 ⊕ •i2. -// qed. - -lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S. - •(i1 · i2) = •i1 ▹ i2. -// qed. - -lemma eclose_star: ∀S:DeqSet.∀i:pitem S. - •i^* = 〈(\fst(•i))^*,true〉. -// qed. - -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. - \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. -#S * #i1 #b1 * #i2 #b2 #w % - [cases b1 cases b2 normalize /2/ * /3/ * /3/ - |cases b1 cases b2 normalize /2/ * /3/ * /3/ - ] -qed. - -lemma odot_true : - ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ▹ i2 = i1 ◃ (•i2). -// qed. - -lemma odot_true_bis : - ∀S.∀i1,i2:pitem S. - 〈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〉. -// qed. - -lemma LcatE : ∀S.∀e1,e2:pitem S. - \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. -// qed. - -lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. -#S #i elim i // - [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot - cases (•i1) #i11 #b1 cases b1 // odot_true_bis // - | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) 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 …)) - >erase_bull @eqP_trans [|@(eqP_union_l … H)] - @eqP_trans [|@eqP_union_l[|@union_comm ]] - @eqP_trans [|@eqP_sym @union_assoc ] /3/ - ] -qed. - -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 [|@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. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}. -#S #e elim e - [#w normalize % [/2/ | * //] - |/2/ - |#x normalize #w % [ /2/ | * [@False_ind | //]] - |#x normalize #w % [ /2/ | * // ] - |#i1 #i2 #IH1 #IH2 >eclose_dot - @eqP_trans [|@odot_dot_aux //] >sem_cat - @eqP_trans - [|@eqP_union_r - [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]] - @eqP_trans [|@union_assoc] - @eqP_trans [||@eqP_sym @union_assoc] - @eqP_union_l // - |#i1 #i2 #IH1 #IH2 >eclose_plus - @eqP_trans [|@sem_oplus] >sem_plus >erase_plus - @eqP_trans [|@(eqP_union_l … IH2)] - @eqP_trans [|@eqP_sym @union_assoc] - @eqP_trans [||@union_assoc] @eqP_union_r - @eqP_trans [||@eqP_sym @union_assoc] - @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 [|@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 (pre_concat_l S eclose e). - -notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. - -interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2). - -lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b. - 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉. -#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) // -qed. - -lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b. - 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉. -// -qed. - -lemma erase_odot:∀S.∀e1,e2:pre S. - |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|). -#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot // -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. - -lemma ostar_false: ∀S.∀i:pitem S. - 〈i,false〉^⊛ = 〈i^*, false〉. -// qed. - -lemma erase_ostar: ∀S.∀e:pre S. - |\fst (e^⊛)| = |\fst e|^*. -#S * #i * // qed. - -lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀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 - [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc] - @eqP_union_l /2/ - |/2/ - ] -qed. - -lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀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 -qed. - -lemma sem_odot: - ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}. -#S #e1 * #i2 * - [>sem_pre_true - @eqP_trans [|@sem_odot_true] - @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux // - |>sem_pre_false >eq_odot_false @odot_dot_aux // - ] -qed. - -(* theorem 16: 4 *) -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 [|@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 - @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps - |>sem_pre_false >sem_pre_false >sem_star /2/ - ] -qed. \ No newline at end of file diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma index dc7474e21..7aac6fabc 100644 --- a/weblib/tutorial/chapter8.ma +++ b/weblib/tutorial/chapter8.ma @@ -1,485 +1,294 @@ -include "re.ma". -include "basics/listb.ma". +include "tutorial/chapter7.ma". -let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝ - match E with +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). + +lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. +// qed. + +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 @{'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}. +#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] +>sem_pre_true >sem_cat >sem_pre_true /2/ +qed. + +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)) + | false ⇒ 〈i1 · i2,false〉 + ] + ]. + +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 ?}. + +let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ + match i with [ pz ⇒ 〈 `∅, false 〉 - | pe ⇒ 〈 ϵ, false 〉 - | ps y ⇒ 〈 `y, false 〉 - | pp y ⇒ 〈 `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)^⊛ ]. + | pe ⇒ 〈 ϵ, true 〉 + | ps x ⇒ 〈 `.x, false〉 + | pp x ⇒ 〈 `.x, false 〉 + | po i1 i2 ⇒ •i1 ⊕ •i2 + | pc i1 i2 ⇒ •i1 ▹ i2 + | pk i ⇒ 〈(\fst (•i))^*,true〉]. -lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. - move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2). -// qed. +notation "• x" non associative with precedence 60 for @{'eclose $x}. +interpretation "eclose" 'eclose x = (eclose ? x). -lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. - move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2). +lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. + •(i1 + i2) = •i1 ⊕ •i2. // qed. -lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S. - move S x i^* = (move ? x i)^⊛. +lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S. + •(i1 · i2) = •i1 ▹ i2. // qed. -definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e). - -lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b. - pmove ? x 〈i,b〉 = move ? x i. +lemma eclose_star: ∀S:DeqSet.∀i:pitem S. + •i^* = 〈(\fst(•i))^*,true〉. // qed. -lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b. - a::l1 = b::l2 → a = b. -#A #l1 #l2 #a #b #H destruct // -qed. - -lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S. - |\fst (move ? a i)| = |i|. -#S #a #i elim i // - [#i1 #i2 #H1 #H2 >move_cat >erase_odot // - |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); // +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. + \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. +#S * #i1 #b1 * #i2 #b2 #w % + [cases b1 cases b2 normalize /2/ * /3/ * /3/ + |cases b1 cases b2 normalize /2/ * /3/ * /3/ ] qed. -theorem move_ok: - ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S. - \sem{move ? a i} w ↔ \sem{i} (a::w). -#S #a #i elim i - [normalize /2/ - |normalize /2/ - |normalize /2/ - |normalize #x #w cases (true_or_false (a==x)) #H >H normalize - [>(\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 - @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 - @iff_trans[||@iff_sym @deriv_middot //] - @cat_ext_l @HI1 - ] -qed. - -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))]. - -lemma moves_empty: ∀S:DeqSet.∀e:pre S. - moves ? [ ] e = e. +lemma odot_true : + ∀S.∀i1,i2:pitem S. + 〈i1,true〉 ▹ i2 = i1 ◃ (•i2). // qed. -lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. - moves ? (a::w) e = moves ? w (move S a (\fst e)). +lemma odot_true_bis : + ∀S.∀i1,i2:pitem S. + 〈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〉. // 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 LcatE : ∀S.∀e1,e2:pitem S. + \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. +// 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 - [% /2/ * // #H destruct |% normalize /2/] +lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. +#S #i elim i // + [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot + cases (•i1) #i11 #b1 cases b1 // odot_true_bis // + | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) 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 …)) + >erase_bull @eqP_trans [|@(eqP_union_l … H)] + @eqP_trans [|@eqP_union_l[|@union_comm ]] + @eqP_trans [|@eqP_sym @union_assoc ] /3/ + ] qed. - -theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. - (\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 - @iff_trans [||@iff_sym @not_epsilon_sem] - @iff_trans [||@move_ok] @Hind - ] + +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 [|@minus_eps_pre] +@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]] +@eqP_trans [||@distribute_substract] +@eqP_substract_r // 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 // +(* theorem 16: 1 *) +theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}. +#S #e elim e + [#w normalize % [/2/ | * //] + |/2/ + |#x normalize #w % [ /2/ | * [@False_ind | //]] + |#x normalize #w % [ /2/ | * // ] + |#i1 #i2 #IH1 #IH2 >eclose_dot + @eqP_trans [|@odot_dot_aux //] >sem_cat + @eqP_trans + [|@eqP_union_r + [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]] + @eqP_trans [|@union_assoc] + @eqP_trans [||@eqP_sym @union_assoc] + @eqP_union_l // + |#i1 #i2 #IH1 #IH2 >eclose_plus + @eqP_trans [|@sem_oplus] >sem_plus >erase_plus + @eqP_trans [|@(eqP_union_l … IH2)] + @eqP_trans [|@eqP_sym @union_assoc] + @eqP_trans [||@union_assoc] @eqP_union_r + @eqP_trans [||@eqP_sym @union_assoc] + @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 [|@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. -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. +(* 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 moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. -#S #w #i elim w // -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/ - ] +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. - -(* bisimulation *) -definition cofinal ≝ λS.λp:(pre S)×(pre S). - \snd (\fst p) = \snd (\snd p). - -theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. - \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)) - [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]] - #Hcut @Hcut @iff_trans [|@decidable_sem] - @iff_trans [|@same_sem] @iff_sym @decidable_sem -|#H #w1 @iff_trans [||@decidable_sem] forget_blank +@eqP_trans [|@eqP_union_r [|@sem_blank]] +@eqP_trans [|@union_comm] @union_empty_r. qed. -definition occ ≝ λS.λe1,e2:pre S. - unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)). - -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. +(* lefted operations *) +definition lifted_cat ≝ λS:DeqSet.λe:pre S. + lift S (pre_concat_l S eclose e). -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. +notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. -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. +interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2). -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/] -#a #tl #Hind #p #q #H cases (orb_true_l … H) -H - [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H] +lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b. + 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉. +#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) // 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) - ] +lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b. + 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉. +// qed. - -(* the algorithm *) -let rec bisim S l n (frontier,visited: list ?) on n ≝ - match n with - [ O ⇒ 〈false,visited〉 (* assert false *) - | S m ⇒ - match frontier with - [ nil ⇒ 〈true,visited〉 - | cons hd tl ⇒ - if beqb (\snd (\fst hd)) (\snd (\snd hd)) then - bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited))) - (sons S l hd)) tl) (hd::visited) - else 〈false,visited〉 - ] - ]. -lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. - bisim S l n frontier visited = - match n with - [ O ⇒ 〈false,visited〉 (* assert false *) - | S m ⇒ - match frontier with - [ nil ⇒ 〈true,visited〉 - | cons hd tl ⇒ - if beqb (\snd (\fst hd)) (\snd (\snd hd)) then - bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) - (sons S l hd)) tl) (hd::visited) - else 〈false,visited〉 - ] - ]. -#S #l #n cases n // qed. - -lemma bisim_never: ∀S,l.∀frontier,visited: list ?. - bisim S l O frontier visited = 〈false,visited〉. -#frontier #visited >unfold_bisim // +lemma erase_odot:∀S.∀e1,e2:pre S. + |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|). +#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot // qed. -lemma bisim_end: ∀Sig,l,m.∀visited: list ?. - bisim Sig l (S m) [] visited = 〈true,visited〉. -#n #visisted >unfold_bisim // -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〉 + ] + ]. -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 ? x (p::visited))) - (sons Sig l p)) frontier) (p::visited). -#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // -qed. +(* 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 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. -lemma notb_eq_true_l: ∀b. notb b = true → b = false. -#b cases b normalize // -qed. +lemma ostar_true: ∀S.∀i:pitem S. + 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉. +// qed. -let rec pitem_enum S (i:re S) on i ≝ - match i with - [ z ⇒ [pz S] - | e ⇒ [pe S] - | s y ⇒ [ps S y; pp S y] - | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2) - | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2) - | k i ⇒ map ?? (pk S) (pitem_enum S i) - ]. +lemma ostar_false: ∀S.∀i:pitem S. + 〈i,false〉^⊛ = 〈i^*, false〉. +// qed. -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)) // +lemma erase_ostar: ∀S.∀e:pre S. + |\fst (e^⊛)| = |\fst e|^*. +#S * #i * // qed. + +lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀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 + [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc] + @eqP_union_l /2/ + |/2/ ] 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 // +lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀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 qed. - -definition space_enum ≝ λS.λi1,i2:re S. - compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2). - -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 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). - -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|→ - 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) - @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 #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 rp #w * #fstp #sndp (bisim_step_true … ptest) @HI -HI - [(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 - [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). -memb ? x l1 = true → sublist ? (sons ? l x) l2. - -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〉 → - 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 - [#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] - (* frontier = hd:: tl and hd is ok *) - #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]] - (* we now exploit the induction hypothesis *) - #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 <(\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 *) - 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 //|//] - ] - |(* case x in visited *) - #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa)) - [#H2 (cases (orb_true_l … H2)) - [#H3 @memb_append_l2 <(\P H3) @memb_hd - |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3 - ] - |#H2 @memb_append_l2 @memb_cons @H2 - ] - ] - ] +lemma sem_odot: + ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}. +#S #e1 * #i2 * + [>sem_pre_true + @eqP_trans [|@sem_odot_true] + @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux // + |>sem_pre_false >eq_odot_false @odot_dot_aux // ] qed. -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 // - ] +(* theorem 16: 4 *) +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 [|@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 + @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps + |>sem_pre_false >sem_pre_false >sem_star /2/ ] -qed. - -lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m. -#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true] -qed. - -definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true. - -definition a ≝ s DeqNat O. -definition b ≝ s DeqNat (S O). -definition c ≝ s DeqNat (S (S O)). - -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. - - - - - - - +qed. \ No newline at end of file diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma new file mode 100644 index 000000000..dc7474e21 --- /dev/null +++ b/weblib/tutorial/chapter9.ma @@ -0,0 +1,485 @@ +include "re.ma". +include "basics/listb.ma". + +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 〉 + | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2) + | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2) + | pk e ⇒ (move ? x e)^⊛ ]. + +lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. + move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2). +// qed. + +lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. + move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2). +// qed. + +lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S. + move S x i^* = (move ? x i)^⊛. +// qed. + +definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e). + +lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b. + pmove ? x 〈i,b〉 = move ? x i. +// qed. + +lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b. + a::l1 = b::l2 → a = b. +#A #l1 #l2 #a #b #H destruct // +qed. + +lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S. + |\fst (move ? a i)| = |i|. +#S #a #i elim i // + [#i1 #i2 #H1 #H2 >move_cat >erase_odot // + |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); // + ] +qed. + +theorem move_ok: + ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S. + \sem{move ? a i} w ↔ \sem{i} (a::w). +#S #a #i elim i + [normalize /2/ + |normalize /2/ + |normalize /2/ + |normalize #x #w cases (true_or_false (a==x)) #H >H normalize + [>(\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 + @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 + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 + ] +qed. + +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))]. + +lemma moves_empty: ∀S:DeqSet.∀e:pre S. + moves ? [ ] e = e. +// qed. + +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 + [% /2/ * // #H destruct |% normalize /2/] +qed. + +lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S. + |\fst (moves ? w e)| = |\fst e|. +#S #w elim w // +qed. + +theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. + (\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 + @iff_trans [||@iff_sym @not_epsilon_sem] + @iff_trans [||@move_ok] @Hind + ] +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 // +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. + \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)) + [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]] + #Hcut @Hcut @iff_trans [|@decidable_sem] + @iff_trans [|@same_sem] @iff_sym @decidable_sem +|#H #w1 @iff_trans [||@decidable_sem] 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 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. + +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/] +#a #tl #Hind #p #q #H cases (orb_true_l … H) -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 *) + | S m ⇒ + match frontier with + [ nil ⇒ 〈true,visited〉 + | cons hd tl ⇒ + if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited))) + (sons S l hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. + +lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. + bisim S l n frontier visited = + match n with + [ O ⇒ 〈false,visited〉 (* assert false *) + | S m ⇒ + match frontier with + [ nil ⇒ 〈true,visited〉 + | cons hd tl ⇒ + if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) + (sons S l hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. +#S #l #n cases n // qed. + +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 ?. + bisim Sig l (S m) [] visited = 〈true,visited〉. +#n #visisted >unfold_bisim // +qed. + +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 ? 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 ?. +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. + +lemma notb_eq_true_l: ∀b. notb b = true → b = false. +#b cases b normalize // +qed. + +let rec pitem_enum S (i:re S) on i ≝ + match i with + [ z ⇒ [pz S] + | e ⇒ [pe S] + | s y ⇒ [ps S y; pp S y] + | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2) + | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2) + | k i ⇒ map ?? (pk S) (pitem_enum S i) + ]. + +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 i2). + +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 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). + +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|→ + 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) + @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 #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 rp #w * #fstp #sndp (bisim_step_true … ptest) @HI -HI + [(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 + [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). +memb ? x l1 = true → sublist ? (sons ? l x) l2. + +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〉 → + 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 + [#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] + (* frontier = hd:: tl and hd is ok *) + #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]] + (* we now exploit the induction hypothesis *) + #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 <(\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 *) + 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 //|//] + ] + |(* case x in visited *) + #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa)) + [#H2 (cases (orb_true_l … H2)) + [#H3 @memb_append_l2 <(\P H3) @memb_hd + |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3 + ] + |#H2 @memb_append_l2 @memb_cons @H2 + ] + ] + ] + ] +qed. + +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 // + ] + ] +qed. + +lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m. +#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true] +qed. + +definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true. + +definition a ≝ s DeqNat O. +definition b ≝ s DeqNat (S O). +definition c ≝ s DeqNat (S (S O)). + +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. + + + + + + +