commit by user andrea

[helm.git] / weblib / basics / lists / iterators.ma

diff --git a/weblib/basics/lists/iterators.ma b/weblib/basics/lists/iterators.ma
index d4497a18b5e34d8e5399a94ec09f81133f56340e..a056992698badf1ae52f89fa238ca2a1256ef9a7 100644 (file)
--- 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 \ 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 ≝
- 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)].
+(******************************* map **********************************)
+\ 5img class="anchor" src="icons/tick.png" id="map"\ 6let rec map (A,B:Type[0]) (f: A → 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 ≝
+ 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)].
 
-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 //] 
+\ 5img class="anchor" src="icons/tick.png" id="map_append"\ 6lemma map_append : ∀A,B,f,l1,l2.
+  (\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
+#A #B #f #l1 elim l1 [ #l2 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 | #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 ≝  
+
+\ 5pre class="smallmargin" style="display: inline;"\ 6\ 5img class="anchor" src="icons/tick.png" id="eq_map"\ 6lemma 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/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed. \ 5/pre\ 6 
+
+(**************************** fold right ******************************)
+\ 5img class="anchor" src="icons/tick.png" id="foldr"\ 6let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/lists/lists/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 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.
+\ 5img class="anchor" src="icons/tick.png" id="compose"\ 6definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    \ 5a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) [ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 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. *)