X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flists%2Fiterators.ma;fp=weblib%2Fbasics%2Flists%2Fiterators.ma;h=a056992698badf1ae52f89fa238ca2a1256ef9a7;hb=d13c122f5238597ef543eb213eb5ce788c0e9fd9;hp=d4497a18b5e34d8e5399a94ec09f81133f56340e;hpb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;p=helm.git

diff --git a/weblib/basics/lists/iterators.ma b/weblib/basics/lists/iterators.ma
index d4497a18b..a05699269 100644
--- a/weblib/basics/lists/iterators.ma
+++ b/weblib/basics/lists/iterators.ma
@@ -2,26 +2,33 @@
 
 include "basics/lists/append.ma".
 
-let rec map (A,B:Type[0]) (f: A span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"→/span B) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a B ≝
- match l with [ nil ⇒ a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x font class="Apple-style-span" color="#FF0000":/fonta title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
+(******************************* map **********************************)
+img class="anchor" src="icons/tick.png" id="map"let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x font class="Apple-style-span" color="#ff0000":/fonta title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
 
-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 //] 
+img class="anchor" src="icons/tick.png" id="map_append"lemma map_append : ∀A,B,f,l1,l2.
+  (a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a A B f l1) a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a A B f l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a A B f (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+#A #B #f #l1 elim l1 [ #l2 @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a | #h #t #IH #l2 normalize //] 
 qed.
-  
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+
+pre class="smallmargin" style="display: inline;"img class="anchor" src="icons/tick.png" id="eq_map"lemma eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed. /pre 
+
+(**************************** fold right ******************************)
+img class="anchor" src="icons/tick.png" id="foldr"let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
- 
-definition filter ≝ 
-  λT.λp:T → bool.
-  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
 
+(***************************** compose ********************************)
 (* compose f [a1;...;an] [b1;...;bm] = 
-  [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
+     [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
  
-definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
-    foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+img class="anchor" src="icons/tick.png" id="compose"definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) [ a title="nil" href="cic:/fakeuri.def(1)"]/a l1.
+
+(***************************** filter *********************************)
+(* definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
 
 lemma filter_true : ∀A,l,a,p. p a = true → 
   filter A p (a::l) = a :: filter A p l.
@@ -29,7 +36,4 @@ lemma filter_true : ∀A,l,a,p. p a = true →
 
 lemma filter_false : ∀A,l,a,p. p a = false → 
   filter A p (a::l) = filter A p l.
-#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
-
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
-#A #B #f #g #l #eqfg (elim l) normalize // qed.
\ No newline at end of file
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed. *)