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=d4497a18b5e34d8e5399a94ec09f81133f56340e;hb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;hp=0000000000000000000000000000000000000000;hpb=4672640dc168a3adcbea86887c38d895358288e8;p=helm.git

diff --git a/weblib/basics/lists/iterators.ma b/weblib/basics/lists/iterators.ma
new file mode 100644
index 000000000..d4497a18b
--- /dev/null
+++ b/weblib/basics/lists/iterators.ma
@@ -0,0 +1,35 @@
+(**************************** iterators ******************************)
+
+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)].
+
+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 //] 
+qed.
+  
+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)].
+ 
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* compose f [a1;...;an] [b1;...;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.
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+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