commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index a75b4ce1e023e8e09bf20662f4718ee2e7ae0e80..9d1e81de0a5bca9307eae6c7eba869f0b6caf504 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -176,15 +176,26 @@ f:A → B, a list l = [a1; a2; ... ; an] and returning the list
 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 ≝
  match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
 
-(* Another simple example is the filter function that given a list l: list A and
-a boolean test p:A → bool returns the sublist of elements satisfying the test. *)
+(* 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:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 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 
+bbol.ma to this purpose. *)
 
 definition filter ≝ 
   λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
   \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p x) (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) l0) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 
 (* 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 
+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.
 *)
 
@@ -196,14 +207,32 @@ lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/f
   \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-(* The most typical list iterator is the fold function, that taken
-a list l = [a1; a2; ... an], a base value b, and a function f: A → B → B 
-returns f a1 (f a2 (... (f an b)...)). *)
+(* 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.
+*)
 
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
-  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+definition map_again ≝ λA,B,f,l. \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 A (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (λa,l.f a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] l.
 
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+(* 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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_map: ∀A,B,f. \ 5a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"\ 6ExtEq\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f) (\ 5a href="cic:/matita/tutorial/chapter3/map_again.def(2)"\ 6map_again\ 5/a\ 6 A B f).
+#A #B #f #n (elim n) normalize // qed. 
+
+
+ theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
 (*
@@ -253,17 +282,4 @@ theorem fold_filter:
   | >\ 5a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
 qed.
 
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
-  {op :2> A → A → A; 
-   nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a; 
-   nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
-   assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
-  }.
-
-theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
-  op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-    \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
-#A #B #I #J #nil #op #f (elim I) normalize 
-  [>\ 5a href="cic:/matita/tutorial/chapter3/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
-qed.
-
+record Aop (A:Type[0]) (ni
\ No newline at end of file