commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index d7b6d4f1e5471b3e009d74e0a5191b5debb94c5a..4ce43679d7c498e59b28f075dd2f0c080c1bf7bb 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -2,10 +2,34 @@
 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 tow 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 typea, like (list (list (nat → nat))), that is a list whose
+elements are lists of functions from natural number 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.
+
+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}.
@@ -21,48 +45,78 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
- λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6| cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6].
-
-theorem nil_cons:
-  ∀A:Type[0].∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
-  #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
-qed.
+(* 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: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
   | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
 
-definition hd ≝ λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+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:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#A #l (elim l) normalize // qed.
+
+(* similarly, we can define the two functions head and tail. 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: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
 definition tail ≝  λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
   match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒  tl].
 
-interpretation "append" 'append l1 l2 = (append ? l1 l2).
+example ex_head: ∀A.∀a,d,l. \ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"\ 6head\ 5/a\ 6 A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) d \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+#A #a #d #l normalize // qed.
 
-theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
-#A #l (elim l) normalize // qed.
+(* Problemi con la notazione *)
+example ex_tail: \ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"\ 6tail\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+normalize // qed.
 
 theorem associative_append: 
- ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/tutorial/chapter3/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
+∀A.∀l1,l2,l3: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. (l1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (l2 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l3).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-(* qualcosa di strano qui theorem append_cons:∀A.∀a:A.∀l,l1: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a]) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l1.
-/2/ qed. *)
+(* Problemi con la notazione *)
+theorem append_cons:
+∀A.∀a:A.∀l,l1: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? a \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l1.
+/2/ qed. 
 
-theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
-  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P l1 l2.
-#A #l1 #l2 #P (cases l1) normalize //
-#a #l3 #heq destruct
-qed.
 
 theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A.
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/tutorial/chapter3/nil_append_elim.def(3)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /2/
 qed.
 
+definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6| cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6].
+
+theorem nil_cons:
+∀A:Type[0].∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+#A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
+qed.
+
 (* iterators *)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝