From 1e15bf5aab8c4d4bdefc1bca9084459a0442a847 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 08:45:22 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter10.ma | 321 +++++++++++++++++------------------ 1 file changed, 160 insertions(+), 161 deletions(-) diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma index 9eef6a350..24efb3e98 100644 --- a/weblib/tutorial/chapter10.ma +++ b/weblib/tutorial/chapter10.ma @@ -79,11 +79,11 @@ lemma bisim_to_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0 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〉 ?)) -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) +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 // + |cut (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S 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) [@Hsub @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a //] #occa + @(a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"memb_map/a … occa) ] qed. @@ -112,17 +112,17 @@ so we have just to check cofinality for any node we add to visited. Here is the extremely simple algorithm: *) -let rec bisim S l n (frontier,visited: list ?) on n ≝ +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 ⇒ 〈false,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 ⇒ 〈true,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 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〉 + 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〉 ] ]. @@ -134,44 +134,44 @@ if and only if all visited nodes are cofinal. The following results explicitly state the behaviour of bisim is the general case and in some relevant instances *) -lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. - bisim S l n frontier visited = +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 ⇒ 〈false,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 ⇒ 〈true,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 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〉 + 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〉 ] ]. #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 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〉. +#frontier #visited >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // qed. -lemma bisim_end: ∀Sig,l,m.∀visited: list ?. - bisim Sig l (S m) [] visited = 〈true,visited〉. -#n #visisted >unfold_bisim // +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〉. +#n #visisted >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // 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 // +lemma bisim_step_true: ∀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,1,0)"true/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 href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig 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 (pa title="cons" href="cic:/fakeuri.def(1)":/a:visited))) + (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a Sig l p)) frontier) (pa title="cons" href="cic:/fakeuri.def(1)":/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. -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 // +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〉. +#Sig #l #m #p #frontier #visited #test >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a whd in ⊢ (??%?); >test // qed. (* In order to prove termination of bisim we must be able to effectively @@ -181,95 +181,95 @@ enumerate all possible pres: *) #b cases b normalize // qed. *) -let rec pitem_enum S (i:re S) on i ≝ +let rec pitem_enum S (i:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a 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) + [ z ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/aspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/spanspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span S)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] + | e ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,2,1)"pe/a S)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] + | s y ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,3,1)"ps/a S y)a title="cons" href="cic:/fakeuri.def(1)":/a:(a href="cic:/matita/tutorial/chapter7/pitem.con(0,4,1)"pp/a S y)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] + | o i1 i2 ⇒ a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,6,1)"po/a S) (pitem_enum S i1) (pitem_enum S i2) + | c i1 i2 ⇒ a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,5,1)"pc/a S) (pitem_enum S i1) (pitem_enum S i2) + | k i ⇒ a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,7,1)"pk/a S) (pitem_enum S i) ]. -lemma pitem_enum_complete : ∀S.∀i:pitem S. - memb (DeqItem S) i (pitem_enum S (|i|)) = true. +lemma pitem_enum_complete : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) i (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/ai|)) 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 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)) // + |3,4:#c normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … c)) // + |5,6:#i1 #i2 #Hind1 #Hind2 @(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/chapter7/DeqItem.def(6)"DeqItem/a S)) // + |#i #Hind @(a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"memb_map/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S)) // ] qed. -definition pre_enum ≝ λS.λi:re S. - compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false]. +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]. -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〉)) +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〉)) // 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). +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). -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〉)) +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〉)) // 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 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 ?. +a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a ? 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="logical and" href="cic:/fakeuri.def(1)"∧/a + ∀p. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p 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="exists" href="cic:/fakeuri.def(1)"∃/aw.(a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1 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 (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p). -definition disjoint ≝ λS:DeqSet.λl1,l2. - ∀p:S. memb S p l1 = true → memb S p l2 = false. +definition disjoint ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λl1,l2. + ∀p:S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S p l1 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S p l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. (* We are ready to prove that bisim is correct; we use the invariant that at each call of bisim the two lists visited and frontier only contain nodes reachable from \langle e_1,e_2\rangle, 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} → - ∀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. +lemma bisim_correct: ∀S.∀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)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2} → + ∀l,n.∀frontier,visited:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ((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 title="norm" href="cic:/fakeuri.def(1)"|/aa 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="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a title="norm" href="cic:/fakeuri.def(1)"|/avisited|→ + a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"all_reachable/a S e1 e2 visited → + a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"all_reachable/a S e1 e2 frontier → + a href="cic:/matita/tutorial/chapter10/disjoint.def(5)"disjoint/a ? frontier visited → + a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/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 a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #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 //] + [#frontier #visited #abs * #unique #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … abs) + @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a @a href="cic:/matita/tutorial/chapter5/sublist_length.def(9)"sublist_length/a // * #e11 #e21 #membp + cut ((a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e11| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e21| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) + [|* #H1 #H2

a href="cic:/matita/tutorial/chapter9/same_kernel_moves.def(9)"same_kernel_moves/a // + |#m #HI * [#visited #vinv #finv >a href="cic:/matita/tutorial/chapter10/bisim_end.def(10)"bisim_end/a //] #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) + cut (a title="exists" href="cic:/fakeuri.def(1)"∃/aw.(a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1 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 (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p)) + [@(r_frontier … (a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a … ))] #rp + cut (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,1,0)"true/a) [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] + @(a href="cic:/matita/basics/logic/proj1.def(2)"proj1/a … (a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"equiv_sem/a … )) @same] #ptest + >(a href="cic:/matita/tutorial/chapter10/bisim_step_true.def(10)"bisim_step_true/a … ptest) @HI -HI + [<a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a // + |% [whd in ⊢ (??%?); >(disjoint … (a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a …)) whd in ⊢ (??%?); // + |#p1 #H (cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … 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 // + |whd % [@a href="cic:/matita/tutorial/chapter5/unique_append_unique.def(6)"unique_append_unique/a @(a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a … u_frontier)] + @a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"unique_append_elim/a #q #H + [cases (a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"memb_sons/a … (a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a … H)) -H + #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (w1a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])) + >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 >mw1 >mw2 >m1 >m2 % // + |@r_frontier @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a // ] - |@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 // + |@a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"unique_append_elim/a #q #H + [@a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a @(a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"filter_true/a … H) + |cut ((qa title="eqb" href="cic:/fakeuri.def(1)"=/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) + [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a //] + cases (a href="cic:/matita/basics/bool/andb_true.def(5)"andb_true/a … u_frontier) #notp #_ @(\bf ?) + @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"not_eq_true_false/a) #eqqp H // ] ] ] @@ -279,60 +279,60 @@ qed. and the sons of visited are either in visited or in the frontier; since 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). +definition all_true ≝ λS.λl.∀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/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p 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 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,1,0)"true/a). -definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). -memb ? x l1 = true → sublist ? (sons ? l x) l2. +definition sub_sons ≝ λS,l,l1,l2.∀x:(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 ? x l1 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 href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a ? (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a ? 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.∀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/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 #_ #_ >bisim_never #H destruct + [#fron #vis #vis_res #_ #_ >a href="cic:/matita/tutorial/chapter10/bisim_never.def(10)"bisim_never/a #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)))) + |#hd cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/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 hd)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a hd)))) [|(* case head of the frontier is non ok (absurd) *) - #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct] + #H #tl #vis #vis_res #allv >(a href="cic:/matita/tutorial/chapter10/bisim_step_false.def(10)"bisim_step_false/a … H) #_ #H1 destruct] (* frontier = hd:: tl and hd is ok *) - #H #tl #visited #visited_res #allv >(bisim_step_true … H) + #H #tl #visited #visited_res #allv >(a href="cic:/matita/tutorial/chapter10/bisim_step_true.def(10)"bisim_step_true/a … 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]] + cut (a href="cic:/matita/tutorial/chapter10/all_true.def(8)"all_true/a S (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited)) + [#p #H1 cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … 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 // + [#H1 #H2 % // #p #membp @H2 -H2 cases (a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"memb_append/a … membp) -membp #membp + [cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … membp) -membp #membp + [@a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a >(\P membp) @a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a + |@a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"sublist_unique_append_l2/a // ] - |@memb_append_l2 @memb_cons // + |@a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a // ] |(* the only thing left to prove is the sub_sons invariant *) - #x #membx cases (orb_true_l … membx) + #x #membx cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … 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 + cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? xa (xa title="cons" href="cic:/fakeuri.def(1)":/a:visited))) + [(* xa visited - trivial *) #membxa @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a // + |(* xa new *) #membxa @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"sublist_unique_append_l1/a @a href="cic:/matita/tutorial/chapter5/memb_filter_l.def(5)"memb_filter_l/a [>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 + #H1 #xa #membxa cases (a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"memb_append/a … (subH x … H1 … membxa)) + [#H2 (cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … H2)) + [#H3 @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a <(\P H3) @a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a + |#H3 @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"sublist_unique_append_l2/a @H3 ] - |#H2 @memb_append_l2 @memb_cons @H2 + |#H2 @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a @H2 ] ] ] @@ -343,57 +343,56 @@ qed. prove that two expressions are equivalente if and only if they define the same language. *) -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〉] []). +definition equiv ≝ λSig.λre1,re2:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a Sig. + let e1 ≝ a title="eclose" href="cic:/fakeuri.def(1)"•/a(a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a ? re1) in + 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]). -theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig. - \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}. +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 @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding] - cut (equiv ? re1 re2 = 〈true,\snd (equiv ? 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)〉) [(memb_single … H) @(ex_intro … ϵ) /2/ + |% // #p whd in ⊢ ((??%?)→?); #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |% // #p #H >(a href="cic:/matita/tutorial/chapter5/memb_single.def(5)"memb_single/a … H) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ |#p #_ normalize // ] ] qed. -lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m. -#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true] +definition eqbnat ≝ λn,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m. + +lemma eqbnat_true : ∀n,m. a href="cic:/matita/tutorial/chapter10/eqbnat.def(2)"eqbnat/a n m 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 n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. +#n #m % [@a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a | @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a] qed. -definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true. +definition DeqNat ≝ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a a href="cic:/matita/tutorial/chapter10/eqbnat_true.def(7)"eqbnat_true/a. -definition a ≝ s DeqNat O. -definition b ≝ s DeqNat (S O). -definition c ≝ s DeqNat (S (S O)). +definition a ≝ a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"s/a a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"DeqNat/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +definition b ≝ a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"s/a a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"DeqNat/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a). +definition c ≝ a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"s/a a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"DeqNat/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)). -definition exp1 ≝ ((a·b)^*·a). -definition exp2 ≝ a·(b·a)^*. -definition exp4 ≝ (b·a)^*. +definition exp1 ≝ ((a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/b.def(9)"b/a)a title="re star" href="cic:/fakeuri.def(1)"^/a*a title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a). +definition exp2 ≝ a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/a(a href="cic:/matita/tutorial/chapter10/b.def(9)"b/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a)a title="re star" href="cic:/fakeuri.def(1)"^/a*. +definition exp4 ≝ (a href="cic:/matita/tutorial/chapter10/b.def(9)"b/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a)a title="re star" href="cic:/fakeuri.def(1)"^/a*. -definition exp6 ≝ a·(a ·a ·b^* + b^* ). -definition exp7 ≝ a · a^* · b^*. +definition exp6 ≝ a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/a(a href="cic:/matita/tutorial/chapter10/a.def(9)"a/a a title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a a title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/b.def(9)"b/aa title="re star" href="cic:/fakeuri.def(1)"^/a* a title="re or" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/tutorial/chapter10/b.def(9)"b/aa title="re star" href="cic:/fakeuri.def(1)"^/a* ). +definition exp7 ≝ a href="cic:/matita/tutorial/chapter10/a.def(9)"a/a a title="re cat" href="cic:/fakeuri.def(1)"·/a a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re star" href="cic:/fakeuri.def(1)"^/a* a title="re cat" href="cic:/fakeuri.def(1)"·/a a href="cic:/matita/tutorial/chapter10/b.def(9)"b/aa title="re star" href="cic:/fakeuri.def(1)"^/a*. -definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ). -definition exp9 ≝ (a·a·a + a·a·a·a·a)^*. +definition exp8 ≝ a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/a(a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re star" href="cic:/fakeuri.def(1)"^/a* ). +definition exp9 ≝ (a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a a title="re or" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a)a title="re star" href="cic:/fakeuri.def(1)"^/a*. -example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true. +example ex1 : a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? (a href="cic:/matita/tutorial/chapter10/exp8.def(10)"exp8/aa title="re or" href="cic:/fakeuri.def(1)"+/aa href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. normalize // qed. - - - -- 2.39.2