From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Mar 2012 17:07:30 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1913
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4aa597ac4bde578ba67f7d4ca3b8a7b8c2ba44a2;p=helm.git

commit by user andrea
---

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.