X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter5.ma;h=21a8abd2fcc515d169a2dca0335ab3136497da8f;hb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb;hp=9cd43fd236e03d1240773b713e8e9786de3e021d;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma
index 9cd43fd23..21a8abd2f 100644
--- a/matita/matita/lib/tutorial/chapter5.ma
+++ b/matita/matita/lib/tutorial/chapter5.ma
@@ -1,253 +1,424 @@
-(* 
-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.*)
+(*
+  More Data Types
+*)
 
-include "basics/list.ma". 
 include "tutorial/chapter4.ma".
+include "arithmetics/nat.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
+(******************************** Option Type *********************************)
+
+(* Matita may only define total functions. However, not always we may return a 
+meaningful value: for instance, working on natural numbers, the predecessor of 
+0 is undefined. In these situations, we may either return a default value 
+(usually, pred 0 = 0), or decide to return an "option type" as a result. An 
+Option type is a polymorphic type that represents encapsulation of an optional 
+value. It consists of either an empty constructor (traditionally called None), 
+or a constructor encapsulating the original data type A (written Some A): *)
+
+inductive option (A:Type[0]) : Type[0] ≝
+   None : option A
+ | Some : A → option A.
+ 
+let rec pred (n:nat) : option nat ≝
+  match n with 
+  [ O ⇒ None nat
+  | S a ⇒ Some nat a
   ].
 
-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)
-*)
+(* The type option A is isomorphic to the disjoint sum between A and unit. The 
+two bijections are simply defined as follows: *)
+
+definition option_to_sum : ∀A.option A → unit + A ≝ λA.λx:option A.
+  match x with 
+  [ None ⇒ inl ?? it 
+  | Some a ⇒ inr ?? a ].
+
+definition sum_to_option :∀A. unit + A → option A ≝ λA.λx:unit+A.
+  match x with 
+  [ inl a ⇒ None A
+  | inr a ⇒ Some A a ].
+
+(* The fact that going from the option type to the sum and back again we get the
+original element follows from a straightforward case analysis: *)
+
+lemma option_bij1: ∀A,x. sum_to_option A (option_to_sum A x) = x.
+#A * [normalize // | #a normalize // ] qed. 
+
+(* The other direction is just slightly more complex, since we need to exploit
+the fact that the unit type contains a single element: we could use lemma 
+eq_unit or proceed by cases on the unit element. *)
+
+lemma option_bij2: ∀A,x. option_to_sum A (sum_to_option A x) = x.
+#A * #x [normalize cases x // | //] qed. 
+
+(* We shall see more examples of functions involving the otion type in the
+next section. *)
+
+(********************************** Lists *************************************)
+
+(* The option type, as well as the cartesian product or the sum are simple
+examples of polymorphic types, that is types that depend in a uniform and 
+effective way on other types. This form of polymorphism (sometimes called 
+"parametric" polymporphism to distinguish it from the "ad hoc" polymorphism
+typical of object oriented languages) is a major feature of modern functional 
+programming languages: in many intersting cases, it allows to write generic 
+functions operating on inputs without depending on their type. Typical examples 
+can be found on lists.
+For instance, appending two lists is an operation that is essentially 
+independent from the type A of the elements in the list, and we would like to 
+write a single append function working parametrically on A.
+
+The first step is to define a type for lists polimorphic over the type A of its 
+elements: *)
+
+inductive list (A:Type[0]) : Type[0] :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+(* The definition should be clear: a list is either empty (nil) or it is 
+obtained by concatenating (cons) an element of type A to a given list. In other 
+words, the type of lists is the smallest inductive type generated by the two 
+constructors nil and cons.
+
+The first element of a list is called its "head". If the list is empty the head 
+is undefined: as discussed in the previous section, we should either return a 
+``default'' element, or decide to return an option type. 
+We have an additional complication in this case, since the ``default'' element 
+should have type A, and we know nothing about A (it could even be an empty 
+type!). We have no way to guess a canonical element, and the only possibility 
+(along this approach) is to take it in input. These are the two options: *)
+
+definition hd ≝ λA.λl: list A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition option_hd ≝ λA.λl:list A. 
+  match l with [ nil ⇒ None ? | cons a _ ⇒ Some ? a ].
+
+(* What remains of a list after removing its head is called the "tail" of the 
+list. Again, the tail of an empty list is undefined, but in this case the result 
+must be a list, and we have a canonical inhabitant of lists, that is the empty 
+list. So, it is natural to extend the definition of tail saying that the tail of 
+nil is nil (that is very similar to say that the predecessor of 0  is 0): *)
+
+definition tail ≝  λA.λl: list A.
+  match l with [ nil ⇒  nil ? | cons hd tl ⇒  tl].
+
+(* Using destruct, it is easy to prove that cons is injective in both 
+arguments. *)
+
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.
+  cons ?a1 l1 = cons ? a2 l2 → a1 = a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
+
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.
+  cons ? a1 l1 = cons ? a2 l2 → l1 = l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
+
+(* The append function is defined by recursion over the first list: *)
+let rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  cons ? hd (append A tl 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.
+(******************************* list notation ********************************)
 
-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.
+(* Before discussing more operations over lists, it is convenient to introduce a 
+bit of notation; in particular, we shall write a::l for (cons ? a l); 
+[a1;a2,…, an] for the list composed by the elements a1, a2,…, an and l1@l2 for 
+the concatenation of l1 and l2. 
 
-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.
+This can be obtained by the following declarations: *)
 
-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. 
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47 for @{'cons $hd $tl}.
 
-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. 
+notation "[ list0 term 19 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
 
-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. 
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47 for @{'append $l1 $l2}.
 
-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 //
-  ]
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+(* Note that [ ] is an alternative notation for the empty list, and [a] is a 
+list containing a singleton element a. 
+Let us check the notation: *)
+
+example append_ex1: [true;false]@[true] = [true;false;true]. 
+normalize // qed.
+
+(* As a simple exerices, now that we have a comfortable notation, let to prove 
+that append is associative, and that nil is a neutral element for it. *)
+
+lemma associative_append: ∀A.∀l1,l2,l3:list A. l1 @ (l2 @ l3) = (l1 @ l2) @ l3. 
+#A #l1 elim l1 [normalize //] 
+#a #tl #Hind #l2 #l3 normalize @eq_f @Hind qed.
+
+lemma append_nil: ∀A.∀l:list A. l@[ ] = l. 
+#A #l elim l // #a #tl #Hind normalize >Hind // qed.
+
+let rec length (A:Type[0]) (l:list A) on l ≝
+  match l with 
+  [ nil ⇒ O
+  | cons a tl ⇒ 1+(length A tl)
+  ].
+  
+interpretation "list length" 'card l = (length ? l).
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
 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/
-  ]
+lemma length_append: ∀A.∀l1,l2:list A. 
+  |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // 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 //
-  ]
+let rec nth (A:Type[0]) (l:list A) n on n ≝
+  match n with 
+  [ O ⇒ option_hd ? l
+  | S x ⇒ nth A (tail ? l) x
+  ].
+  
+lemma nth_length : ∀A,l,n. n < length A l → nth A l n ≠ None ?.
+#A #l elim l 
+  [#n normalize #H @False_ind /2 by absurd/
+  |#a #tl #Hind #n normalize 
+   #H lapply (le_S_S_to_le  … H) -H cases n
+     [#_ normalize % #H1 destruct (H1)
+     |#m #H normalize @Hind @H
+     ]
+   ] 
 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. 
-*)
+(*************************** More list operations *****************************)
 
-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
+(* We conclude this section discussing another important operation over lists, 
+namely the reverse funtion, retrurning a list with the same elements of the 
+original list but in reverse order.
+
+One could define the revert operation as follows: *)
+
+let rec rev A (l1: list A) on l1 ≝
+  match l1 with 
+  [ nil ⇒ nil ?
+  | cons a tl ⇒ rev A tl @ [a]
   ].
 
-(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
+(* However, this implementation is sligtly inefficient, since it has a quadratic 
+complexity. A better solution consists in exploiting an accumulator, passing 
+through the following auxilary function: *)
 
-let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
-  match l1 with
+let rec rev_append A (l1,l2:list A) 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
+  | cons a tl ⇒ rev_append A tl (a::l2)
   ].
 
-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. 
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a]. 
+// qed.
+
+example example_rev1: reverse ? [true;false] = [false;true]. 
+normalize // qed.
+
+(* Let us prove the following results, as a simple exercise. 
+
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = (reverse A l)@[a].
+
+If you try a brute force approach (e.g., induction on l); you will get in 
+trouble. The point is that reverse is defined as a particular case of 
+rev_append, and you should suitably generalize your result taking rev_append in 
+mind. 
+*)
+
+lemma rev_append_append: ∀A,l1,l2,l3. 
+  rev_append A l1 (l2@l3)  = rev_append A l1 l2 @l3.
+#A #l1 elim l1 // 
+#hd #tl normalize #Hind #l2 #l3 @(Hind (hd::l2)) qed. 
+
+(* Now we get reverse_cons as a trivial corollary, since 
+  reverse A (a::l) = rev_append A (a::l) [ ] = rev_append l [a] =
+  rev_append l ([ ]@[a]) = (rev_append l [ ])@[a] = reverse A l @ [a]
+*)
+  
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = reverse A l@[a].
+#A #a #l normalize <rev_append_append % qed.
+
+(* More generally, we can prove the following property of rev_append
+specyfing its general behaviour *)
 
-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/ 
+lemma rev_append_def : ∀S,l1,l2. 
+  rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 #l2 normalize <rev_append_append //  
 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 //
+lemma reverse_append: ∀S,l1,l2. 
+  reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons >Hind >associative_append // 
 qed.
 
-(*
-Sublists
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append 
+>reverse_single >Hind // qed.
 
-*)
-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 //
-    ]
-  ]
+
+(***************************** List iterators *********************************)
+
+(* In general, an iterator for some data type is an object that enables to 
+traverse its structure performing a given computation. 
+There is a canonical set of iterators over lists deriving from the programming 
+experience. In this section we shall review a few of them, proving some of their 
+properties.
+
+A first, famous iterator is the map function, that applies a function f to each 
+element of a list [a1,…, an],  building the list [f a1; … ; f an]. *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+(* The map function distributes over append, as can be simply proved by 
+induction over the first list: *)
+
+lemma map_append : ∀A,B,f,l1,l2.
+  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1
+  [ #l2 @refl | #h #t #IH #l2 normalize >IH // ] qed.
+  
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
 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/]
-]
+(* The most important iterator is traditionally called "fold"; we shall only 
+consider the so called fold-right variant, that takes in input a function 
+f:A→B→B, a list [a1; …; an] of elements of type A, a base element b:B and 
+returns the value 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)].
+
+(* Many other interesting functions can be defined in terms of foldr. A first 
+interesting example is the filter function, taking in input a boolean test p and 
+a list l and returning the sublist of all elements of l satisfying the test. *)
+
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* As another example, we can generalize the map function to an operation taking 
+in input a binary function f:A → B → C, two lists [a1;… ;an] and [b1;… ;bm] and 
+returning the list [f a1 b1; ˙… ;f an b1;… ;f a1 b_m; … f an bm]. *)
+
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+  foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+(* The folded function 
+                  λi,acc.(map ?? (f i) l2)@acc
+takes in input an element i and an accumulator, and add to the accumulator the 
+values obtained by mapping the partial instantiation (f i) on the elements of 
+l2. This function is iterated over all elements of the first list l1, starting 
+with an empty accumulator. *)
+
+(************************************ Vectors *********************************)
+
+(* A vector of length n of elements of type A is simply defined in Matita as a 
+record composed by a list of elements of type A, plus a proof that the list has 
+the expected length. Vectors are a paradigmatic example of dependent type, that 
+is of a type whose definition depends on a term. *)
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
+{ vec :> list A;
+  len: length ? vec = n }.
+
+(* Given a list l we may trivially turn it into a vector of length |l|; we just 
+need to prove that |l|=|l| that follows from the reflexivity of equality. *)
+
+lemma Vector_of_list ≝ λA,l.mk_Vector A (|l|) l (refl ??).
+
+(* Then we can prove that any vector of zero lenght has no elements: *)
+
+lemma vector_nil: ∀A.∀v:Vector A 0. 
+  v = Vector_of_list A [ ]. 
+#A * * // #a #tl normalize #H destruct
+qed. 
+
+(* It is convenient to re-define on vectors the hd, tail and cons operations 
+on lists *)
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+  mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
 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]
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+  mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
 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 //
-    ] 
-  ]
+definition vec_hd ≝ λA.λn.λv:Vector A (S n). hd A v ?. 
+elim v * [normalize #H destruct | #a #H #eq @a] 
 qed.
 
-(*
-Filtering
-*)
+(* Any vector of lenght (S n) can be expanded as a concatenation of a head and a
+tail vector of length n *)
 
-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
+lemma vec_expand: ∀A,n,v. 
+ v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v).
+#A #n * #l cases l [normalize in ⊢ (%→?); #H destruct  |//]
 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
+(* Most functions operating on lists can be naturally extended to vectors: 
+interesting cases are vec_append, concatenating vectors, and vec_map, mapping a 
+function f on all elements of the input vector and returning a vector of the 
+same dimension of the input one. *)
 
-*)
+definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
+mk_Vector A (n1+n2) (v1@v2) ?.
+>length_append >(len … v1) >(len … v2) // qed. 
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v) 
+  (trans_eq … (length_map …) (len A n v)).
+  
+(* Since a vector is automatically coerced, if needed, to the list of its 
+elements, we may simply use typical functions over lists (such as nth) to 
+extract/filter specific components. 
+
+The following function (change_vec A n v a i) replaces the content of the vector 
+v at position i with the value a. *)
+
+let rec change_vec (A:Type[0]) (n:nat) on n ≝
+match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
+[ O ⇒ λv,a,i.v
+| S m ⇒ λv,a,i.
+  match i with
+  [ O ⇒ vec_cons A a m (vec_tail … v) 
+  | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
+  ]
+].
+
+(* A frequent operation between vectors is their comparison. The following 
+lemma allow us to reduce the comparisons of vectors of a same lenght to the
+comparison of their components. *)
+
+lemma eq_vec: ∀A,n.∀v1,v2:Vector A n. 
+  (∀i. i < n → nth A v1 i = nth A v2 i) → v1 = v2.
+#A #n elim n -n 
+  [#v1 #v2 #_ >(vector_nil A v1) >(vector_nil A v2) //
+  |#n #Hind #v1 #v2 #H >(vec_expand … v1) >(vec_expand … v2)
+   >(Hind (vec_tail … v1) (vec_tail … v2))
+    [cut (vec_hd A n v1 = vec_hd A n v2) // lapply (H 0 (lt_O_S ?)) -H
+     >(vec_expand … v1) in ⊢ (%→?); >(vec_expand … v2) in ⊢ (%→?);
+     change with (Some ?? = Some ?? → ?) #H destruct (H) @e0
+    |#i #ltin @(H (S i)) @le_S_S //
+    ]
+  ]
+qed.
 
-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