weblib/basics/lists/iterators.ma

   1 (**************************** iterators ******************************)
   2
   3 include "basics/lists/append.ma".
   4
   5 let rec map (A,B:Type[0]) (f: A \ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6→\ 5/span\ 6 B) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
   6  match l with [ nil ⇒ \ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5font class="Apple-style-span" color="#FF0000"\ 6:\ 5/font\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 (map A B f tl)].
   7
   8 lemma map_append : ∀A,B,f,l1,l2.
   9   (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
  10 #A #B #f #l1 elim l1 [ #l2 @refl | #h #t #IH #l2 normalize //]
  11 qed.
  12
  13 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
  14  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  15
  16 definition filter ≝
  17   λT.λp:T → bool.
  18   foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
  19
  20 (* compose f [a1;...;an] [b1;...;bm] =
  21   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
  22
  23 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
  24     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
  25
  26 lemma filter_true : ∀A,l,a,p. p a = true →
  27   filter A p (a::l) = a :: filter A p l.
  28 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
  29
  30 lemma filter_false : ∀A,l,a,p. p a = false →
  31   filter A p (a::l) = filter A p l.
  32 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
  33
  34 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
  35 #A #B #f #g #l #eqfg (elim l) normalize // qed.