X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter8.ma;h=0e3293c1e79186894105304f7d6d3b9eefe45e25;hb=c0ac63fead67ea1902e3d923ce877a2779cf501e;hp=905e6604a628d70087956466d4150030e08b816c;hpb=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma index 905e6604a..0e3293c1e 100644 --- a/weblib/tutorial/chapter8.ma +++ b/weblib/tutorial/chapter8.ma @@ -26,11 +26,11 @@ If we define then, we just have •(i1+i2) = •(i1)⊕ •(i2). *) -definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉. +img class="anchor" src="icons/tick.png" id="lo"definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. 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:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b1,b2. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,b1〉a title="oplus" href="cic:/fakeuri.def(1)"⊕/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b2〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem or" href="cic:/fakeuri.def(1)"+/ai2,b1a title="boolean or" href="cic:/fakeuri.def(1)"∨/ab2〉. +img class="anchor" src="icons/tick.png" id="lo_def"lemma lo_def: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b1,b2. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,b1a title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="oplus" href="cic:/fakeuri.def(1)"⊕/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b2a title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem or" href="cic:/fakeuri.def(1)"+/ai2,b1a title="boolean or" href="cic:/fakeuri.def(1)"∨/ab2a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. (* @@ -47,20 +47,20 @@ In turn, ◃ says how to concatenate an item with a pre, that is however extreme Let us come to the formalized definitions: *) -definition pre_concat_r ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - match e with [ mk_Prod i1 b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i1, b〉]. +img class="anchor" src="icons/tick.png" id="pre_concat_r"definition pre_concat_r ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + match e with [ mk_Prod i1 b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i1, ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a]. 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:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. +img class="anchor" src="icons/tick.png" id="eq_to_ex_eq"lemma eq_to_ex_eq: ∀S.∀A,B:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. A a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a B → A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B. #S #A #B #H >H #x % // qed. (* The behaviour of ◃ is summarized by the following, easy lemma: *) -lemma sem_pre_concat_r : ∀S,i.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{i a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e}. +img class="anchor" src="icons/tick.png" id="sem_pre_concat_r"lemma sem_pre_concat_r : ∀S,i.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{i a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a ea title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_prl" href="cic:/fakeuri.def(1)"}/a. #S #i * #i1 #b1 cases b1 [2: @a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"eq_to_ex_eq/a //] >a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a >a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"sem_cat/a >a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a /span class="autotactic"2span class="autotrace" trace /span/span/ qed. @@ -71,11 +71,11 @@ is to abstract one of the two functions with respect to the other. In particular we abstract pre_concat_l with respect to an input bcast function from items to pres. *) -definition pre_concat_l ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λbcast:∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S → a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λe1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λi2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +img class="anchor" src="icons/tick.png" id="pre_concat_l"definition pre_concat_l ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λbcast:∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S → a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λe1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λi2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. match e1 with [ mk_Prod i1 b1 ⇒ match b1 with [ true ⇒ (i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (bcast ? i2)) - | false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 + | false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a ] ]. @@ -86,59 +86,59 @@ 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: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on i : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ +img class="anchor" src="icons/tick.png" id="eclose"let rec eclose (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on i : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ match i with - [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a ?, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉 - | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a 〉 - | ps x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 - | pp x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉 + [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a ?, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a + | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a + | ps x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/aa title="pitem pp" href="cic:/fakeuri.def(1)"./ax, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a + | pp x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/aa title="pitem pp" href="cic:/fakeuri.def(1)"./ax, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a | po i1 i2 ⇒ •i1 a title="oplus" href="cic:/fakeuri.def(1)"⊕/a •i2 | pc i1 i2 ⇒ •i1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 - | pk i ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (•i))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉]. + | pk i ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (•i))a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a]. notation "• x" non associative with precedence 60 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). (* Here are a few simple properties of ▹ and •(-) *) -lemma pcl_true : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2). +img class="anchor" src="icons/tick.png" id="pcl_true"lemma pcl_true : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2). // qed. -lemma pcl_true_bis : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)〉. +img class="anchor" src="icons/tick.png" id="pcl_true_bis"lemma pcl_true_bis : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. #S #i1 #i2 normalize cases (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) // qed. -lemma pcl_false: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉. +img class="anchor" src="icons/tick.png" id="pcl_false"lemma pcl_false: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. -lemma eclose_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +img class="anchor" src="icons/tick.png" id="eclose_plus"lemma eclose_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="eclose" href="cic:/fakeuri.def(1)"•/a(i1 a title="pitem or" href="cic:/fakeuri.def(1)"+/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="eclose" href="cic:/fakeuri.def(1)"•/ai1 a title="oplus" href="cic:/fakeuri.def(1)"⊕/a a title="eclose" href="cic:/fakeuri.def(1)"•/ai2. // qed. -lemma eclose_dot: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +img class="anchor" src="icons/tick.png" id="eclose_dot"lemma eclose_dot: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="eclose" href="cic:/fakeuri.def(1)"•/a(i1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="eclose" href="cic:/fakeuri.def(1)"•/ai1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2. // qed. -lemma eclose_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="eclose" href="cic:/fakeuri.def(1)"•/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a* a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a(a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉. +img class="anchor" src="icons/tick.png" id="eclose_star"lemma eclose_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="eclose" href="cic:/fakeuri.def(1)"•/aia title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a(a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. (* The definition of •(-) (eclose) can then be lifted from items to pres in the obvious way. *) -definition lift ≝ λS.λf:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S →a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +img class="anchor" src="icons/tick.png" id="lift"definition lift ≝ λS.λf:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S →a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. match e with - [ mk_Prod i b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (f i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (f i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉]. + [ mk_Prod i b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (f i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (f i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a]. -definition preclose ≝ λS. a href="cic:/matita/tutorial/chapter8/lift.def(2)"lift/a S (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a S). +img class="anchor" src="icons/tick.png" id="preclose"definition preclose ≝ λS. a href="cic:/matita/tutorial/chapter8/lift.def(2)"lift/a S (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a S). interpretation "preclose" 'eclose x = (preclose ? x). (* Obviously, broadcasting does not change the carrier of the item, as it is easily proved by structural induction. *) -lemma erase_bull : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai)| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/ai|. +img class="anchor" src="icons/tick.png" id="erase_bull"lemma erase_bull : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai)a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a. #S #i elim i // [ #i1 #i2 #IH1 #IH2 >a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"erase_dot/a a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"eclose_dot/a cases (a title="eclose" href="cic:/fakeuri.def(1)"•/ai1) #i11 #b1 cases b1 // a href="cic:/matita/tutorial/chapter8/pcl_true_bis.def(5)"pcl_true_bis/a // @@ -156,8 +156,8 @@ sem_bullet \sem{•i} =1 \sem{i} ∪ \sem{|i|} The proof of sem_oplus is straightforward. *) -lemma sem_oplus: ∀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="oplus" href="cic:/fakeuri.def(1)"⊕/a e2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}. +img class="anchor" src="icons/tick.png" id="sem_oplus"lemma sem_oplus: ∀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="oplus" href="cic:/fakeuri.def(1)"⊕/a e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a. #S * #i1 #b1 * #i2 #b2 #w % [cases b1 cases b2 normalize /span class="autotactic"2span class="autotrace" trace /span/span/ * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ |cases b1 cases b2 normalize /span class="autotactic"2span class="autotrace" trace /span/span/ * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ @@ -174,13 +174,13 @@ sem_pcl_aux: Then, using the previous result, we prove sem_bullet by induction on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *) -lemma LcatE : ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a e2} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ae2|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e2}. +img class="anchor" src="icons/tick.png" id="LcatE"lemma LcatE : ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a e2a title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ae2a title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_pl" href="cic:/fakeuri.def(1)"}/a. // qed. -lemma sem_pcl_aux : ∀S.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/ai2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i2} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ai2|} → - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ai2|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i2}. +img class="anchor" src="icons/tick.png" id="sem_pcl_aux"lemma sem_pcl_aux : ∀S.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/ai2a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i2a title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ai2a title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a → + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ai2a title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i2a title="in_pl" href="cic:/fakeuri.def(1)"}/a. #S * #i1 #b1 #i2 cases b1 [2:#th >a href="cic:/matita/tutorial/chapter8/pcl_false.def(5)"pcl_false/a >a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"sem_pre_false/a >a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"sem_pre_false/a >a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"sem_cat/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"eq_to_ex_eq/a/span/span/ |#H >a href="cic:/matita/tutorial/chapter8/pcl_true.def(5)"pcl_true/a >a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a @(a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a … (a href="cic:/matita/tutorial/chapter8/sem_pre_concat_r.def(10)"sem_pre_concat_r/a …)) @@ -190,8 +190,8 @@ lemma sem_pcl_aux : ∀S.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1) ] qed. -lemma minus_eps_pre_aux: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀A. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a A → a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a (A a title="substraction" href="cic:/fakeuri.def(1)"-/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]}). +img class="anchor" src="icons/tick.png" id="minus_eps_pre_aux"lemma minus_eps_pre_aux: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀A. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a A → a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a (A a title="substraction" href="cic:/fakeuri.def(1)"-/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/aa title="singleton" href="cic:/fakeuri.def(1)"}/a). #S #e #i #A #seme @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter7/minus_eps_pre.def(10)"minus_eps_pre/a] @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [||@a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"eqP_union_r/a [|@a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"eqP_sym/a @a href="cic:/matita/tutorial/chapter7/minus_eps_item.def(9)"minus_eps_item/a]] @@ -199,7 +199,7 @@ lemma minus_eps_pre_aux: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.de @a href="cic:/matita/tutorial/chapter4/eqP_substract_r.def(3)"eqP_substract_r/a // qed. -theorem sem_bull: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a. ∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/ai} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/ai|}. +img class="anchor" src="icons/tick.png" id="sem_bull"theorem sem_bull: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a. ∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/aia title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a. #S #e elim e [#w normalize % [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | * //] |/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"eq_to_ex_eq/a/span/span/ @@ -238,20 +238,20 @@ having e as carrier and no point, and then broadcast a point in it. The semantic (blank e) is obviously the empty language: from the point of view of the automaton, it corresponds with the pit state. *) -let rec blank (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i :a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S ≝ +img class="anchor" src="icons/tick.png" id="blank"let rec blank (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i :a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S ≝ match i with [ z ⇒ a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a ? | e ⇒ a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a | s y ⇒ a title="pitem ps" href="cic:/fakeuri.def(1)"`/ay | o e1 e2 ⇒ (blank S e1) a title="pitem or" href="cic:/fakeuri.def(1)"+/a (blank S e2) | c e1 e2 ⇒ (blank S e1) a title="pitem cat" href="cic:/fakeuri.def(1)"·/a (blank S e2) - | k e ⇒ (blank S e)a title="pitem star" href="cic:/fakeuri.def(1)"^/a* ]. + | k e ⇒ (blank S e)a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a ]. -lemma forget_blank: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.a title="forget" href="cic:/fakeuri.def(1)"|/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S e| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e. +img class="anchor" src="icons/tick.png" id="forget_blank"lemma forget_blank: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.a title="forget" href="cic:/fakeuri.def(1)"|/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S ea title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e. #S #e elim e normalize // qed. -lemma sem_blank: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="empty set" href="cic:/fakeuri.def(1)"∅/a. +img class="anchor" src="icons/tick.png" id="sem_blank"lemma sem_blank: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S ea title="in_pl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="empty set" href="cic:/fakeuri.def(1)"∅/a. #S #e elim e [1,2:@a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"eq_to_ex_eq/a // |#s @a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"eq_to_ex_eq/a // @@ -267,8 +267,8 @@ lemma sem_blank: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)" ] qed. -theorem re_embedding: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/a(a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S e)} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{e}. +img class="anchor" src="icons/tick.png" id="re_embedding"theorem re_embedding: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="eclose" href="cic:/fakeuri.def(1)"•/a(a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S e)a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_l" href="cic:/fakeuri.def(1)"}/a. #S #e @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter8/sem_bull.def(12)"sem_bull/a] >a href="cic:/matita/tutorial/chapter8/forget_blank.def(4)"forget_blank/a @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"eqP_union_r/a [|@a href="cic:/matita/tutorial/chapter8/sem_blank.def(9)"sem_blank/a]] @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"union_comm/a] @a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"union_empty_r/a. @@ -280,36 +280,36 @@ qed. Plus and bullet have been already lifted from items to pres. We can now do a similar job for concatenation ⊙ and Kleene's star ⊛.*) -definition lifted_cat ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +img class="anchor" src="icons/tick.png" id="lifted_cat"definition lifted_cat ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter8/lift.def(2)"lift/a S (a href="cic:/matita/tutorial/chapter8/pre_concat_l.def(3)"pre_concat_l/a S a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a 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:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)),a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉. +img class="anchor" src="icons/tick.png" id="odot_true_b"lemma odot_true_b : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)),a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. #S #i1 #i2 #b normalize in ⊢ (??%?); cases (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) // qed. -lemma odot_false_b : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2 ,b〉. +img class="anchor" src="icons/tick.png" id="odot_false_b"lemma odot_false_b : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2 ,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. -lemma erase_odot:∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2)| 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="re cat" 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|). +img class="anchor" src="icons/tick.png" id="erase_odot"lemma erase_odot:∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2)a title="forget" href="cic:/fakeuri.def(1)"|/a 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 e1a title="forget" href="cic:/fakeuri.def(1)"|/a a title="re cat" 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 e2a title="forget" href="cic:/fakeuri.def(1)"|/a). #S * #i1 * * #i2 #b2 // >a href="cic:/matita/tutorial/chapter8/odot_true_b.def(6)"odot_true_b/a >a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"erase_dot/a // qed. (* Let us come to the star operation: *) -definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +img class="anchor" src="icons/tick.png" id="lk"definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. match e with [ mk_Prod i1 b1 ⇒ match b1 with - [true ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a ? i1))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 - |false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 + [true ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a ? i1))a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a + |false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a ] ]. @@ -317,22 +317,22 @@ definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)" interpretation "lk" 'lk a = (lk ? a). notation "a^⊛" non associative with precedence 90 for @{'lk $a}. -lemma ostar_true: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉. +img class="anchor" src="icons/tick.png" id="ostar_true"lemma ostar_true: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. -lemma ostar_false: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉. +img class="anchor" src="icons/tick.png" id="ostar_false"lemma ostar_false: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aia title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. // qed. -lemma erase_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (ea title="lk" href="cic:/fakeuri.def(1)"^/a⊛)| 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 e|a title="re star" href="cic:/fakeuri.def(1)"^/a*. +img class="anchor" src="icons/tick.png" id="erase_ostar"lemma erase_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (ea title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a)a title="forget" href="cic:/fakeuri.def(1)"|/a 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 ea title="forget" href="cic:/fakeuri.def(1)"|/aa title="re star" href="cic:/fakeuri.def(1)"^/aa title="re star" href="cic:/fakeuri.def(1)"*/a. #S * #i * // qed. -lemma sem_odot_true: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/a a title="nil" href="cic:/fakeuri.def(1)"[/a ] }. +img class="anchor" src="icons/tick.png" id="sem_odot_true"lemma sem_odot_true: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a ia title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/a a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a a title="singleton" href="cic:/fakeuri.def(1)"}/a. #S #e1 #i -cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉) [//] +cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a) [//] #H >H cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) #i1 #b1 cases b1 [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a @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/chapter4/union_assoc.def(3)"union_assoc/a] @a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"eqP_union_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"eqP_sym/a/span/span/ @@ -340,18 +340,18 @@ cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair ] qed. -lemma eq_odot_false: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. - e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i. +img class="anchor" src="icons/tick.png" id="eq_odot_false"lemma eq_odot_false: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. + e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i. #S #e1 #i -cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉) [//] +cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a) [//] cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) #i1 #b1 cases b1 #H @H qed. (* We conclude this section with the proof of the main semantic properties of ⊙ and ⊛. *) -lemma sem_odot: - ∀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="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}. +img class="anchor" src="icons/tick.png" id="sem_odot"lemma sem_odot: + ∀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="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/aa title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2a title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a. #S #e1 * #i2 * [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter8/sem_odot_true.def(10)"sem_odot_true/a] @@ -360,8 +360,8 @@ lemma sem_odot: ] qed. -theorem sem_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="lk" href="cic:/fakeuri.def(1)"^/a⊛} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e} a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|}a title="star lang" href="cic:/fakeuri.def(1)"^/a*. +img class="anchor" src="icons/tick.png" id="sem_ostar"theorem sem_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/aa title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/aa title="in_l" href="cic:/fakeuri.def(1)"}/aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a. #S * #i #b cases b [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a >a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a >a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"sem_star/a >a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"erase_bull/a @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"eqP_union_r/a[|@a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"cat_ext_l/a [|@a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"minus_eps_pre_aux/a //]]]