commit by user andrea

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 7db59752219008680d7ca079abce0e8e7a72705d..838a5f9f621aeefffeb0ba6859aa1be875d8c74e 100644 (file)
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -59,27 +59,25 @@ lemma eq_to_ex_eq: ∀S.∀A,B:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3
   A \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 B → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 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:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+  \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}.
+#S #i * #i1 #b1 cases b1 [2: @\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //] 
+>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
 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:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λbcast:∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λe1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λi2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
   match e1 with 
   [ mk_Prod i1 b1 ⇒ match b1 with 
-    [ true ⇒ (i1 ◃ (bcast ? i2)) 
-    | false ⇒ 〈i1 · i2,false〉
+    [ true ⇒ (i1 \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 (bcast ? i2)) 
+    | false ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
     ]
   ].
 
@@ -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: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on i : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 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 ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 ?, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
+  | pe ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6,  \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 〉
+  | ps x ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem pp" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6.x, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
+  | pp x ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem pp" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6.x, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
+  | po i1 i2 ⇒ •i1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 •i2
+  | pc i1 i2 ⇒ •i1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2
+  | pk i ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (•i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉].
   
 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.