commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index 9d1e81de0a5bca9307eae6c7eba869f0b6caf504..ca7e89355b9e9bf5fcf98d772056a4c5b6a50dd3 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -228,29 +228,46 @@ definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a \ 5a title="leibnitz's e
 (* 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).
+lemma eq_maps: ∀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.
-
-(*
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
-  [ nil ⇒ nil ?  
-  | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
-  ]. *)
-
-(**************************** fold *******************************)
-
-let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
+(* 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. \ 5a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"\ 6ExtEq\ 5/a\ 6 A B f g → \ 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 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A B f) (\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 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.
+
+(**************************** BIGOPS *******************************)
+
+(* 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→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→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 ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p a) (op (f a) (fold A B op b p f l))
       (fold A B op b p f l)].
-      
-notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
+
+(* 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}.
 
@@ -282,4 +299,16 @@ 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]) (ni
\ No newline at end of file
+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:A → B.
+ 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.
\ No newline at end of file