[helm.git] / matita / matita / lib / tutorial / chapter5.ma

(*
  More Data Types
*)

include "tutorial/chapter4.ma".
include "arithmetics/nat.ma".


(******************************** 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
  ].

(* 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) ].

(******************************* list notation ********************************)

(* 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. 

This can be obtained by the following declarations: *)

notation "hvbox(hd break :: tl)"
  right associative with precedence 47 for @{'cons $hd $tl}.

notation "[ list0 term 19 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).
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 length_append: ∀A.∀l1,l2:list A. 
  |l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
qed.

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.


(*************************** More list operations *****************************)

(* 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]
  ].

(* 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 rev_append A (l1,l2:list A) on l1 ≝
  match l1 with 
  [ nil ⇒ l2
  | cons a tl ⇒ rev_append A tl (a::l2)
  ].

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 rev_append_def : ∀S,l1,l2. 
  rev_append S l1 l2 = (reverse S l1) @ l2 .
#S #l1 #l2 normalize <rev_append_append //  
qed.

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.

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.


(***************************** 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.

(* 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.

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.

definition vec_hd ≝ λA.λn.λv:Vector A (S n). hd A v ?. 
elim v * [normalize #H destruct | #a #H #eq @a] 
qed.

(* Any vector of lenght (S n) can be expanded as a concatenation of a head and a
tail vector of length n *)

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.

(* 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.