From 102c93c0642ae14649d501332a075124ae18e5b3 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 11:50:58 +0000 Subject: [PATCH] commit by user utente2 --- weblib/tutorial/chapter10.ma | 49 ++++++++++++++++++------------------ 1 file changed, 24 insertions(+), 25 deletions(-) diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma index bfdf8016c..08c78c632 100644 --- a/weblib/tutorial/chapter10.ma +++ b/weblib/tutorial/chapter10.ma @@ -15,7 +15,7 @@ e1 and e2 are equivalent iff for any word w the states reachable through w are cofinal. *) theorem equiv_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2} a title="iff" href="cic:/fakeuri.def(1)"↔/a ∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2} a title="iff" href="cic:/fakeuri.def(1)"↔/a ∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉. #S #e1 #e2 % [#same_sem #w cut (∀b1,b2. a href="cic:/matita/basics/logic/iff.def(1)"iff/a (b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) (b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2)) @@ -34,8 +34,8 @@ definition occ ≝ λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1) a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|)) (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)). lemma occ_enough: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. -(∀w.(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2))→ a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉) - →∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉. +(∀w.(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2))→ a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉) + →∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉. #S #e1 #e2 #H #w cases (a href="cic:/matita/tutorial/chapter5/decidable_sublist.def(6)"decidable_sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2)) [@H] -H #H >a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"to_pit/a [2: @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 #a #memba @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"sublist_unique_append_l1/a @H1 //] @@ -47,7 +47,7 @@ qed. occurring the given regular expressions. *) lemma equiv_sem_occ: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. -(∀w.(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2))→ a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉) +(∀w.(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2))→ a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉) → a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}. #S #e1 #e2 #H @(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a … (a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"equiv_sem/a …)) @a href="cic:/matita/tutorial/chapter10/occ_enough.def(11)"occ_enough/a #w @H qed. @@ -60,7 +60,7 @@ w.r.t. moves, and all its members are cofinal. *) definition sons ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S.λp:(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S)a title="Product" href="cic:/fakeuri.def(1)"×/a(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S). - a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (λa.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p)),a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p))〉) l. + a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (λa.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p)),a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p))〉) l. lemma memb_sons: ∀S,l.∀p,q:(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S)a title="Product" href="cic:/fakeuri.def(1)"×/a(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S). a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a ? l q) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="exists" href="cic:/fakeuri.def(1)"∃/aa.(a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a q)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p a title="logical and" href="cic:/fakeuri.def(1)"∧/a @@ -76,9 +76,9 @@ definition is_bisim ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1, (* Using lemma equiv_sem_occ it is easy to prove the following result: *) lemma bisim_to_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?.∀e1,e2: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"is_bisim/a S l (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2) → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}. + a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"is_bisim/a S l (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2) → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}. #S #l #e1 #e2 #Hbisim #Hmemb @a href="cic:/matita/tutorial/chapter10/equiv_sem_occ.def(17)"equiv_sem_occ/a -#w #Hsub @(a href="cic:/matita/basics/logic/proj1.def(2)"proj1/a … (Hbisim a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2〉 ?)) +#w #Hsub @(a href="cic:/matita/basics/logic/proj1.def(2)"proj1/a … (Hbisim a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2〉 ?)) lapply Hsub @(a href="cic:/matita/basics/list/list_elim_left.def(10)"list_elim_left/a … w) [//] #a #w1 #Hind #Hsub >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a @(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a …(Hbisim …(Hind ?))) [#x #Hx @Hsub @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a // @@ -114,15 +114,15 @@ Here is the extremely simple algorithm: *) let rec bisim S l n (frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?) on n ≝ match n with - [ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 (* assert false *) + [ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 (* assert false *) | S m ⇒ match frontier with - [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉 + [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉 | cons hd tl ⇒ if a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a hd)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a hd)) then bisim S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited))) (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited) - else a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 + else a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 ] ]. @@ -137,26 +137,26 @@ case and in some relevant instances *) lemma unfold_bisim: ∀S,l,n.∀frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l n frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a match n with - [ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 (* assert false *) + [ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 (* assert false *) | S m ⇒ match frontier with - [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉 + [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉 | cons hd tl ⇒ if a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a hd)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a hd)) then a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited))) (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited) - else a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 + else a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉 ] ]. #S #l #n cases n // qed. lemma bisim_never: ∀S,l.∀frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉. #frontier #visited >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // qed. lemma bisim_end: ∀Sig,l,m.∀visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="nil" href="cic:/fakeuri.def(1)"[/a] visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="nil" href="cic:/fakeuri.def(1)"[/a] visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited〉. #n #visisted >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // qed. @@ -170,7 +170,7 @@ qed. lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/a:frontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/a:frontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visited〉. #Sig #l #m #p #frontier #visited #test >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a whd in ⊢ (??%?); >test // qed. @@ -202,20 +202,20 @@ lemma pitem_enum_complete : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pit qed. definition pre_enum ≝ λS.λi:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S. - a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉) (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S i) a title="cons" href="cic:/fakeuri.def(1)"[/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a;a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a]. + a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉) (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S i) a title="cons" href="cic:/fakeuri.def(1)"[/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a;a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a]. lemma pre_enum_complete : ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? e (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. -#S * #i #b @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqBool/a ? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉)) +#S * #i #b @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqBool/a ? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉)) // cases b normalize // qed. definition space_enum ≝ λS.λi1,i2:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S. - a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λe1,e2.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i1) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i2). + a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λe1,e2.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i1) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i2). lemma space_enum_complete : ∀S.∀e1,e2: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 (a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. -#S #e1 #e2 @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a … (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉)) + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 (a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#S #e1 #e2 @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a … (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉)) // qed. definition all_reachable ≝ λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. @@ -289,7 +289,7 @@ lemma bisim_complete: ∀S,l,n.∀frontier,visited,visited_res:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter10/all_true.def(8)"all_true/a S visited → a href="cic:/matita/tutorial/chapter10/sub_sons.def(8)"sub_sons/a S l visited (frontiera title="append" href="cic:/fakeuri.def(1)"@/avisited) → - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l n frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited_res〉 → + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l n frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visited_res〉 → a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"is_bisim/a S visited_res l a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a ? (frontiera title="append" href="cic:/fakeuri.def(1)"@/avisited) visited_res. #S #l #n elim n [#fron #vis #vis_res #_ #_ >a href="cic:/matita/tutorial/chapter10/bisim_never.def(10)"bisim_never/a #H destruct @@ -348,13 +348,13 @@ definition equiv ≝ λSig.λre1,re2:a href="cic:/matita/tutorial/chapter7/re.i let e2 ≝ a title="eclose" href="cic:/fakeuri.def(1)"•/a(a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a ? re2) in let n ≝ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a Sig (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|))) in let sig ≝ (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a Sig e1 e2) in - (a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a ? sig n a title="cons" href="cic:/fakeuri.def(1)"[/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉] a title="nil" href="cic:/fakeuri.def(1)"[/a]). + (a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a ? sig n a title="cons" href="cic:/fakeuri.def(1)"[/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉] a title="nil" href="cic:/fakeuri.def(1)"[/a]). theorem euqiv_sem : ∀Sig.∀e1,e2:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a Sig. a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? e1 e2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{e2}. #Sig #re1 #re2 % [#H @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"eqP_sym/a @a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"re_embedding/a] @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [||@a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"re_embedding/a] - cut (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? re1 re2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? re1 re2)〉) + cut (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? re1 re2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? re1 re2)〉) [