definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
-(* The following function compute the list of characters occurring in a given
-item i. *)
+(* The following "occur" function compute the list of characters occurring in a
+given item i. We first define a special append function that appends two lists
+avoiding repetitions, and prove a few properties of it.
+*)
+
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒
+ let r ≝ unique_append S tl l2 in
+ if memb S a r then r else a::r
+ ].
+
+lemma memb_unique_append: ∀S,a,l1,l2.
+memb S a (unique_append S l1 l2) = true →
+ memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //]
+#b #tl #Hind #l2 cases (true_or_false … (a==b)) #Hab >Hab normalize /2/
+cases (memb S b (unique_append S tl l2)) normalize
+ [@Hind | >Hab normalize @Hind]
+qed.
+
+lemma unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2.
+(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
+∀x. memb S x (unique_append S l1 l2) = true → P x.
+#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx)
+/2/
+qed.
+
+lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+ uniqueb S (unique_append S l1 l2) = true.
+#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
+cases (true_or_false … (memb S a (unique_append S tl l2)))
+#H >H normalize [@Hind //] >H normalize @Hind //
+qed.
+
+definition sublist ≝
+ λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+lemma memb_exists: ∀S,a,l.memb S a l = true →
+ ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /2/]
+#b #tl #Hind #H cases (orb_true_l … H)
+ [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
+ |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+ @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+ ]
+qed.
+
+lemma sublist_length: ∀S,l1,l2.
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
+#S #l1 elim l1 //
+#a #tl #Hind #l2 #unique #sub
+cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub normalize >(\b (refl … a)) //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
+>eql2 in sub; #sub #x #membx
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+ [#membxl3 @memb_append_l1 //
+ |#membxal4 cases (orb_true_l … membxal4)
+ [#eqxa @False_ind lapply (andb_true_l … unique)
+ <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
+ ]
+ ]
+qed.
+
+lemma sublist_unique_append_l1:
+ ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
+#x #tl #Hind #l2 #a
+normalize cases (true_or_false … (a==x)) #eqax >eqax
+[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
+ [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize
+ [/2/ |>eqax normalize /2/]
+]
+qed.
+
+lemma sublist_unique_append_l2:
+ ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+#S #l1 elim l1 [normalize //] #x #tl #Hind normalize
+#l2 #a cases (memb S x (unique_append S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
+qed.
+
+lemma decidable_sublist:∀S,l1,l2.
+ (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
+#S #l1 #l2 elim l1
+ [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
+ |#a #tl * #subtl
+ [cases (true_or_false (memb S a l2)) #memba
+ [%1 whd #x #membx cases (orb_true_l … membx)
+ [#eqax >(\P eqax) // |@subtl]
+ |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 normalize
+ >(\b (refl … a)) //
+ ]
+ |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 normalize cases (x==a)
+ normalize //
+ ]
+ ]
+qed.
let rec occur (S: DeqSet) (i: re S) on i ≝
match i with
| 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].
+
+
(* If a symbol a does not occur in i, then move(i,a) gets to the
pit state. *)
(* We cannot escape form the pit state. *)
-lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+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 //
qed.
lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
-#S #w #i elim w //
-qed.
+#S #w #i elim w // #a #w1 #H normalize >move_pit @H
+qed.
(* If any character in w does not occur in i, then moves(i,w) gets
to the pit state. *)
-lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
- moves S w e = pit_pre S (\fst e).
+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|))))
+ |#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 //]
Regular Expressions Equivalence
*)
-include "tutorial/chapter9.ma".
+include "tutorial/chapter10.ma".
(* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and
only if b_1 = b_2. *)
definition cofinal ≝ λS.λp:(pre S)×(pre S).
- \snd (\fst p) = \snd (\snd p).
+ snd ?? (fst ?? p) = snd ?? (snd ?? p).
(* As a corollary of decidable_sem, we have that two expressions
e1 and e2 are equivalent iff for any word w the states reachable
through w are cofinal. *)
theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+ \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
#S #e1 #e2 %
[#same_sem #w
cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
to characters occurring in the given pres. *)
definition occ ≝ λS.λe1,e2:pre S.
- unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
+ 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〉)
lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
-→ \sem{e1}=1\sem{e2}.
+→ \sem{e1} ≐ \sem{e2}.
#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
qed.
*)
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.
+ 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).
+ ∃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]
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).
+(* We define an elimination principle for lists working on the tail, that we
+be used in the sequel *)
+
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l)
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
+
(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
- is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+ is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1} ≐ \sem{e2}.
#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
lapply Hsub @(list_elim_left … w) [//]
#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
+ |cut (memb S a (occ S e1 e2) = true)
+ [@Hsub @memb_append_l2 normalize >(\b (refl … a)) //] #occa
@(memb_map … occa)
]
qed.
match frontier with
[ nil ⇒ 〈true,visited〉
| cons hd tl ⇒
- if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ 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〉
match frontier with
[ nil ⇒ 〈true,visited〉
| cons hd tl ⇒
- if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ 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〉
qed.
lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
-beqb (\snd (\fst p)) (\snd (\snd p)) = true →
+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).
qed.
lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
-beqb (\snd (\fst p)) (\snd (\snd p)) = false →
+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 whd in ⊢ (??%?); >test //
qed.
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.
+ memb ? e (pre_enum S (|fst ?? e|)) = true.
#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
// cases b normalize //
qed.
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.
+ memb ? 〈e1,e2〉 ( space_enum S (|fst ?? e1|) (|fst ?? e2|)) = true.
+#S #e1 #e2 @(memb_compose ?? (DeqProd (DeqProd ??) (DeqProd ??)) (λi,b.〈i,b〉))
+// qed.
-definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?.
+definition all_reachable ≝ λS.λe1,e2:pre S.
+λl: list (DeqProd (DeqProd ??) (DeqProd ??)).
uniqueb ? l = true ∧
∀p. memb ? p l = true →
- ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
-
+ ∃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.
nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair
which is not cofinal. *)
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
+(* we first prove a few auxiliary results *)
+lemma memb_filter_memb: ∀S,f,a,l.
+ memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //] #b #tl #Hind normalize (cases (f b)) normalize
+cases (a==b) normalize // @Hind
+qed.
+
+lemma filter_true: ∀S,f,a,l.
+ memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /2/] #b #tl #Hind
+cases (true_or_false (f b)) #H normalize >H normalize [2:@Hind]
+cases (true_or_false (a==b)) #eqab [#_ >(\P eqab) // | >eqab normalize @Hind]
+qed.
+
+lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
+#S #f #x #l #fx elim l normalize //
+#b #tl #Hind cases (true_or_false (x==b)) #eqxb
+ [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
+ |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
+ ]
+qed.
+
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1} ≐ \sem{e2} →
∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
- |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
+ |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.
+ 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|))
+ cut ((|fst ?? e11| = |fst ?? e1|) ∧ (|fst ?? e21| = |fst ?? e2|))
[|* #H1 #H2 <H1 <H2 @space_enum_complete]
- cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
+ cases (H … membp) #w * normalize #we1 #we2 <we1 <we2 % >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))
+ 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)
+ cut (beqb (snd ?? (fst ?? p)) (snd ?? (snd ?? p)) = true)
[cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
@(proj1 … (equiv_sem … )) @same] #ptest
>(bisim_step_true … ptest) @HI -HI
|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 @(memb_filter_true … H)
+ [@injective_notb @(filter_true … H)
|cut ((q==p) = false)
[|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
cases (andb_true … u_frontier) #notp #_ @(\bf ?)
at the end frontier is empty, visited is hence a bisimulation. *)
definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
- (beqb (\snd (\fst p)) (\snd (\snd p)) = 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.
-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))))
+ |#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 *)
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 //|//]
+ |(* 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))
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 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}.
+ fst ?? (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
#Sig #re1 #re2 %
[#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
- cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
+ cut (equiv ? re1 re2 = 〈true,snd ?? (equiv ? re1 re2)〉)
[<H //] #Hcut
cases (bisim_complete … Hcut)
[2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
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.
+example ex1 : fst ?? (equiv ? (exp8+exp9) exp9) = true.
normalize // qed.
\ No newline at end of file
projects / helm.git / commitdiff