From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Sat, 21 Jul 2012 14:07:48 +0000 (+0000)
Subject: An executable version of the tutorial.
X-Git-Tag: make_still_working~1599
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

An executable version of the tutorial.
---

diff --git a/matita/matita/lib/tutorial/chapter10.ma b/matita/matita/lib/tutorial/chapter10.ma
new file mode 100644
index 000000000..2a5da62ac
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter10.ma
@@ -0,0 +1,397 @@
+(* 
+Regular Expressions Equivalence
+*)
+
+include "tutorial/chapter9.ma".
+
+(* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and 
+only if b_1 = b_2. *)
+
+definition cofinal ≝ λS.λp:(pre S)×(pre S). 
+  \snd (\fst p) = \snd (\snd p).
+
+(* As a corollary of decidable_sem, we have that two expressions
+e1 and e2 are equivalent iff for any word w the states reachable 
+through w are cofinal. *)
+
+theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. 
+  \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 % 
+[#same_sem #w 
+  cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2)) 
+    [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
+  #Hcut @Hcut @iff_trans [|@decidable_sem] 
+  @iff_trans [|@same_sem] @iff_sym @decidable_sem
+|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
+qed.
+
+(* This does not directly imply decidability: we have no bound over the
+length of w; moreover, so far, we made no assumption over the cardinality 
+of S. Instead of requiring S to be finite, we may restrict the analysis
+to characters occurring in the given pres. *)
+
+definition occ ≝ λS.λe1,e2:pre S. 
+  unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
+
+lemma occ_enough: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+ →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 #H #w
+cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba  @sublist_unique_append_l2 @H1 //]
+ //
+qed.
+
+(* The following is a stronger version of equiv_sem, relative to characters
+occurring the given regular expressions. *)
+
+lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+→ \sem{e1}=1\sem{e2}.
+#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H 
+qed.
+
+(* 
+Bisimulations
+
+
+We say that a list of pairs of pres is a bisimulation if it is closed
+w.r.t. moves, and all its members are cofinal.
+*)
+
+definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S). 
+ map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
+
+lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
+  ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
+      move ? a (\fst (\snd q)) = \snd p).
+#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/] 
+#a #tl #Hind #p #q #H cases (orb_true_l … H) -H
+  [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
+qed.
+
+definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
+  ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+
+(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+
+lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. 
+  is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ 
+#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves 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)
+  ]
+qed.
+
+(* This is already an interesting result: checking if l is a bisimulation 
+is decidable, hence we could generate l with some untrusted piece of code 
+and then run a (boolean version of) is_bisim to check that it is actually 
+a bisimulation. 
+However, in order to prove that equivalence of regular expressions
+is decidable we must prove that we can always effectively build such a list 
+(or find a counterexample).
+The idea is that the list we are interested in is just the set of 
+all pair of pres reachable from the initial pair via some
+sequence of moves. 
+
+The algorithm for computing reachable nodes in graph is a very 
+traditional one. We split nodes in two disjoint lists: a list of 
+visited nodes and a frontier, composed by all nodes connected
+to a node in visited but not visited already. At each step we select a node 
+a from the frontier, compute its sons, add a to the set of 
+visited nodes and the (not already visited) sons to the frontier. 
+
+Instead of fist computing reachable nodes and then performing the 
+bisimilarity test we can directly integrate it in the algorithm:
+the set of visited nodes is closed by construction w.r.t. reachability,
+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 ≝
+  match n with 
+  [ O ⇒ 〈false,visited〉 (* assert false *)
+  | S m ⇒ 
+    match frontier with
+    [ nil ⇒ 〈true,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〉
+    ]
+  ].
+
+(* The integer n is an upper bound to the number of recursive call, 
+equal to the dimension of the graph. It returns a pair composed
+by a boolean and a the set of visited nodes; the boolean is true
+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 =
+  match n with 
+  [ O ⇒ 〈false,visited〉 (* assert false *)
+  | S m ⇒ 
+    match frontier with
+    [ nil ⇒ 〈true,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〉
+    ]
+  ].
+#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 // 
+qed.
+
+lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
+  bisim Sig l (S m) [] visited = 〈true,visited〉.
+#n #visisted >unfold_bisim // 
+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 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 whd in ⊢ (??%?); >test // 
+qed.
+
+(* In order to prove termination of bisim we must be able to effectively 
+enumerate all possible pres: *)
+ 
+(* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
+#b cases b normalize //
+qed. *)
+
+let rec pitem_enum S (i:re 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)
+  ].
+  
+lemma pitem_enum_complete : ∀S.∀i:pitem S.
+  memb (DeqItem S) i (pitem_enum S (|i|)) = true.
+#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)) //
+  ]
+qed.
+
+definition pre_enum ≝ λS.λi:re S.
+  compose ??? (λi,b.〈i,b〉) ( pitem_enum S i) (true::false::[]).
+  
+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〉))
+// 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).
+
+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〉))
+// 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 disjoint ≝ λS:DeqSet.λl1,l2.
+  ∀p:S. memb S p l1 = true →  memb S p l2 = false.
+        
+(* 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 〈e_1,e_2〉, 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.
+#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 <H1 <H2 @space_enum_complete]
+   cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //    
+  |#m #HI * [#visited #vinv #finv >bisim_end //]
+   #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)
+    [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?) 
+     @(proj1 … (equiv_sem … )) @same] #ptest 
+   >(bisim_step_true … ptest) @HI -HI 
+     [<plus_n_Sm //
+     |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
+        |#p1 #H (cases (orb_true_l … 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 //
+       ]
+     |@unique_append_elim #q #H
+       [@injective_notb @(memb_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 <notp <eqqp >H //
+       ]
+     ]
+   ]  
+qed.  
+
+(* For completeness, we use the invariant that all the nodes in visited are cofinal, 
+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 sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). 
+memb ? x l1 = true → sublist ? (sons ? 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 elim n
+  [#fron #vis #vis_res #_ #_ >bisim_never #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))))
+      [|(* case head of the frontier is non ok (absurd) *)
+       #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
+     (* frontier = hd:: tl and hd is ok *)
+     #H #tl #visited #visited_res #allv >(bisim_step_true … 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]]
+     (* 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 // 
+          ]
+        |@memb_append_l2 @memb_cons //
+        ] 
+      |(* the only thing left to prove is the sub_sons invariant *)  
+     #x #membx cases (orb_true_l … 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
+          [>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
+          ]
+        |#H2 @memb_append_l2 @memb_cons @H2
+        ]
+      ]
+    ]
+  ]
+qed.
+
+(* We can now give the definition of the equivalence algorithm, and
+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〉::[]) []).
+
+theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
+   \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{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 //] #Hcut
+   cases (bisim_complete … Hcut) 
+     [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/] 
+   #Hbisim #Hsub @(bisim_to_sem … Hbisim) 
+   @Hsub @memb_hd
+  |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2))) 
+    [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
+    |// 
+    |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/  
+    |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
+    |#p #_ normalize //
+    ]
+  ]
+qed.
+
+definition eqbnat ≝ λn,m:nat. eqb n m.
+
+lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
+#n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
+qed.
+
+definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
+
+definition a ≝ s DeqNat O.
+definition b ≝ s DeqNat (S O).
+definition c ≝ s DeqNat (S (S O)).
+
+definition exp1 ≝ ((a·b)^*·a).
+definition exp2 ≝ a·(b·a)^*.
+definition exp4 ≝ (b·a)^*.
+
+definition exp6 ≝ a·(a ·a ·b^* + b^* ).
+definition exp7 ≝ a · a^* · b^*.
+
+definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
+definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+
+example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
+normalize // qed.
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter3.ma b/matita/matita/lib/tutorial/chapter3.ma
new file mode 100644
index 000000000..a6a05a7b6
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter3.ma
@@ -0,0 +1,338 @@
+(*
+Polymorphism and Higher Order
+
+*)
+include "tutorial/chapter2.ma".
+include "basics/bool.ma".
+
+(* Matita supports polymorphic data types. The most typical case are polymorphic
+lists, parametric in the type of their elements: *)
+
+inductive list (A:Type[0]) : Type[0] ≝
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+(* The type notation list A is the type of all lists with elements of type A: 
+it is defined by two constructors: a polymorphic empty list (nil A) and a cons 
+operation, adding a new head element of type A to a previous list. For instance, 
+(list nat) and and (list bool) are lists of natural numbers and booleans, 
+respectively. But we can also form more complex data types, like 
+(list (list (nat → nat))), that is a list whose elements are lists of functions 
+from natural numbers to natural numbers.
+
+Typical elements in (list bool) are for instance,
+  nil nat                                    - the empty list of type nat
+  cons nat true (nil nat)                    - the list containing true
+  cons nat false (cons nat (true (nil nat))) - the list containing false and true
+and so on. 
+
+Note that both constructos nil and cons are expecting in input the type parameter:
+in this case, bool.
+*)
+
+(*
+Defining your own notation
+
+We now add a bit of notation, in order to make the syntax more readable. In 
+particular, we would like to write [] instead of (nil A) and a::l instead of 
+(cons A a l), leaving the system the burden to infer A, whenever possible.
+*)
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+(* 
+Basic operations on lists
+
+Let us define a few basic functions over lists. Our first example is the 
+append function, concatenating two lists l1 and l2. The natural way is to proceed 
+by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl 
+then we recursively append tl and l2 , and then add hd as first element. Note that 
+the append function itself is polymorphic, and the first argument it takes in input 
+is the type A of the elements of two lists l1 and l2. 
+Moreover, since the append function takes in input several parameters, we must also 
+specify in the its defintion on which one of them we are recurring: in this case l1.
+If not othewise specified, recursion is supposed to act on the first argument of the
+function.*)
+
+let rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :: append A tl l2 ].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+(* As usual, the function is executable. For instance, (append A nil l) reduces to
+l, as shown by the following example: *)
+
+example nil_append: ∀A.∀l:list A. [] @ l = l.
+#A #l normalize // qed.
+
+(* Proving that l @ [] = l is just a bit more complex. The situation is exactly 
+the same as for the addition operation of the previous chapter: since append is 
+defined by recutsion over the first argument, the computation of l @ [] is stuck, 
+and we must proceed by induction on l *) 
+
+lemma append_nil: ∀A.∀l:list A.l @ [] = l.
+#A #l (elim l) normalize // qed.
+
+(* similarly, we can define the two functions head and tail. Since we can only define
+total functions, we should decide what to do in case the input list is empty. 
+For tl, it is natural to return the empty list; for hd, we take in input a default 
+element d of type A to return in this case. *)
+
+definition head ≝ λA.λl: list A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝  λA.λl: list A.
+  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+
+example ex_head: ∀A.∀a,d,l. head A (a::l) d = a.
+#A #a #d #l normalize // qed.
+
+example ex_tail: tail ? (cons ? true []) = [].
+normalize // qed.
+
+theorem associative_append: 
+∀A.∀l1,l2,l3: list A. (l1 @ l2) @ l3 = l1 @ (l2 @ l3).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+(* Problemi con la notazione *)
+lemma a_append: ∀A.∀a.∀l:list A. (a::[]) @ l = a::l.
+// qed.
+
+theorem append_cons:
+∀A.∀a:A.∀l,l1: list A.l@(a::l1)= (l @ (cons ? a [])) @ l1.
+// qed. 
+
+(* Other typical functions over lists are those computing the length 
+of a list, and the function returning the nth element *)
+
+let rec length (A:Type[0]) (l:list A) on l ≝ 
+match l with 
+  [ nil ⇒ O
+    | cons a tl ⇒ S (length A tl)].
+
+let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
+  match n with
+    [O ⇒ head A l d
+    |S m ⇒ nth m A (tail A l) d].
+
+example ex_length: length ? (cons ? O []) = S O.
+normalize // qed.
+
+example ex_nth: nth (S O) ? (cons ? (S O) (cons ? O [])) O = O.
+normalize // qed.
+
+(* Proving that the length of l1@l2 is the sum of the lengths of l1
+and l2 just requires a trivial induction on the first list. *)
+
+ lemma  length_add: ∀A.∀l1,l2:list A. 
+  length ? (l1@l2) = add (length ? l1) (length ? l2).
+#A #l1 elim l1 normalize // qed. 
+
+(* 
+Comparing Costructors
+
+Let us come to a more interesting question. How can we prove that the empty 
+list is different from any list with at least one element, that is from any list 
+of the kind (a::l)? We start defining a simple predicate stating if a list is 
+empty or not. The predicate is computed by inspection over the list *)
+
+definition is_nil: ∀A:Type[0].list A → Prop ≝
+λA.λl.match l with [ nil ⇒ l = [] | cons hd tl ⇒ (l ≠ [])].
+
+(* Next we need a simple result about negation: if you wish to prove ¬P you are
+authorized to add P to your hypothesis: *)
+
+lemma neg_aux : ∀P:Prop. (P → ¬P) → ¬P.
+#P #PtonegP % /3/ qed. 
+
+theorem diff_cons_nil:
+∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+#A #l #a @neg_aux #Heq 
+(* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux. 
+Next we use the change tactic to pass from the current goal a::l≠ [] to the 
+expression is_nil a::l, convertible with it. *)
+(change with (is_nil ? (a::l))) 
+(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial 
+goal [] = [] *)
+>Heq // qed.
+
+(* As an application of the previous result let us prove that l1@l2 is empty if 
+and only if both l1 and l2 are empty. 
+The idea is to proceed by cases on l1: if l1=[] the statement is trivial; on the 
+other side, if l1 = a::tl, then the hypothesis (a::tl)@l2 = [] is absurd, hence we 
+can prove anything from it. 
+When we know we can prove both A and ¬A, a sensible way to proceed is to apply 
+False_ind: ∀P.False → P to the current goal, that breaks down to prove False, and 
+then absurd: ∀A:Prop. A → ¬A → False to reduce to the contradictory cases. 
+Usually, you may invoke automation to take care to solve the absurd case. *)
+
+lemma nil_to_nil:  ∀A.∀l1,l2:list A.
+  l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 cases l1 normalize /2/ #a #tl #l2 #H @False_ind /2/ qed. 
+
+(* 
+Higher Order Functionals
+
+Let us come to some important, higher order, polymorphic functionals 
+acting over lists. A typical example is the map function, taking a function
+f:A → B, a list l = [a1; a2; ... ; an] and returning the list 
+[f a1; f a2; ... ; f an]. *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ [] | cons x tl ⇒ f x :: (map A B f tl)].
+
+(* Another major example is the fold function, that taken a list 
+l = [a1; a2; ... ;an], a base value b:B, and a function f: A → B → B returns 
+(f a1 (f a2 (... (f an b)...))). *)
+
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+
+(* As an example of application of foldr, let us use it to define a filter 
+function that given a list l: list A and a boolean test p:A → bool returns the 
+sublist of elements satisfying the test. In this case, the result type B of 
+foldr should be (list A), the base value is [], and f: A → list A →list A is 
+the function that taken x and l returns x::l, if x satisfies the test, and l 
+otherwise. We use an if_then_else function included from bool.ma to this purpose. *)
+
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0. if p x then x::l0 else l0) [].
+
+(* Here are a couple of simple lemmas on the behaviour of the filter function. 
+It is often convenient to state such lemmas, in order to be able to use rewriting
+as an alternative to reduction in proofs: reduction is a bit difficult to control.
+*)
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false → 
+  filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+(* As another example, let us redefine the map function using foldr. The
+result type B is (list B), the base value b is [], and the fold function 
+of type A → list B → list B is the function mapping a and l to (f a)::l.
+*)
+
+definition map_again ≝ λA,B,f,l. foldr A (list B) (λa,l.f a::l) [] l.
+
+(* 
+Extensional equality
+
+Can we prove that map_again is "the same" as map? We should first of all
+clarify in which sense we expect the two functions to be equal. Equality in
+Matita has an intentional meaning: it is the smallest predicate induced by 
+convertibility, i.e. syntactical equality up to normalization. From an 
+intentional point of view, map and map_again are not functions, but programs,
+and they are clearly different. What we would like to say is that the two
+programs behave in the same way: this is a different, extensional equality 
+that can be defined in the following way. *)
+
+definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a = g a.
+
+(* Proving that map and map_again are extentionally equal in the 
+previous sense can be proved by a trivial structural induction on the list *)
+
+lemma eq_maps: ∀A,B,f. ExtEq ?? (map A B f) (map_again A B f).
+#A #B #f #n (elim n) normalize // qed. 
+
+(* Let us make another remark about extensional equality. It is clear that,
+if f is extensionally equal to g, then (map A B f) is extensionally equal to
+(map A B g). Let us prove it. *)
+
+theorem eq_map : ∀A,B,f,g. ExtEq A B f g → ExtEq ?? (map A B f) (map A B g).
+#A #B #f #g #eqfg
+ 
+(* the relevant point is that we cannot proceed by rewriting f with g via
+eqfg, here. Rewriting only works with Matita intensional equality, while here
+we are dealing with a different predicate, defined by the user. The right way 
+to proceed is to unfold the definition of ExtEq, and work by induction on l, 
+as usual when we want to prove extensional equality between functions over 
+inductive types; again the rest of the proof is trivial. *)
+
+#l (elim l) normalize // qed.
+
+(*
+Big Operators
+
+Building a library of basic functions, it is important to achieve a 
+good degree of abstraction and generality, in order to be able to reuse
+suitable instances of the same function in different context. This has not
+only the obvious benefit of factorizing code, but especially to avoid 
+repeating proofs of generic properties over and over again.
+A really convenient tool is the following combination of fold and filter,
+that essentially allow you to iterate on every subset of a given enumerated
+(finite) type, represented as a list. *) 
+
+ let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l:B ≝  
+ match l with 
+  [ nil ⇒ b 
+  | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else
+      (fold A B op b p f l)].
+
+(* It is also important to spend a few time to introduce some fancy notation
+for these iterators. *)
+
+ notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
+
+interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
+
+theorem fold_true: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
+  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_false: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+  \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_filter: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
+  \fold[op,nil]_{i ∈ l| p i} (f i) = 
+    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //  
+#a #tl #Hind cases(true_or_false (p a)) #pa 
+  [ >filter_true // > fold_true // >fold_true //
+  | >filter_false // >fold_false // ]
+qed.
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+{op :2> A → A → A; 
+  nill:∀a. op nil a = a; 
+  nilr:∀a. op a nil = a;
+  assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+}.
+
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f:A → B.
+ op (\fold[op,nil]_{i ∈ I} (f i)) (\fold[op,nil]_{i ∈ J} (f i)) = 
+   \fold[op,nil]_{i ∈ (I@J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize 
+  [>nill//|#a #tl #Hind <assoc //]
+qed.
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter4.ma b/matita/matita/lib/tutorial/chapter4.ma
new file mode 100644
index 000000000..30fae3df0
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter4.ma
@@ -0,0 +1,337 @@
+(* 
+Naif Set Theory
+
+*)
+include "basics/types.ma".
+include "basics/bool.ma".
+(* 
+In this Chapter we shall develop a naif theory of sets represented as 
+characteristic predicates over some universe A, that is as objects of type 
+A→Prop. 
+For instance the empty set is defined by the always false function: *)
+
+definition empty_set ≝ λA:Type[0].λa:A.False.
+notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
+interpretation "empty set" 'empty_set = (empty_set ?).
+
+(* Similarly, a singleton set contaning containing an element a, is defined
+by by the characteristic function asserting equality with a *)
+
+definition singleton ≝ λA.λx,a:A.x=a.
+(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
+interpretation "singleton" 'singl x = (singleton ? x).
+
+(* The membership relation between an element of type A and a set S:A →Prop is
+simply the predicate resulting from the application of S to a.
+The operations of union, intersection, complement and substraction 
+are easily defined in terms of the propositional connectives of dijunction,
+conjunction and negation *)
+
+definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
+
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
+
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
+(* Finally, we use implication to define the inclusion relation between
+sets *)
+
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
+interpretation "subset" 'subseteq a b = (subset ? a b).
+
+(* 
+Set Equality
+
+Two sets are equals if and only if they have the same elements, that is,
+if the two characteristic functions are extensionally equivalent: *) 
+
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
+notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+
+(*
+This notion of equality is different from the intensional equality of
+functions; the fact it defines an equivalence relation must be explicitly 
+proved: *)
+
+lemma eqP_sym: ∀U.∀A,B:U →Prop. 
+  A =1 B → B =1 A.
+#U #A #B #eqAB #a @iff_sym @eqAB qed.
+ 
+lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
+  A =1 B → B =1 C → A =1 C.
+#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+
+(* For the same reason, we must also prove that all the operations behave well
+with respect to eqP: *)
+
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
+  A =1 C  → A ∪ B =1 C ∪ B.
+#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
+  
+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
+  B =1 C  → A ∪ B =1 A ∪ C.
+#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+  
+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
+  A =1 C  → A ∩ B =1 C ∩ B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+  
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
+  B =1 C  → A ∩ B =1 A ∩ C.
+#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
+  A =1 C  → A - B =1 C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+  
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
+  B =1 C  → A - B =1 A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
+(* 
+Simple properties of sets
+
+We can now prove several properties of the previous set-theoretic operations. 
+In particular, union is commutative and associative, and the empty set is an 
+identity element: *)
+
+lemma union_empty_r: ∀U.∀A:U→Prop. 
+  A ∪ ∅ =1 A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+qed.
+
+lemma union_comm : ∀U.∀A,B:U →Prop. 
+  A ∪ B =1 B ∪ A.
+#U #A #B #a % * /2/ qed. 
+
+lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
+  A ∪ B ∪ C =1 A ∪ (B ∪ C).
+#S #A #B #C #w % [* [* /3/ | /3/ ] | * [/3/ | * /3/]
+qed.   
+
+(* In the same way we prove commutativity and associativity for set 
+interesection *)
+
+lemma cap_comm : ∀U.∀A,B:U →Prop. 
+  A ∩ B =1 B ∩ A.
+#U #A #B #a % * /2/ qed. 
+
+lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
+  A ∩ (B ∩ C) =1 (A ∩ B) ∩ C.
+#U #A #B #C #w % [ * #Aw * /3/ | * * /3/ ]
+qed.
+
+(* We can also easily prove idempotency for union and intersection *)
+
+lemma union_idemp: ∀U.∀A:U →Prop. 
+  A  ∪ A =1 A.
+#U #A #a % [* // | /2/] qed. 
+
+lemma cap_idemp: ∀U.∀A:U →Prop. 
+  A ∩ A =1 A.
+#U #A #a % [* // | /2/] qed. 
+
+(* We conclude our examples with a couple of distributivity theorems, and a 
+characterization of substraction in terms of interesection and complementation. *)
+
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+  
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) - C =1 (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+
+lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+#U #A #B #w normalize /2/
+qed.
+
+(* 
+Bool vs. Prop
+
+In several situation it is important to assume to have a decidable equality 
+between elements of a set U, namely a boolean function eqb: U→U→bool such that
+for any pair of elements a and b in U, (eqb x y) is true if and only if x=y. 
+A set equipped with such an equality is called a DeqSet: *)
+
+record DeqSet : Type[1] ≝ { carr :> Type[0];
+   eqb: carr → carr → bool;
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+}.
+
+(* We use the notation == to denote the decidable equality, to distinguish it
+from the propositional equality. In particular, a term of the form a==b is a 
+boolean, while a=b is a proposition. *)
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+(* 
+Small Scale Reflection
+
+It is convenient to have a simple way to reflect a proof of the fact 
+that (eqb a b) is true into a proof of the proposition (a = b); to this aim, 
+we introduce two operators "\P" and "\b". *)
+
+notation "\P H" non associative with precedence 90 
+  for @{(proj1 … (eqb_true ???) $H)}. 
+
+notation "\b H" non associative with precedence 90 
+  for @{(proj2 … (eqb_true ???) $H)}. 
+  
+(* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
+\b h: eqb a b = true. Let us see an example of their use: the following 
+statement asserts that we can reflect a proof that eqb a b is false into
+a proof of the proposition a ≠ b. *)
+
+lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
+  (eqb ? a b) = false ↔ a ≠ b.
+
+(* We start the proof introducing the hypothesis, and then split the "if" and
+"only if" cases *)
+ 
+#S #a #b % #H 
+
+(* The latter is easily reduced to prove the goal true=false under the assumption
+H1: a = b *)
+  [@(not_to_not … not_eq_true_false) #H1 
+  
+(* since by assumption H false is equal to (a==b), by rewriting we obtain the goal 
+true=(a==b) that is just the boolean version of H1 *) 
+
+  <H @sym_eq @(\b H1)
+
+(* In the "if" case, we proceed by cases over the boolean equality (a==b); if 
+(a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
+true, then by reflection a=b, while by hypothesis a≠b *)
+  
+ |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
+  ]
+qed.
+ 
+(* We also introduce two operators "\Pf" and "\bf" to reflect a proof
+of (a==b)=false into a proof of a≠b, and vice-versa *) 
+
+notation "\Pf H" non associative with precedence 90 
+  for @{(proj1 … (eqb_false ???) $H)}. 
+
+notation "\bf H" non associative with precedence 90 
+  for @{(proj2 … (eqb_false ???) $H)}. 
+
+(* The following statement proves that propositional equality in a 
+DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
+
+ lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
+#S #a #b cases (true_or_false (eqb ? a b)) #H
+  [%1 @(\P H) | %2 @(\Pf H)]
+qed.
+
+(* 
+Unification Hints
+
+A simple example of a set with a decidable equality is bool. We first define 
+the boolean equality beqb, that is just the xand function, then prove that 
+beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by 
+instantiating the DeqSet record with the previous information *)
+
+definition beqb ≝ λb1,b2.
+  match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
+
+lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
+#b1 #b2 cases b1 cases b2 normalize /2/
+qed. 
+
+definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+
+(* At this point, we would expect to be able to prove things like the
+following: for any boolean b, if b==false is true then b=false. 
+Unfortunately, this would not work, unless we declare b of type 
+DeqBool (change the type in the following statement and see what 
+happens). *)
+
+example exhint: ∀b:DeqBool. (b==false) = true → b=false.
+#b #H @(\P H) 
+qed.
+
+(* The point is that == expects in input a pair of objects whose type must be the 
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference 
+system has no knowledge of it (it is an information that has been supplied by the 
+user, and stored somewhere in the library). More explicitly, the type inference 
+inference system, would face an unification problem consisting to unify bool 
+against the carrier of something (a metavaribale) and it has no way to synthetize 
+the answer. To solve this kind of situations, matita provides a mechanism to hint 
+the system the expected solution. A unification hint is a kind of rule, whose rhd 
+is the unification problem, containing some metavariables X1, ..., Xn, and whose 
+left hand side is the solution suggested to the system, in the form of equations 
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.
+To make an example, in the previous case, the unification problem is bool = carr X,
+and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since 
+bool is convertible with (carr (mk_DeqSet bool beb true)). *)
+
+unification hint  0 ≔ ; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    bool ≡ carr X.
+    
+unification hint  0 ≔ b1,b2:bool; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    beqb b1 b2 ≡ eqb X b1 b2.
+    
+(* After having provided the previous hints, we may rewrite example exhint 
+declaring b of type bool. *)
+ 
+example exhint1: ∀b:bool. (b == false) = true → b = false. 
+#b #H @(\P H)
+qed.
+
+(* The cartesian product of two DeqSets is still a DeqSet. To prove
+this, we must as usual define the boolen equality function, and prove
+it correctly reflects propositional equality. *)
+
+definition eq_pairs ≝
+  λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+  eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+  [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+  ]
+qed.
+
+definition DeqProd ≝ λA,B:DeqSet.
+  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+
+(* Having an unification problem of the kind T1×T2 = carr X, what kind 
+of hint can we give to the system? We expect T1 to be the carrier of a
+DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
+This is expressed by the following hint: *)
+
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ carr C1,
+    T2 ≟ carr C2,
+    X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1×T2 ≡ carr X.
+
+unification hint  0 ≔ T1,T2,p1,p2; 
+    X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢ 
+    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2. 
+  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H).
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma
new file mode 100644
index 000000000..9cd43fd23
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter5.ma
@@ -0,0 +1,253 @@
+(* 
+Effective searching
+
+The fact of being able to decide, via a computable boolean function, the 
+equality between elements of a given set is an essential prerequisite for 
+effectively searching an element of that set inside a data structure. In this 
+section we shall define several boolean functions acting on lists of elements in 
+a DeqSet, and prove some of their properties.*)
+
+include "basics/list.ma". 
+include "tutorial/chapter4.ma".
+
+(* The first function we define is an effective version of the membership relation,
+between an element x and a list l. Its definition is a straightforward recursion on
+l.*)
+
+let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
+  match l with
+  [ nil ⇒ false
+  | cons a tl ⇒ (x == a) ∨ memb S x tl
+  ].
+
+notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
+interpretation "boolean membership" 'memb a l = (memb ? a l).
+
+(* We can now prove several interesing properties for memb:
+- memb_hd: x is a member of x::l
+- memb_cons: if x is a member of l than x is a member of a::l
+- memb_single: if x is a member of [a] then x=a
+- memb_append: if x is a member of l1@l2 then either x is a member of l1
+  or x is a member of l2
+- memb_append_l1: if x is a member of l1 then x is a member of l1@l2
+- memb_append_l2: if x is a member of l2 then x is a member of l1@l2
+- memb_exists: if x is a member of l, than l can decomposed as l1@(x::l2)
+- not_memb_to_not_eq: if x is not a member of l and y is, then x≠y
+- memb_map: if a is a member of l, then (f a) is a member of (map f l)
+- memb_compose: if a is a member of l1 and b is a meber of l2 than
+  (op a b) is a member of (compose op l1 l2)
+*)
+
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
+qed.
+
+lemma memb_cons: ∀S,a,b,l. 
+  memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize // 
+qed.
+
+lemma memb_single: ∀S,a,x. memb S a (x::[]) = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+  [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
+qed.
+
+lemma memb_append: ∀S,a,l1,l2. 
+memb S a (l1@l2) = true → memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //] 
+#b #tl #Hind #l2 cases (a==b) normalize /2/ 
+qed. 
+
+lemma memb_append_l1: ∀S,a,l1,l2. 
+ memb S a l1= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize
+  [normalize #le #abs @False_ind /2/
+  |#b #tl #Hind #l2 cases (a==b) normalize /2/ 
+  ]
+qed. 
+
+lemma memb_append_l2: ∀S,a,l1,l2. 
+ memb S a l2= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize //
+#b #tl #Hind #l2 cases (a==b) normalize /2/ 
+qed. 
+
+lemma memb_exists: ∀S,a,l.memb S a l = true → ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /2/]
+#b #tl #Hind #H cases (orb_true_l … H)
+  [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
+  |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+   @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+  ]
+qed.
+
+lemma not_memb_to_not_eq: ∀S,a,b,l. 
+ memb S a l = false → memb S b l = true → a==b = false.
+#S #a #b #l cases (true_or_false (a==b)) // 
+#eqab >(\P eqab) #H >H #abs @False_ind /2/
+qed. 
+ 
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → 
+  memb S2 (f a) (map … f l) = true.
+#S1 #S2 #f #a #l elim l normalize [//]
+#x #tl #memba cases (true_or_false (a==x))
+  [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
+  |#eqx >eqx cases (f a==f x) normalize /2/
+  ]
+qed.
+
+lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
+  memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+  memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
+#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
+  [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // 
+  |#membtl @memb_append_l2 @Hind //
+  ]
+qed.
+
+(* 
+Unicity
+
+If we are interested in representing finite sets as lists, is is convenient
+to avoid duplications of elements. The following uniqueb check this property. 
+*)
+
+let rec uniqueb (S:DeqSet) l on l : bool ≝
+  match l with 
+  [ nil ⇒ true
+  | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+  ].
+
+(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
+
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
+  match l1 with
+  [ nil ⇒ l2
+  | cons a tl ⇒ 
+     let r ≝ unique_append S tl l2 in
+     if memb S a r then r else a::r
+  ].
+
+lemma memb_unique_append: ∀S,a,l1,l2. 
+  memb S a (unique_append S l1 l2) = true → memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //] 
+#b #tl #Hind #l2 cases (true_or_false … (a==b)) #Hab >Hab normalize /2/
+cases (memb S b (unique_append S tl l2)) normalize 
+  [@Hind | >Hab normalize @Hind]   
+qed. 
+
+lemma unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. 
+  (∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
+    ∀x. memb S x (unique_append S l1 l2) = true → P x. 
+#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/ 
+qed.
+
+lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+  uniqueb S (unique_append S l1 l2) = true.
+#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
+cases (true_or_false … (memb S a (unique_append S tl l2))) 
+#H >H normalize [@Hind //] >H normalize @Hind //
+qed.
+
+(*
+Sublists
+
+*)
+definition sublist ≝ 
+  λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+lemma sublist_length: ∀S,l1,l2. 
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
+#S #l1 elim l1 // 
+#a #tl #Hind #l2 #unique #sub
+cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize 
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
+>eql2 in sub; #sub #x #membx 
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+  [#membxl3 @memb_append_l1 //
+  |#membxal4 cases (orb_true_l … membxal4)
+    [#eqxa @False_ind lapply (andb_true_l … unique)
+     <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
+    ]
+  ]
+qed.
+
+lemma sublist_unique_append_l1: 
+  ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
+#x #tl #Hind #l2 #a 
+normalize cases (true_or_false … (a==x)) #eqax >eqax 
+[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
+  [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize 
+  [/2/ |>eqax normalize /2/]
+]
+qed.
+
+lemma sublist_unique_append_l2: 
+  ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+#S #l1 elim l1 [normalize //] #x #tl #Hind normalize 
+#l2 #a cases (memb S x (unique_append S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
+qed.
+
+lemma decidable_sublist:∀S,l1,l2. 
+  (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
+#S #l1 #l2 elim l1 
+  [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
+  |#a #tl * #subtl 
+    [cases (true_or_false (memb S a l2)) #memba
+      [%1 whd #x #membx cases (orb_true_l … membx)
+        [#eqax >(\P eqax) // |@subtl]
+      |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
+      ]
+    |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons //
+    ] 
+  ]
+qed.
+
+(*
+Filtering
+*)
+
+lemma memb_filter_true: ∀S,f,a,l. 
+  memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /2/]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+cases (true_or_false (a==b)) #eqab
+  [#_ >(\P eqab) // | >eqab normalize @Hind]
+qed. 
+  
+lemma memb_filter_memb: ∀S,f,a,l. 
+  memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize 
+cases (a==b) normalize // @Hind
+qed.
+  
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → 
+memb S x l = true ∧ (f x = true).
+/3/ qed.
+
+lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
+#S #f #x #l #fx elim l normalize //
+#b #tl #Hind cases (true_or_false (x==b)) #eqxb
+  [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
+  |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
+  ]
+qed. 
+
+(*
+Exists
+
+*)
+
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
+match l with
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
+].
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
new file mode 100644
index 000000000..150b07b76
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -0,0 +1,193 @@
+(*
+Formal Languages
+
+In this chapter we shall apply our notion of DeqSet, and the list operations 
+defined in Chapter 4 to formal languages. A formal language is an arbitrary set
+of words over a given alphabet, that we shall represent as a predicate over words. 
+*)
+include "tutorial/chapter5.ma".
+
+(* A word (or string) over an alphabet S is just a list of elements of S.*)
+definition word ≝ λS:DeqSet.list S.
+
+(* For any alphabet there is only one word of length 0, the empty word, which is 
+denoted by ϵ .*) 
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (nil ?).
+
+(* The operation that consists in appending two words to form a new word, whose 
+length is the sum of the lengths of the original words is called concatenation.
+String concatenation is just the append operation over lists, hence there is no
+point to define it. Similarly, many of its properties, such as the fact that 
+concatenating a word with the empty word gives the original word, follow by 
+general results over lists.
+*)
+
+(*
+Operations over languages
+
+Languages inherit all the basic operations for sets, namely union, intersection, 
+complementation, substraction, and so on. In addition, we may define some new 
+operations induced by string concatenation, and in particular the concatenation 
+A · B of two languages A and B, the so called Kleene's star A* of A and the 
+derivative of a language A w.r.t. a given character a. *)
+
+definition cat : ∀S,l1,l2,w.Prop ≝ 
+  λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+
+notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+interpretation "cat lang" 'middot a b = (cat ? a b).
+
+
+(* Given a language l, the Kleene's star of l, denoted by l*, is the set of 
+finite-length strings that can be generated by concatenating arbitrary strings of 
+l. In other words, w belongs to l* is and only if there exists a list of strings 
+w1,w2,...wk all belonging to l, such that l = w1w2...wk. 
+We need to define the latter operations. The following flatten function takes in 
+input a list of words and concatenates them together. *)
+
+let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+(* Given a list of words l and a language r, (conjunct l r) is true if and only if
+all words in l are in r, that is for every w in l, r w holds. *)
+
+let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
+match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
+
+(* We are ready to give the formal definition of the Kleene's star of l:
+a word w belongs to l* is and only if there exists a list of strings 
+lw such that (conjunct lw l) and  l = flatten lw. *)
+
+definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
+
+(* The derivative of a language A with respect to a character a is the set of
+all strings w such that aw is in A. *)
+
+definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+
+(* 
+Language equalities
+
+Equality between languages is just the usual extensional equality between
+sets. The operation of concatenation behaves well with respect to this equality. *)
+
+lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. 
+  A =1 C  → A · B =1 C · B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /6/
+qed.
+
+lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. 
+  B =1 C → A · B =1 A · C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /6/ 
+qed.
+  
+(* Concatenating a language with the empty language results in the
+empty language. *) 
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
+(* Concatenating a language l with the singleton language containing the
+empty string, results in the language l; that is {ϵ} is a left and right 
+unit with respect to concatenation. *)
+
+lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
+  A · {ϵ} =1  A. 
+#S #A #w %
+  [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+  |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
+  ]
+qed.
+
+lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
+  {ϵ} · A =1  A. 
+#S #A #w %
+  [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+  |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
+  ]
+  qed.
+
+(* Concatenation is distributive w.r.t. union. *)
+
+lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
+  (A ∪ B) · C =1  A · C ∪ B · C. 
+#S #A #B #C #w %
+  [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] 
+qed.
+
+lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
+  (A ∪ {ϵ}) · C =1  A · C ∪ C. 
+  #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+qed.
+
+(* The following is a major property of derivatives *)
+
+lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → deriv S (A·B) a =1 (deriv S A a) · B.
+#S #A #B #a #noteps #w normalize %
+  [* #w1 cases w1 
+    [* #w2 * * #_ #Aeps @False_ind /2/
+    |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
+     #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
+    ]
+  |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
+   @(ex_intro … w2) % // % normalize //
+  ]
+qed. 
+
+(* 
+Main Properties of Kleene's star
+
+We conclude this section with some important properties of Kleene's
+star that will be used in the following chapters. *)
+
+lemma espilon_in_star: ∀S.∀A:word S → Prop.
+  A^* ϵ.
+#S #A @(ex_intro … [ ]) normalize /2/
+qed.
+
+lemma cat_to_star:∀S.∀A:word S → Prop.
+  ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
+% normalize /2/
+qed.
+
+lemma fix_star: ∀S.∀A:word S → Prop. 
+  A^* =1 A · A^* ∪ {ϵ}.
+#S #A #w %
+  [* #l generalize in match w; -w cases l [normalize #w * /2/]
+   #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
+   #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
+   % /2/ whd @(ex_intro … tl) /2/
+  |* [2: whd in ⊢ (%→?); #eqw <eqw //]
+   * #w1 * #w2 * * #eqw <eqw @cat_to_star 
+  ]
+qed.
+
+lemma star_fix_eps : ∀S.∀A:word S → Prop.
+  A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.  
+#S #A #w %
+  [* #l elim l 
+    [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw // 
+    |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
+       |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1 
+        @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
+         [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
+       ]
+    ]
+  |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+     | whd in ⊢ (%→?); #H <H //
+     ]
+  ]
+qed. 
+     
+lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
+  A^* ∪ {ϵ} =1 A^*.
+#S #A #w % /2/ * // 
+qed.
+  
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter7.ma b/matita/matita/lib/tutorial/chapter7.ma
new file mode 100644
index 000000000..4b12b75fc
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter7.ma
@@ -0,0 +1,308 @@
+(* 
+Regular Expressions
+
+We shall apply all the previous machinery to the study of regular languages 
+and the constructions of the associated finite automata. *)
+
+include "tutorial/chapter6.ma".
+
+(* The type re of regular expressions over an alphabet $S$ is the smallest 
+collection of objects generated by the following constructors: *)
+
+inductive re (S: DeqSet) : Type[0] ≝
+   z: re S                (* empty: ∅ *)
+ | e: re S                (* epsilon: ϵ *)
+ | s: S → re S            (* symbol: a *)
+ | c: re S → re S → re S  (* concatenation: e1 · e2 *)
+ | o: re S → re S → re S  (* plus: e1 + e2 *)
+ | k: re S → re S.        (* kleene's star: e* *)
+
+interpretation "re epsilon" 'epsilon = (e ?).
+interpretation "re or" 'plus a b = (o ? a b).
+interpretation "re cat" 'middot a b = (c ? a b).
+interpretation "re star" 'star a = (k ? a).
+
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
+
+notation "`∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+(* The language sem{e} associated with the regular expression e is inductively 
+defined by the following function: *)
+
+let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝ 
+match r with
+[ z ⇒ ∅
+| e ⇒ {ϵ}
+| s x ⇒ { (x::[]) }
+| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
+| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
+| k r1 ⇒ (in_l ? r1) ^*].
+
+notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
+interpretation "in_l" 'in_l E = (in_l ? E).
+interpretation "in_l mem" 'mem w l = (in_l ? l w).
+
+lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
+// qed.
+
+
+(* 
+Pointed Regular expressions
+
+We now introduce pointed regular expressions, that are the main tool we shall 
+use for the construction of the automaton. 
+A pointed regular expression is just a regular expression internally labelled 
+with some additional points. Intuitively, points mark the positions inside the 
+regular expression which have been reached after reading some prefix of
+the input string, or better the positions where the processing of the remaining 
+string has to be started. Each pointed expression for $e$ represents a state of 
+the {\em deterministic} automaton associated with $e$; since we obviously have 
+only a finite number of possible labellings, the number of states of the automaton 
+is finite.
+
+Pointed regular expressions provide the tool for an algebraic revisitation of 
+McNaughton and Yamada's algorithm for position automata, making the proof of its 
+correctness, that is far from trivial, particularly clear and simple. In particular, 
+pointed expressions offer an appealing alternative to Brzozowski's derivatives, 
+avoiding their weakest point, namely the fact of being forced to quotient derivatives 
+w.r.t. a suitable notion of equivalence in order to get a finite number of states 
+(that is not essential for recognizing strings, but is crucial for comparing regular 
+expressions). 
+
+Our main data structure is the notion of pointed item, that is meant whose purpose
+is to encode a set of positions inside a regular expression. 
+The idea of formalizing pointers inside a data type by means of a labelled version 
+of the data type itself is probably one of the first, major lessons learned in the 
+formalization of the metatheory of programming languages. For our purposes, it is 
+enough to mark positions preceding individual characters, so we shall have two kinds 
+of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
+
+inductive pitem (S: DeqSet) : Type[0] ≝
+   pz: pitem S                       (* empty *)
+ | pe: pitem S                       (* epsilon *)
+ | ps: S → pitem S                   (* symbol *)
+ | pp: S → pitem S                   (* pointed sysmbol *)
+ | pc: pitem S → pitem S → pitem S   (* concatenation *)
+ | po: pitem S → pitem S → pitem S   (* plus *)
+ | pk: pitem S → pitem S.            (* kleene's star *)
+ 
+(* A pointed regular expression (pre) is just a pointed item with an additional 
+boolean, that must be understood as the possibility to have a trailing point at 
+the end of the expression. As we shall see, pointed regular expressions can be 
+understood as states of a DFA, and the boolean indicates if
+the state is final or not. *)
+
+definition pre ≝ λS.pitem S × bool.
+
+interpretation "pitem star" 'star a = (pk ? a).
+interpretation "pitem or" 'plus a b = (po ? a b).
+interpretation "pitem cat" 'middot a b = (pc ? a b).
+notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "pitem pp" 'pp a = (pp ? a).
+interpretation "pitem ps" 'ps a = (ps ? a).
+interpretation "pitem epsilon" 'epsilon = (pe ?).
+interpretation "pitem empty" 'empty = (pz ?).
+
+(* The carrier $|i|$ of an item i is the regular expression obtained from i by 
+removing all the points. Similarly, the carrier of a pointed regular expression 
+is the carrier of its item. *)
+
+let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
+ match l with
+  [ pz ⇒ z ? (* `∅ *)
+  | pe ⇒ ϵ
+  | ps x ⇒ `x
+  | pp x ⇒ `x
+  | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
+  | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
+  | pk E ⇒ (forget ? E)^* ].
+ 
+(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
+interpretation "forget" 'norm a = (forget ? a).
+
+lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
+// qed.
+
+lemma erase_plus : ∀S.∀i1,i2:pitem S.
+  |i1 + i2| = |i1| + |i2|.
+// qed.
+
+lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. 
+// qed.
+
+(* 
+Comparing items and pres
+
+Items and pres are very concrete datatypes: they can be effectively compared, 
+and enumerated. In particular, we can define a boolean equality beqitem and a proof
+beqitem_true that it refects propositional equality, enriching the set (pitem S)
+to a DeqSet. *)
+
+let rec beqitem S (i1,i2: pitem S) on i1 ≝ 
+  match i1 with
+  [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
+  | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
+  | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
+  | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
+  | po i11 i12 ⇒ match i2 with 
+    [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+    | _ ⇒ false]
+  | pc i11 i12 ⇒ match i2 with 
+    [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+    | _ ⇒ false]
+  | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
+  ].
+
+lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). 
+#S #i1 elim i1
+  [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+  |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+  |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+    [>(\P H) // | @(\b (refl …))]
+  |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+    [>(\P H) // | @(\b (refl …))]
+  |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+   normalize #H destruct 
+    [cases (true_or_false (beqitem S i11 i21)) #H1
+      [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+      |>H1 in H; normalize #abs @False_ind /2/
+      ]
+    |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+    ]
+  |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+   normalize #H destruct 
+    [cases (true_or_false (beqitem S i11 i21)) #H1
+      [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+      |>H1 in H; normalize #abs @False_ind /2/
+      ]
+    |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+    ]
+  |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
+   normalize #H destruct 
+    [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
+  ]
+qed. 
+
+definition DeqItem ≝ λS.
+  mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+
+(* We also add a couple of unification hints to allow the type inference system 
+to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the 
+equality function of a DeqSet. *)
+
+unification hint  0 ≔ S; 
+    X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢ 
+    pitem S ≡ carr X.
+    
+unification hint  0 ≔ S,i1,i2; 
+    X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢ 
+    beqitem S i1 i2 ≡ eqb X i1 i2.
+
+(* 
+Semantics of pointed regular expressions
+
+The intuitive semantic of a point is to mark the position where
+we should start reading the regular expression. The language associated
+to a pre is the union of the languages associated with its points. *)
+
+let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ 
+match r with
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
+| pp x ⇒ { (x::[]) }
+| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
+| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
+| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^*  ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition in_prl ≝ λS : DeqSet.λp:pre S. 
+  if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
+  
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_l E = (in_prl ? E).
+
+(* The following, trivial lemmas are only meant for rewriting purposes. *)
+
+lemma sem_pre_true : ∀S.∀i:pitem S. 
+  \sem{〈i,true〉} = \sem{i} ∪ {ϵ}. 
+// qed.
+
+lemma sem_pre_false : ∀S.∀i:pitem S. 
+  \sem{〈i,false〉} = \sem{i}. 
+// qed.
+
+lemma sem_cat: ∀S.∀i1,i2:pitem S. 
+  \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+// qed.
+
+lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
+  \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_plus: ∀S.∀i1,i2:pitem S. 
+  \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+// qed.
+
+lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w. 
+  \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_star : ∀S.∀i:pitem S.
+  \sem{i^*} = \sem{i} · \sem{|i|}^*.
+// qed.
+
+lemma sem_star_w : ∀S.∀i:pitem S.∀w.
+  \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
+// qed.
+
+(* Below are a few, simple, semantic properties of items. In particular:
+- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
+- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+The first property is proved by a simple induction on $i$; the other
+results are easy corollaries. We need an auxiliary lemma first. *)
+
+lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
+#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
+
+lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
+#S #e elim e normalize /2/  
+  [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H 
+   >(append_eq_nil …H…) /2/
+  |#r1 #r2 #n1 #n2 % * /2/
+  |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
+  ]
+qed.
+
+lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
+#S * #i #b cases b // normalize #H @False_ind /2/ 
+qed.
+
+lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
+#S * #i #b #btrue normalize in btrue; >btrue %2 // 
+qed.
+
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+#S #i #w % 
+  [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
+  |* //
+  ]
+qed.
+
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+#S * #i * 
+  [>sem_pre_true normalize in ⊢ (??%?); #w % 
+    [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
+  |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
+  ]
+qed.
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma
new file mode 100644
index 000000000..0d6a8a431
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter8.ma
@@ -0,0 +1,377 @@
+(*
+Broadcasting points
+
+Intuitively, a regular expression e must be understood as a pointed expression with a single 
+point in front of it. Since however we only allow points before symbols, we must broadcast 
+this initial point inside e traversing all nullable subexpressions, that essentially corresponds 
+to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
+its definition is the expected one: let us start discussing an example.
+
+Example
+Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the 
+first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence 
+reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in 
+parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the 
+star, and to traverse it, stopping in front of a; the second point just stops in front of b. 
+No point reached that end of b^*a + b hence no further propagation is possible. In conclusion: 
+               •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
+*)
+
+include "tutorial/chapter7.ma".
+
+(* Broadcasting a point inside an item generates a pre, since the point could possibly reach 
+the end of the expression. 
+Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
+If we define
+                 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
+then, we just have •(i1+i2) = •(i1)⊕ •(i2).
+*)
+
+definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+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:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
+// qed.
+
+(*
+Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2 
+we should start broadcasting it inside i1 and then proceed into i2 if and only if a 
+point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where 
+e ▹ i is a general operation of concatenation between a pre and an item, defined by 
+cases on the boolean in e: 
+
+       〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
+       〈i1,false〉 ▹ i2 = i1 · i2
+In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
+        i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
+Let us come to the formalized definitions:
+*)
+
+definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
+  match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
+ 
+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:word S → Prop. 
+  A = B → A =1 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: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/ 
+qed.
+ 
+(* 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.
+  match e1 with 
+  [ mk_Prod i1 b1 ⇒ match b1 with 
+    [ true ⇒ (i1 ◃ (bcast ? i2)) 
+    | false ⇒ 〈i1 · i2,false〉
+    ]
+  ].
+
+notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
+
+(* We are ready to give the formal definition of the broadcasting operation. *)
+
+notation "•" non associative with precedence 60 for @{eclose ?}.
+
+let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
+ match i with
+  [ pz ⇒ 〈 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〉].
+  
+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: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.
+// qed.
+
+lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
+  •(i1 · i2) = •i1 ▹ i2.
+// qed.
+
+lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
+  •i^* = 〈(\fst(•i))^*,true〉.
+// qed.
+
+(* The definition of •(-) (eclose) can then be lifted from items to pres
+in the obvious way. *)
+
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. 
+  match e with 
+  [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+  
+definition preclose ≝ λS. lift S (eclose 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:pitem S. |\fst (•i)| = |i|.
+#S #i elim i // 
+  [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
+    cases (•i1) #i11 #b1 cases b1 // <IH2 >pcl_true_bis //
+  | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
+    cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //  
+  | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+  ]
+qed.
+
+(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
+
+sem_oplus:     \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2} 
+sem_pcl:       \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet     \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+
+The proof of sem_oplus is straightforward. *)
+
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+  \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. 
+#S * #i1 #b1 * #i2 #b2 #w %
+  [cases b1 cases b2 normalize /2/ * /3/ * /3/
+  |cases b1 cases b2 normalize /2/ * /3/ * /3/
+  ]
+qed.
+
+(* For the others, we proceed as follow: we first prove the following 
+auxiliary lemma, that assumes sem_bullet:
+
+sem_pcl_aux: 
+   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+
+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:pitem S.
+  \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. 
+// qed.
+
+lemma sem_pcl_aux : ∀S.∀e1:pre S.∀i2:pitem S.
+   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+#S * #i1 #b1 #i2 cases b1
+  [2:#th >pcl_false >sem_pre_false >sem_pre_false >sem_cat /2/
+  |#H >pcl_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
+   >erase_bull @eqP_trans [|@(eqP_union_l … H)]
+    @eqP_trans [|@eqP_union_l[|@union_comm ]]
+    @eqP_trans [|@eqP_sym @union_assoc ] /3/ 
+  ]
+qed.
+  
+lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. 
+ \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
+#S #e #i #A #seme
+@eqP_trans [|@minus_eps_pre]
+@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
+@eqP_trans [||@distribute_substract] 
+@eqP_substract_r //
+qed.
+
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+#S #e elim e 
+  [#w normalize % [/2/ | * //]
+  |/2/ 
+  |#x normalize #w % [ /2/ | * [@False_ind | //]]
+  |#x normalize #w % [ /2/ | * // ] 
+  |#i1 #i2 #IH1 #IH2 >eclose_dot
+   @eqP_trans [|@sem_pcl_aux //] >sem_cat 
+   @eqP_trans
+     [|@eqP_union_r
+       [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+   @eqP_trans [|@union_assoc]
+   @eqP_trans [||@eqP_sym @union_assoc]
+   @eqP_union_l //
+  |#i1 #i2 #IH1 #IH2 >eclose_plus
+   @eqP_trans [|@sem_oplus] >sem_plus >erase_plus 
+   @eqP_trans [|@(eqP_union_l … IH2)]
+   @eqP_trans [|@eqP_sym @union_assoc]
+   @eqP_trans [||@union_assoc] @eqP_union_r
+   @eqP_trans [||@eqP_sym @union_assoc]
+   @eqP_trans [||@eqP_union_l [|@union_comm]]
+   @eqP_trans [||@union_assoc] /2/
+  |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
+   @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
+   @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+   @eqP_trans [|@union_assoc] @eqP_union_l >erase_star 
+   @eqP_sym @star_fix_eps 
+  ]
+qed.
+
+(*
+Blank item
+ 
+
+As a corollary of theorem sem_bullet, given a regular expression e, we can easily 
+find an item with the same semantics of $e$: it is enough to get an item (blank e) 
+having e as carrier and no point, and then broadcast a point in it. The semantics of
+(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: DeqSet) (i: re S) on i :pitem S ≝
+ match i with
+  [ z ⇒ pz ?
+  | e ⇒ ϵ
+  | s y ⇒ `y
+  | o e1 e2 ⇒ (blank S e1) + (blank S e2) 
+  | c e1 e2 ⇒ (blank S e1) · (blank S e2)
+  | k e ⇒ (blank S e)^* ].
+  
+lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
+#S #e elim e normalize //
+qed.
+
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+#S #e elim e 
+  [1,2:@eq_to_ex_eq // 
+  |#s @eq_to_ex_eq //
+  |#e1 #e2 #Hind1 #Hind2 >sem_cat 
+   @eqP_trans [||@(union_empty_r … ∅)] 
+   @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
+   @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
+  |#e1 #e2 #Hind1 #Hind2 >sem_plus 
+   @eqP_trans [||@(union_empty_r … ∅)] 
+   @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
+  |#e #Hind >sem_star
+   @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
+  ]
+qed.
+   
+theorem re_embedding: ∀S.∀e:re S. 
+  \sem{•(blank S e)} =1 \sem{e}.
+#S #e @eqP_trans [|@sem_bull] >forget_blank 
+@eqP_trans [|@eqP_union_r [|@sem_blank]]
+@eqP_trans [|@union_comm] @union_empty_r.
+qed.
+
+(*
+Lifted Operators
+ 
+
+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:DeqSet.λe:pre S. 
+  lift S (pre_concat_l S eclose 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:pitem S.∀b. 
+  〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
+#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) // 
+qed.
+
+lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
+  〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
+// 
+qed.
+  
+lemma erase_odot:∀S.∀e1,e2:pre S.
+  |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
+#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //  
+qed.
+
+(* Let us come to the star operation: *)
+
+definition lk ≝ λS:DeqSet.λe:pre S.
+  match e with 
+  [ mk_Prod i1 b1 ⇒
+    match b1 with 
+    [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
+    |false ⇒ 〈i1^*,false〉
+    ]
+  ]. 
+
+(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
+interpretation "lk" 'lk a = (lk ? a).
+notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
+
+lemma ostar_true: ∀S.∀i:pitem S.
+  〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
+// qed.
+
+lemma ostar_false: ∀S.∀i:pitem S.
+  〈i,false〉^⊛ = 〈i^*, false〉.
+// qed.
+  
+lemma erase_ostar: ∀S.∀e:pre S.
+  |\fst (e^⊛)| = |\fst e|^*.
+#S * #i * // qed.
+
+lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. 
+  \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+#S #e1 #i 
+cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
+#H >H cases (e1 ▹ i) #i1 #b1 cases b1 
+  [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
+   @eqP_union_l /2/ 
+  |/2/
+  ]
+qed.
+
+lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i. 
+  e1 ⊙ 〈i,false〉 = e1 ▹ i.
+#S #e1 #i  
+cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
+cases (e1 ▹ 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: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+#S #e1 * #i2 * 
+  [>sem_pre_true 
+   @eqP_trans [|@sem_odot_true]
+   @eqP_trans [||@union_assoc] @eqP_union_r @sem_pcl_aux //
+  |>sem_pre_false >eq_odot_false @sem_pcl_aux //
+  ]
+qed.
+
+theorem sem_ostar: ∀S.∀e:pre S. 
+  \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
+#S * #i #b cases b
+  [>sem_pre_true >sem_pre_true >sem_star >erase_bull
+   @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
+   @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+   @eqP_trans [||@eqP_sym @distr_cat_r]
+   @eqP_trans [|@union_assoc] @eqP_union_l
+   @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps 
+  |>sem_pre_false >sem_pre_false >sem_star /2/
+  ]
+qed. 
\ No newline at end of file
diff --git a/matita/matita/lib/tutorial/chapter9.ma b/matita/matita/lib/tutorial/chapter9.ma
new file mode 100644
index 000000000..cc499002c
--- /dev/null
+++ b/matita/matita/lib/tutorial/chapter9.ma
@@ -0,0 +1,252 @@
+(* 
+Moves
+We now define the move operation, that corresponds to the advancement of the 
+state in response to the processing of an input character a. The intuition is 
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must 
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
+*)
+
+include "tutorial/chapter8.ma".
+
+let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+  [ pz ⇒ 〈 pz S, false 〉
+  | pe ⇒ 〈 ϵ, false 〉
+  | ps y ⇒ 〈 `y, false 〉
+  | pp y ⇒ 〈 `y, x == y 〉
+  | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2) 
+  | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
+  | pk e ⇒ (move ? x e)^⊛ ].
+  
+lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+  move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
+// qed.
+
+lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+  move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
+// qed.
+
+lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
+  move S x i^* = (move ? x i)^⊛.
+// qed.
+
+(*
+Example. Let us consider the item                      
+  
+                               (•a + ϵ)((•b)*•a + •b)b
+
+and the two moves w.r.t. the characters a and b. 
+For a, we have two possible positions (all other points gets erased); the innermost 
+point stops in front of the final b, while the other one broadcast inside (b^*a + b)b, 
+so
+ 
+      move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
+
+For b, we have two positions too. The innermost point stops in front of the final b too, 
+while the other point reaches the end of b* and must go back through b*a:  
+    
+      move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a +  ϵ)((•b)*•a + b)•b, false〉
+
+*)
+
+definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
+
+lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b. 
+  pmove ? x 〈i,b〉 = move ? x i.
+// qed.
+
+lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b. 
+  a::l1 = b::l2 → a = b.
+#A #l1 #l2 #a #b #H destruct //
+qed. 
+
+(* Obviously, a move does not change the carrier of the item, as one can easily 
+prove by induction on the item. *)
+
+lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
+  |\fst (move ? a i)| = |i|.
+#S #a #i elim i //
+  [#i1 #i2 #H1 #H2 >move_cat >erase_odot //
+  |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); // 
+  ]
+qed.
+
+(* Here is our first, major result, stating the correctness of the
+move operation. The proof is a simple induction on i. *)
+
+theorem move_ok:
+ ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S. 
+   \sem{move ? a i} w ↔ \sem{i} (a::w).
+#S #a #i elim i 
+  [normalize /2/
+  |normalize /2/
+  |normalize /2/
+  |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
+    [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
+    |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
+    ]
+  |#i1 #i2 #HI1 #HI2 #w >move_cat
+   @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
+   @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r 
+   @iff_trans[||@iff_sym @deriv_middot //]
+   @cat_ext_l @HI1
+  |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w 
+   @iff_trans[|@sem_oplus] 
+   @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
+  |#i1 #HI1 #w >move_star 
+   @iff_trans[|@sem_ostar] >same_kernel >sem_star_w 
+   @iff_trans[||@iff_sym @deriv_middot //]
+   @cat_ext_l @HI1
+  ]
+qed.
+    
+(* The move operation is generalized to strings in the obvious way. *)
+
+notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+
+let rec moves (S : DeqSet) w e on w : pre S ≝
+ match w with
+  [ nil ⇒ e
+  | cons x w' ⇒ w' ↦* (move S x (\fst e))]. 
+
+lemma moves_empty: ∀S:DeqSet.∀e:pre S. 
+  moves ? [ ] e = e.
+// qed.
+
+lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. 
+  moves ? (a::w)  e = moves ? w (move S a (\fst e)).
+// qed.
+
+lemma moves_left : ∀S,a,w,e. 
+  moves S (w@(a::[])) e = move S a (\fst (moves S w e)). 
+#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+qed.
+
+lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. 
+  iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+#S #a #w * #i #b cases b normalize 
+  [% /2/ * // #H destruct |% normalize /2/]
+qed.
+
+lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
+  |\fst (moves ? w e)| = |\fst e|.
+#S #w elim w //
+qed.
+
+theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. 
+   (\snd (moves ? w e) = true) ↔ \sem{e} w.
+#S #w elim w 
+ [* #i #b >moves_empty cases b % /2/
+ |#a #w1 #Hind #e >moves_cons
+  @iff_trans [||@iff_sym @not_epsilon_sem]
+  @iff_trans [||@move_ok] @Hind
+ ]
+qed.
+
+(* It is now clear that we can build a DFA D_e for e by taking pre as states, 
+and move as transition function; the initial state is •(e) and a state 〈i,b〉 is 
+final if and only if b is true. The fact that states in D_e are finite is obvious: 
+in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in 
+e. This is one of the advantages of pointed regular expressions w.r.t. derivatives, 
+whose finite nature only holds after a suitable quotient.
+
+Let us discuss a couple of examples.
+
+Example. 
+Below is the DFA associated with the regular expression (ac+bc)*.
+
+DFA for (ac+bc)  
+
+The graphical description of the automaton is the traditional one, with nodes for 
+states and labelled arcs for transitions. Unreachable states are not shown.
+Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and 
+only if b is true, we may just label nodes with the item.
+The automaton is not minimal: it is easy to see that the two states corresponding to 
+the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe 
+that they define the same language!). In fact, an important property of pres e is that 
+each state has a clear semantics, given in terms of the specification e and not of the 
+behaviour of the automaton. As a consequence, the construction of the automaton is not 
+only direct, but also extremely intuitive and locally verifiable. 
+
+Let us consider a more complex case.
+
+Example. 
+Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
+
+DFA for (a+ϵ)(b*a + b)b 
+
+Remarkably, this DFA is minimal, testifying the small number of states produced by our 
+technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7 
+are final, while 8 and 9 are not). 
+
+
+Move to pit
+. 
+
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *)
+
+definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
+
+(* The following function compute the list of characters occurring in a given
+item i. *)
+
+let rec occur (S: DeqSet) (i: re S) on i ≝  
+  match i with
+  [ z ⇒ [ ]
+  | e ⇒ [ ]
+  | s y ⇒ y::[]
+  | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
+  | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
+  | k e ⇒ occur S e].
+
+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *)
+
+lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
+  move S a i  = pit_pre S i.
+#S #a #i elim i //
+  [#x normalize cases (a==x) normalize // #H @False_ind /2/
+  |#i1 #i2 #Hind1 #Hind2 #H >move_cat 
+   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+  |#i1 #i2 #Hind1 #Hind2 #H >move_plus 
+   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+  |#i #Hind #H >move_star >Hind // 
+  ]
+qed.
+
+(* We cannot escape form the pit state. *)
+
+lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+#S #a #i elim i //
+  [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
+  |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // 
+  |#i #Hind >move_star >Hind //
+  ]
+qed. 
+
+lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+#S #w #i elim w // 
+qed. 
+ 
+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *)
+
+lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
+ moves S w e = pit_pre S (\fst e).
+#S #w elim w
+  [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
+  |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
+    [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) 
+     @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+      [#H2 >(\P H2) // |#H2 @H1 //]
+    |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
+    ]
+  ]
+qed.
\ No newline at end of file