From 4aa597ac4bde578ba67f7d4ca3b8a7b8c2ba44a2 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 2 Mar 2012 17:07:30 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter8.ma | 61 ++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 24 deletions(-) diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma index 7db597522..838a5f9f6 100644 --- a/weblib/tutorial/chapter8.ma +++ b/weblib/tutorial/chapter8.ma @@ -59,27 +59,25 @@ lemma eq_to_ex_eq: ∀S.∀A,B:a href="cic:/matita/tutorial/chapter6/word.def(3 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 \triangleleft is summarized by the following, easy lemma: *) +(* The behaviour of ◃ is summarized by the following, easy lemma: *) -lemma sem_pre_concat_r : ∀S,i.∀e:pre S. - \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. -#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] ->sem_pre_true >sem_cat >sem_pre_true /2/ +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}. +#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. -(* The definition of $\bullet(-)$ (\verb+eclose+) and -$\triangleright$ (\verb+pre_concat_l+) are mutually recursive. -In this situation, a viable alternative that is usually simpler -to reason about, is to abstract one of the two functions with respect -to the other. We make the notation declarations explicit in this -case, for the sake of clarity. -*) +(* The definition of $•(-)$ (eclose) and ▹ (pre_concat_l) are mutually recursive. +In this situation, a viable alternative that is usually simpler to reason about, +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:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. +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 ◃ (bcast ? i2)) - | false ⇒ 〈i1 · i2,false〉 + [ 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〉 ] ]. @@ -90,20 +88,35 @@ interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b). notation "•" non associative with precedence 60 for @{eclose ?}. -let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ +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 ⇒ 〈 `∅, false 〉 - | pe ⇒ 〈 ϵ, true 〉 - | ps x ⇒ 〈 `.x, false〉 - | pp x ⇒ 〈 `.x, false 〉 - | po i1 i2 ⇒ •i1 ⊕ •i2 - | pc i1 i2 ⇒ •i1 ▹ i2 - | pk i ⇒ 〈(\fst (•i))^*,true〉]. + [ 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 〉 + | 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〉]. notation "• x" non associative with precedence 60 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). -(* Here are a few simple properties of •(-) *) +(* Here are a few simple properties of ▹ and •(-) *) + +lemma pcl_true : + ∀S.∀i1,i2:pitem S. + 〈i1,true〉 ▸ i2 = i1 ◂ (•i2). +// qed. + +lemma pcl_true_bis : + ∀S.∀i1,i2:pitem S. + 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. +#S #i1 #i2 normalize cases (•i2) // qed. + +lemma pcl_false: + ∀S.∀i1,i2:pitem S. + 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉. +// qed. lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. •(i1 + i2) = •i1 ⊕ •i2. -- 2.39.2