From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 May 2013 13:58:02 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d13c122f5238597ef543eb213eb5ce788c0e9fd9;p=helm.git

commit by user andrea
---

diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
index 73fbd36cc..5b0c403e1 100644
--- a/weblib/basics/lists/append.ma
+++ b/weblib/basics/lists/append.ma
@@ -3,37 +3,37 @@
 include "basics/lists/lists.ma".
 include "basics/relations.ma".
 
-img class="anchor" src="icons/tick.png" id="append"let rec append A (l1: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
+let rec append A (l1: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
   | cons hd tl ⇒  hd :a title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-img class="anchor" src="icons/tick.png" id="append_nil"theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="associative_append"theorem associative_append: 
- ∀A.font class="Apple-style-span" color="#FF0000"a href="cic:/matita/basics/relations/associative.def(1)"associative/a /font(a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A).
+theorem associative_append: 
+ ∀A.font class="Apple-style-span" color="#ff0000"a href="cic:/matita/basics/relations/associative.def(1)"associative/a /font(a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="append_cons"theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al1.
+theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al1.
 #A #a #l #l1 >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a // qed.
 
-img class="anchor" src="icons/tick.png" id="nil_append_elim"theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
+theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
   l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a[a title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-img class="anchor" src="icons/tick.png" id="nil_to_nil"theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
+theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
   l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
 #A #l1 #l2 #isnil @(a href="cic:/matita/basics/lists/append/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 (* comparing lists *)
 
-img class="anchor" src="icons/tick.png" id="compare_append"lemma compare_append : ∀A,l1,l2,l3,l4. l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al4 → 
+lemma compare_append : ∀A,l1,l2,l3,l4. l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al4 → 
 ∃l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a Aa title="exists" href="cic:/fakeuri.def(1)"./a(l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l4a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al2) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al4).
 #A #l1 elim l1
   [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
@@ -48,5 +48,4 @@ qed.
       ]
     ]
   ]
-qed.
-
+qed. 
\ No newline at end of file
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. *)
diff --git a/weblib/basics/lists/length.ma b/weblib/basics/lists/length.ma
new file mode 100644
index 000000000..a347b1066
--- /dev/null
+++ b/weblib/basics/lists/length.ma
@@ -0,0 +1,115 @@
+(**************************** length ******************************)
+
+include "basics/lists/iterators.ma".
+include "basics/lists/reverse.ma".
+include "arithmetics/nat.ma".
+
+img class="anchor" src="icons/tick.png" id="length"let rec length (A:Type[0]) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l ≝ 
+  match l with 
+    [ nil ⇒ a title="natural number" href="cic:/fakeuri.def(1)"0/a
+    | cons a tl ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (length A tl)].
+
+interpretation "list length" 'card l = (length ? l).
+
+img class="anchor" src="icons/tick.png" id="length_tail"lemma length_tail: ∀A,l. |a href="cic:/matita/basics/lists/lists/tail.def(1)"tail/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (|la title="list length" href="cic:/fakeuri.def(1)"|/a).
+#A #l elim l // 
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_tail1"lemma length_tail1 : ∀A,l.a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a |la title="list length" href="cic:/fakeuri.def(1)"|/a → |a href="cic:/matita/basics/lists/lists/tail.def(1)"tail/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A * normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_append"lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="list length" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|l2a title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_map"lemma length_map: ∀A,B,l.∀f:A→B. |a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a ?? f la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_reverse"lemma length_reverse: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l elim l // #a #l0 #IH >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a >a href="cic:/matita/basics/lists/length/length_append.def(2)"length_append/a >IH normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="lenght_to_nil"lemma lenght_to_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
+  |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"0/a → l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [ a title="nil" href="cic:/fakeuri.def(1)"]/a.
+#A * // #a #tl normalize #H destruct
+qed.
+ 
+img class="anchor" src="icons/tick.png" id="lists_length_split"lemma lists_length_split : ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.a title="exists" href="cic:/fakeuri.def(1)"∃/ala,lba title="exists" href="cic:/fakeuri.def(1)"./a
+  (|laa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a laa title="append" href="cic:/fakeuri.def(1)"@/alb) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (|laa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a laa title="append" href="cic:/fakeuri.def(1)"@/alb).
+#A #l1 elim l1
+[ #l2 %{[ a title="nil" href="cic:/fakeuri.def(1)"]/a} %{l2} % % %
+| #hd1 #tl1 #IH *
+  [ %{[ a title="nil" href="cic:/fakeuri.def(1)"]/a} %{(hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1)} %2 % %
+  | #hd2 #tl2 cases (IH tl2) #x * #y *
+    [ * #IH1 #IH2 %{(hd2:a title="cons" href="cic:/fakeuri.def(1)":/ax)} %{y} % normalize % //
+    | * #IH1 #IH2 %{(hd1:a title="cons" href="cic:/fakeuri.def(1)":/ax)} %{y} %2 normalize % // ]
+  ]
+]
+qed.
+
+(****************** traversing two lists in parallel *****************)
+img class="anchor" src="icons/tick.png" id="list_ind2"lemma list_ind2 : 
+  ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2.∀P:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1 → a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2 → Prop.
+  |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a →
+  (P [a title="nil" href="cic:/fakeuri.def(1)"]/a [a title="nil" href="cic:/fakeuri.def(1)"]/a) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1) (hd2:a title="cons" href="cic:/fakeuri.def(1)":/atl2)) → 
+  P l1 l2.
+#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
+generalize in match Hl; generalize in match l2;
+elim l1
+  [#l2 cases l2 // normalize #t2 #tl2 #H destruct
+  |#t1 #tl1 #IH #l2 cases l2
+    [normalize #H destruct
+    |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="list_cases2"lemma list_cases2 : 
+  ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2.∀P:Prop.
+  |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a →
+  (l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → P) → 
+  (∀hd1,hd2,tl1,tl2.l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1 → l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a hd2:a title="cons" href="cic:/fakeuri.def(1)":/atl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hl)
+  [ #Pnil #Pcons @Pnil //
+  | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+img class="anchor" src="icons/tick.png" id="append_l1_injective"lemma append_l1_injective : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+  
+img class="anchor" src="icons/tick.png" id="append_l2_injective"lemma append_l2_injective : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="append_l1_injective_r"lemma append_l1_injective_r :
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l3a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l4a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq)
+>a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a #Heq1
+lapply (a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"append_l2_injective/a … Heq1) [ // ] #Heq2
+lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq2) //
+qed.
+  
+img class="anchor" src="icons/tick.png" id="append_l2_injective_r"lemma append_l2_injective_r : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l3a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l4a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq)
+>a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a #Heq1
+lapply (a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"append_l1_injective/a … Heq1) [ // ] #Heq2
+lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq2) //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_rev_append"lemma length_rev_append: ∀A.∀l,acc:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"rev_append/a ? l acca title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|acca title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l elim l // #a #tl #Hind normalize 
+#acc >Hind normalize // 
+qed.
+ 
\ No newline at end of file
diff --git a/weblib/basics/lists/reverse.ma b/weblib/basics/lists/reverse.ma
new file mode 100644
index 000000000..20a0110d1
--- /dev/null
+++ b/weblib/basics/lists/reverse.ma
@@ -0,0 +1,43 @@
+(**************************** reverse *****************************)
+
+include "basics/lists/iterators.ma".
+
+img class="anchor" src="icons/tick.png" id="rev_append"let rec rev_append S (l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (a:a title="cons" href="cic:/fakeuri.def(1)":/al2)
+  ]
+.
+
+img class="anchor" src="icons/tick.png" id="reverse"definition reverse ≝λS.λl.a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"rev_append/a S l [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+
+img class="anchor" src="icons/tick.png" id="reverse_single"lemma reverse_single : ∀S,a. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a. 
+// qed.
+
+img class="anchor" src="icons/tick.png" id="rev_append_def"lemma rev_append_def : ∀S,l1,l2. 
+  a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"rev_append/a S l1 l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 .
+#S #l1 elim l1 normalize 
+  [// | #a #tl #Hind #l2 >Hind >(Hind a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a) >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a]
+qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_cons"lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a.
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_append"lemma reverse_append: ∀S,l1,l2. 
+  a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a
+>a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a >Hind // qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_reverse"lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+#S #l elim l // #a #tl #Hind >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >Hind %
+qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+img class="anchor" src="icons/tick.png" id="list_elim_left"lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a S) →
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/lists/reverse/reverse_reverse.def(8)"reverse_reverse/a … l) 
+generalize in match (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l); #l elim l //
+#a #tl #H >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a @Pstep //
+qed.
diff --git a/weblib/basics/lists/search.ma b/weblib/basics/lists/search.ma
new file mode 100644
index 000000000..77bfa106d
--- /dev/null
+++ b/weblib/basics/lists/search.ma
@@ -0,0 +1,268 @@
+include "basics/lists/length.ma".
+include "basics/types.ma".
+
+(****************************** mem ********************************)
+img class="anchor" src="icons/tick.png" id="mem"let rec mem A (a:A) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l ≝
+  match l with
+  [ nil ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a
+  | cons hd tl ⇒ aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ahd a title="logical or" href="cic:/fakeuri.def(1)"∨/a mem A a tl
+  ]. 
+  
+img class="anchor" src="icons/tick.png" id="mem_append"lemma mem_append: ∀A,a,l1,l2.a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) →
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? a l1 a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? a l2.
+#A #a #l1 elim l1 
+  [#l2 #mema %2 @mema
+  |#b #tl #Hind #l2 * 
+    [#eqab %1 %1 @eqab 
+    |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_append_l1"lemma mem_append_l1: ∀A,a,l1,l2.a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a l1 → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+#A #a #l1 #l2 elim l1
+  [whd in ⊢ (%→?); @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+  |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_append_l2"lemma mem_append_l2: ∀A,a,l1,l2.a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a l2 → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+#A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_single"lemma mem_single: ∀A,a,b. a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a a title="cons" href="cic:/fakeuri.def(1)"[/aba title="nil" href="cic:/fakeuri.def(1)"]/a → aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab.
+#A #a #b * // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_map"lemma mem_map: ∀A,B.∀f:A→B.∀l,b. 
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? b (a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a … f l) → a title="exists" href="cic:/fakeuri.def(1)"∃/aa. a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? a l a title="logical and" href="cic:/fakeuri.def(1)"∧/a f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
+#A #B #f #l elim l 
+  [#b normalize @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+  |#a #tl #Hind #b normalize *
+    [#eqb @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
+    |#memb cases (Hind … memb) #a * #mema #eqb
+     @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_map_forward"lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l. 
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a l → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a B (f a) (a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a ?? f l).
+ #A #B #f #a #l elim l
+  [normalize @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+  |#b #tl #Hind * 
+    [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+  ]
+qed.
+
+(****************************** fitler ******************************)
+
+img class="anchor" src="icons/tick.png" id="filter"definition filter ≝ 
+  λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+  a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T) (λx,l0.if p x then x:a title="cons" href="cic:/fakeuri.def(1)":/al0 else l0) (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a T).
+
+img class="anchor" src="icons/tick.png" id="filter_true"lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a :a title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+img class="anchor" src="icons/tick.png" id="filter_false"lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
+  a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+(****************************** mem filter ***************************)
+img class="anchor" src="icons/tick.png" id="mem_filter"lemma mem_filter: ∀S,f,a,l. 
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a S a (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a S f l) → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a S a l.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize
+  [* [#eqab %1 @eqab | #H %2 @Hind @H]
+  |#H %2 @Hind @H]
+qed.
+
+img class="anchor" src="icons/tick.png" id="mem_filter_true"lemma mem_filter_true: ∀S,f,a,l. 
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a S a (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a S f l)  → f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#S #f #a #l elim l [normalize @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a ]
+#b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b)) #H
+normalize >H normalize [2:@Hind]
+* [#eqab // | @Hind]
+qed. 
+
+img class="anchor" src="icons/tick.png" id="mem_filter_l"lemma mem_filter_l: ∀S,f,x,l. (f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a S x l →
+a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a S x (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? f l).
+#S #f #x #l #fx elim l [@a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a]
+#b #tl #Hind * 
+  [#eqxb <eqxb >(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a ???? fx) %1 % 
+  |#Htl cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b)) #fb 
+    [>(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a ???? fb) %2 @Hind @Htl
+    |>(a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a ???? fb) @Hind @Htl
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="filter_case"lemma filter_case: ∀A,p,l,x. a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? x l → 
+  a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? x (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p l) a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? x (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A (λx.a title="boolean not" href="cic:/fakeuri.def(1)"¬/a p x) l).
+#A #p #l elim l 
+  [#x @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a 
+  |#a #tl #Hind #x * 
+    [#eqxa >eqxa cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #Hcase
+      [%1 >(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a p Hcase) %1 % 
+      |%2 >(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a ??) [%1 % | >Hcase %]
+      ]
+    |#memx cases (Hind … memx) -memx #memx
+      [%1 cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #Hpa 
+        [>(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a p Hpa) %2 @memx
+        |>(a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a A tl a p Hpa) @memx
+        ]
+      |cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #Hcase
+        [%2 >(a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a A tl a) [@memx |>Hcase %]
+        |%2 >(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a) [%2 @memx|>Hcase %]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="filter_length2"lemma filter_length2: ∀A,p,l. |a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A p la title="list length" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a A (λx.a title="boolean not" href="cic:/fakeuri.def(1)"¬/a p x) la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #p #l elim l //
+#a #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #Hcase
+  [>(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a p Hcase) >(a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a A tl a ??) 
+    [@(a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a ?? a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a) @Hind | >Hcase %]
+  |>(a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a A tl a p Hcase) >(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a A tl a ??) 
+    [<a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a @(a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a ?? a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a) @Hind | >Hcase %]
+  ]
+qed.
+
+(***************************** unique *******************************)
+img class="anchor" src="icons/tick.png" id="unique"let rec unique A (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l ≝ 
+  match l with 
+  [nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a
+  |cons a tl ⇒ a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a A a tl a title="logical and" href="cic:/fakeuri.def(1)"∧/a unique A tl].
+
+img class="anchor" src="icons/tick.png" id="unique_filter"lemma unique_filter : ∀S,l,f.
+ a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a S l → a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a S (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a S f l).
+#S #l #f elim l //
+#a #tl #Hind * 
+#memba #uniquetl cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (f a)) #Hfa
+  [>(a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a ???? Hfa) % 
+    [@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … memba) @a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a |/span class="autotactic"2span class="autotrace" trace /span/span/ ]
+  |>a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a /span class="autotactic"2span class="autotrace" trace /span/span/
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="filter_eqb"lemma filter_eqb : ∀m,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → 
+  (a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? m l a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/ama title="nil" href="cic:/fakeuri.def(1)"]/a)a title="logical or" href="cic:/fakeuri.def(1)"∨/a(a title="logical not" href="cic:/fakeuri.def(1)"¬/aa href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? m l a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a).
+#m #l elim l
+  [#_ %2 % [% @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a | //]
+  |#a #tl #Hind * #Hmema #Hunique
+   cases (Hind Hunique)
+    [* #Hmemm #Hind %1 % [%2 //]
+     >a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a // @a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a % #eqma @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? Hmemm) //
+    |* #Hmemm #Hind cases (a href="cic:/matita/arithmetics/nat/decidable_eq_nat.def(5)"decidable_eq_nat/a m a) #eqma 
+      [%1 <eqma % [%1 //] >a href="cic:/matita/basics/lists/search/filter_true.def(3)"filter_true/a [2: @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a //] >Hind //
+      |%2 % 
+        [@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … Hmemm) * // #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a  @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … H) //
+        |>a href="cic:/matita/basics/lists/search/filter_false.def(3)"filter_false/a // @a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a @eqma
+        ]
+      ]
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_filter_eqb"lemma length_filter_eqb: ∀m,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → 
+  |a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="natural number" href="cic:/fakeuri.def(1)"1/a.
+#m #l #Huni cases (a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"filter_eqb/a m l Huni) * #_ #H >H // 
+qed. 
+
+(***************************** split *******************************)
+img class="anchor" src="icons/tick.png" id="split_rev"let rec split_rev A (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) acc n on n ≝ 
+  match n with 
+  [O ⇒ 〈acc,la title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
+  |S m ⇒ match l with 
+    [nil ⇒ 〈acc,[a title="nil" href="cic:/fakeuri.def(1)"]/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
+    |cons a tl ⇒ split_rev A tl (a:a title="cons" href="cic:/fakeuri.def(1)":/aacc) m
+    ]
+  ].
+  
+img class="anchor" src="icons/tick.png" id="split"definition split ≝ λA,l,n.
+  let 〈l1,l2〉 ≝ a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a A l [a title="nil" href="cic:/fakeuri.def(1)"]/a n in 〈a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ? l1,l2a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a.
+
+img class="anchor" src="icons/tick.png" id="split_rev_len"lemma split_rev_len: ∀A,n,l,acc. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |la title="list length" href="cic:/fakeuri.def(1)"|/a →
+  |a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a A l acc n)a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/a|acca title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #n elim n // #m #Hind *
+  [normalize #acc #Hfalse @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+  |#a #tl #acc #Hlen normalize >Hind 
+    [normalize // |@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a //]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="split_len"lemma split_len: ∀A,n,l. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |la title="list length" href="cic:/fakeuri.def(1)"|/a →
+  |a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/basics/lists/search/split.def(3)"split/a A l n)a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+#A #n #l #Hlen normalize >(a href="cic:/matita/basics/types/eq_pair_fst_snd.def(2)"eq_pair_fst_snd/a ?? (a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a …))
+normalize >a href="cic:/matita/basics/lists/length/length_reverse.def(7)"length_reverse/a  >(a href="cic:/matita/basics/lists/search/split_rev_len.def(6)"split_rev_len/a … [ a title="nil" href="cic:/fakeuri.def(1)"]/a Hlen) normalize //
+qed.
+  
+img class="anchor" src="icons/tick.png" id="split_rev_eq"lemma split_rev_eq: ∀A,n,l,acc. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |la title="list length" href="cic:/fakeuri.def(1)"|/a → 
+  a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ? acca title="append" href="cic:/fakeuri.def(1)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ? (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a A l acc n))a title="append" href="cic:/fakeuri.def(1)"@/a(a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a A l acc n)).
+ #A #n elim n //
+ #m #Hind * 
+   [#acc whd in ⊢ ((??%)→?); #False_ind /span class="autotactic"2span class="autotrace" trace /span/span/ 
+   |#a #tl #acc #Hlen >a href="cic:/matita/basics/lists/append/append_cons.def(5)"append_cons/a <a href="cic:/matita/basics/lists/reverse/reverse_single.def(3)"reverse_single/a <a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a 
+    @(Hind tl) @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @Hlen
+   ]
+qed.
+ 
+img class="anchor" src="icons/tick.png" id="split_eq"lemma split_eq: ∀A,n,l. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |la title="list length" href="cic:/fakeuri.def(1)"|/a → 
+  l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/basics/lists/search/split.def(3)"split/a A l n))a title="append" href="cic:/fakeuri.def(1)"@/a(a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/basics/lists/search/split.def(3)"split/a A l n)).
+#A #n #l #Hlen change with ((a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ? [ a title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al) in ⊢ (??%?);
+>(a href="cic:/matita/basics/lists/search/split_rev_eq.def(8)"split_rev_eq/a … Hlen) normalize 
+>(a href="cic:/matita/basics/types/eq_pair_fst_snd.def(2)"eq_pair_fst_snd/a ?? (a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"split_rev/a A l [a title="nil" href="cic:/fakeuri.def(1)"]/a n)) %
+qed.
+
+img class="anchor" src="icons/tick.png" id="split_exists"lemma split_exists: ∀A,n.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |la title="list length" href="cic:/fakeuri.def(1)"|/a → 
+  a title="exists" href="cic:/fakeuri.def(1)"∃/al1,l2a title="exists" href="cic:/fakeuri.def(1)"./a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="logical and" href="cic:/fakeuri.def(1)"∧/a |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+#A #n #l #Hlen @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/basics/lists/search/split.def(3)"split/a A l n)))
+@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/basics/lists/search/split.def(3)"split/a A l n))) % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/lists/search/split_len.def(8)"split_len/a, a href="cic:/matita/basics/lists/search/split_eq.def(9)"split_eq/a/span/span/
+qed.
+  
+(****************************** flatten ******************************)
+img class="anchor" src="icons/tick.png" id="flatten"definition flatten ≝ λA.a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"foldr/a (a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A) [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+
+img class="anchor" src="icons/tick.png" id="flatten_to_mem"lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n →
+  (∀x. a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? x l → |xa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n) → |aa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → a href="cic:/matita/basics/lists/search/flatten.def(2)"flatten/a ? l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1a title="append" href="cic:/fakeuri.def(1)"@/aaa title="append" href="cic:/fakeuri.def(1)"@/al2  →
+    (a title="exists" href="cic:/fakeuri.def(1)"∃/aq.|l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aq)  → a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"mem/a ? a l.
+#A #n #l elim l
+  [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+   cut (|aa title="list length" href="cic:/fakeuri.def(1)"|/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="natural number" href="cic:/fakeuri.def(1)"0/a) [@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/nat/le_n_O_to_eq.def(4)"le_n_O_to_eq/a 
+   @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (|a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a Aa title="list length" href="cic:/fakeuri.def(1)"|/a)) // >Hnil >a href="cic:/matita/basics/lists/length/length_append.def(2)"length_append/a >a href="cic:/matita/basics/lists/length/length_append.def(2)"length_append/a //] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+  |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha 
+   whd in match (a href="cic:/matita/basics/lists/search/flatten.def(2)"flatten/a A (hd:a title="cons" href="cic:/fakeuri.def(1)":/atl)); #Hflat * #q cases q
+    [<a href="cic:/matita/arithmetics/nat/times_n_O.def(4)"times_n_O/a #Hl1 
+     cut (a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a hd) [>(a href="cic:/matita/basics/lists/length/lenght_to_nil.def(3)"lenght_to_nil/a… Hl1) in Hflat; 
+     whd in ⊢ ((???%)→?); #Hflat @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @(a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"append_l1_injective/a … Hflat)
+     >Ha >Hlen // %1 //   
+     ] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/
+    |#q1 #Hl1 lapply (a href="cic:/matita/basics/lists/search/split_exists.def(10)"split_exists/a … n l1 ?) //
+     * #l11 * #l12 * #Heql1 #Hlenl11 %2
+     @(Hind l12 l2 … posn ? Ha) 
+      [#x #memx @Hlen %2 //
+      |@(a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"append_l2_injective/a ? hd l11) 
+        [>Hlenl11 @Hlen %1 %
+        |>Hflat >Heql1 >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a %
+        ]
+      |@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a …q1) @(a href="cic:/matita/arithmetics/nat/injective_plus_r.def(5)"injective_plus_r/a n) 
+       <Hlenl11 in ⊢ (??%?); <a href="cic:/matita/basics/lists/length/length_append.def(2)"length_append/a <Heql1 >Hl1 //
+      ]
+    ]
+  ]
+qed.
+
+(****************************** nth ********************************)
+img class="anchor" src="icons/tick.png" id="nth"let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (d:A)  ≝  
+  match n with
+    [O ⇒ a href="cic:/matita/basics/lists/lists/hd.def(1)"hd/a A l d
+    |S m ⇒ nth m A (a href="cic:/matita/basics/lists/lists/tail.def(1)"tail/a A l) d].
+
+img class="anchor" src="icons/tick.png" id="nth_nil"lemma nth_nil: ∀A,a,i. a href="cic:/matita/basics/lists/search/nth.fix(0,0,2)"nth/a i A ([a title="nil" href="cic:/fakeuri.def(1)"]/a) a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
+#A #a #i elim i normalize //
+qed.
+