commit by user andrea

diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
index 73fbd36cc5afb91e0021d333522efef89f069383..5b0c403e1b58ab707a31f7223ade3f8e61e1e384 100644 (file)
--- 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".
 
-\ 5img class="anchor" src="icons/tick.png" id="append"\ 6let rec append A (l1: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
+let rec append A (l1: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
   | cons hd tl ⇒  hd :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-\ 5img class="anchor" src="icons/tick.png" id="append_nil"\ 6theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
 #A #l (elim l) normalize // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append: 
- ∀A.\ 5font class="Apple-style-span" color="#FF0000"\ 6\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5/font\ 6(\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
+theorem associative_append: 
+ ∀A.\ 5font class="Apple-style-span" color="#ff0000"\ 6\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5/font\ 6(\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="append_cons"\ 6theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
+theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
 #A #a #l #l1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="nil_append_elim"\ 6theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
+theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="nil_to_nil"\ 6theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/lists/append/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (* comparing lists *)
 
-\ 5img class="anchor" src="icons/tick.png" id="compare_append"\ 6lemma compare_append : ∀A,l1,l2,l3,l4. l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → 
+lemma compare_append : ∀A,l1,l2,l3,l4. l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → 
 ∃l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6(l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l4\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4).
 #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 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. *)

diff --git a/weblib/basics/lists/length.ma b/weblib/basics/lists/length.ma
new file mode 100644 (file)
index 0000000..a347b10
--- /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".
+
+\ 5img class="anchor" src="icons/tick.png" id="length"\ 6let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
+  match l with 
+    [ nil ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6
+    | cons a tl ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
+
+interpretation "list length" 'card l = (length ? l).
+
+\ 5img class="anchor" src="icons/tick.png" id="length_tail"\ 6lemma length_tail: ∀A,l. |\ 5a href="cic:/matita/basics/lists/lists/tail.def(1)"\ 6tail\ 5/a\ 6 A l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (|l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6).
+#A #l elim l // 
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_tail1"\ 6lemma length_tail1 : ∀A,l.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → |\ 5a href="cic:/matita/basics/lists/lists/tail.def(1)"\ 6tail\ 5/a\ 6 A l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A * normalize //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_append"\ 6lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
+  |l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A #l1 elim l1 // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_map"\ 6lemma length_map: ∀A,B,l.∀f:A→B. |\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? f l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_reverse"\ 6lemma length_reverse: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
+  |\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 A l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A #l elim l // #a #l0 #IH >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/length/length_append.def(2)"\ 6length_append\ 5/a\ 6 >IH normalize //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="lenght_to_nil"\ 6lemma lenght_to_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 → l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#A * // #a #tl normalize #H destruct
+qed.
+ 
+\ 5img class="anchor" src="icons/tick.png" id="lists_length_split"\ 6lemma lists_length_split : ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6la,lb\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6
+  (|la\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 la\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6lb) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (|la\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 la\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6lb).
+#A #l1 elim l1
+[ #l2 %{[ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6} %{l2} % % %
+| #hd1 #tl1 #IH *
+  [ %{[ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6} %{(hd1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1)} %2 % %
+  | #hd2 #tl2 cases (IH tl2) #x * #y *
+    [ * #IH1 #IH2 %{(hd2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6x)} %{y} % normalize % //
+    | * #IH1 #IH2 %{(hd1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6x)} %{y} %2 normalize % // ]
+  ]
+]
+qed.
+
+(****************** traversing two lists in parallel *****************)
+\ 5img class="anchor" src="icons/tick.png" id="list_ind2"\ 6lemma list_ind2 : 
+  ∀T1,T2:Type[0].∀l1:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1.∀l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2.∀P:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1 → \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2 → Prop.
+  |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 →
+  (P [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1) (hd2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl2)) → 
+  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.
+
+\ 5img class="anchor" src="icons/tick.png" id="list_cases2"\ 6lemma list_cases2 : 
+  ∀T1,T2:Type[0].∀l1:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1.∀l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2.∀P:Prop.
+  |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 →
+  (l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P) → 
+  (∀hd1,hd2,tl1,tl2.l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 hd1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1 → l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 hd2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"\ 6list_ind2\ 5/a\ 6 … Hl)
+  [ #Pnil #Pcons @Pnil //
+  | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+\ 5img class="anchor" src="icons/tick.png" id="append_l1_injective"\ 6lemma append_l1_injective : 
+  ∀A.∀l1,l2,l3,l4:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"\ 6list_ind2\ 5/a\ 6 … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+  
+\ 5img class="anchor" src="icons/tick.png" id="append_l2_injective"\ 6lemma append_l2_injective : 
+  ∀A.∀l1,l2,l3,l4:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l2\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"\ 6list_ind2\ 5/a\ 6 … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="append_l1_injective_r"\ 6lemma append_l1_injective_r :
+  ∀A.∀l1,l2,l3,l4:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. |l3\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l4\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ?) … Heq)
+>\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 #Heq1
+lapply (\ 5a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"\ 6append_l2_injective\ 5/a\ 6 … Heq1) [ // ] #Heq2
+lapply (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ?) … Heq2) //
+qed.
+  
+\ 5img class="anchor" src="icons/tick.png" id="append_l2_injective_r"\ 6lemma append_l2_injective_r : 
+  ∀A.∀l1,l2,l3,l4:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. |l3\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l4\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ?) … Heq)
+>\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 #Heq1
+lapply (\ 5a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"\ 6append_l1_injective\ 5/a\ 6 … Heq1) [ // ] #Heq2
+lapply (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ?) … Heq2) //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_rev_append"\ 6lemma length_rev_append: ∀A.∀l,acc:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
+  |\ 5a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 ? l acc\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|acc\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#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 (file)
index 0000000..20a0110
--- /dev/null
+++ b/weblib/basics/lists/reverse.ma
@@ -0,0 +1,43 @@
+(**************************** reverse *****************************)
+
+include "basics/lists/iterators.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="rev_append"\ 6let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2)
+  ]
+.
+
+\ 5img class="anchor" src="icons/tick.png" id="reverse"\ 6definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+
+\ 5img class="anchor" src="icons/tick.png" id="reverse_single"\ 6lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6. 
+// qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="rev_append_def"\ 6lemma rev_append_def : ∀S,l1,l2. 
+  \ 5a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l1 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2 .
+#S #l1 elim l1 normalize 
+  [// | #a #tl #Hind #l2 >Hind >(Hind \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="reverse_cons"\ 6lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="reverse_append"\ 6lemma reverse_append: ∀S,l1,l2. 
+  \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (l1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6
+>\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 >Hind // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="reverse_reverse"\ 6lemma reverse_reverse : ∀S,l. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#S #l elim l // #a #tl #Hind >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 >Hind %
+qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+\ 5img class="anchor" src="icons/tick.png" id="list_elim_left"\ 6lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
+(∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/lists/reverse/reverse_reverse.def(8)"\ 6reverse_reverse\ 5/a\ 6 … l) 
+generalize in match (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
+#a #tl #H >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 @Pstep //
+qed.

diff --git a/weblib/basics/lists/search.ma b/weblib/basics/lists/search.ma
new file mode 100644 (file)
index 0000000..77bfa10
--- /dev/null
+++ b/weblib/basics/lists/search.ma
@@ -0,0 +1,268 @@
+include "basics/lists/length.ma".
+include "basics/types.ma".
+
+(****************************** mem ********************************)
+\ 5img class="anchor" src="icons/tick.png" id="mem"\ 6let rec mem A (a:A) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
+  match l with
+  [ nil ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6
+  | cons hd tl ⇒ a\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6hd \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 mem A a tl
+  ]. 
+  
+\ 5img class="anchor" src="icons/tick.png" id="mem_append"\ 6lemma mem_append: ∀A,a,l1,l2.\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) →
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? a l1 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? 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.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_append_l1"\ 6lemma mem_append_l1: ∀A,a,l1,l2.\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a l1 → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
+#A #a #l1 #l2 elim l1
+  [whd in ⊢ (%→?); @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+  |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_append_l2"\ 6lemma mem_append_l2: ∀A,a,l1,l2.\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a l2 → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
+#A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_single"\ 6lemma mem_single: ∀A,a,b. \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6b\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → a\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b.
+#A #a #b * // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_map"\ 6lemma mem_map: ∀A,B.∀f:A→B.∀l,b. 
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? b (\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 … f l) → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6a. \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? a l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
+#A #B #f #l elim l 
+  [#b normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+  |#a #tl #Hind #b normalize *
+    [#eqb @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … a) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+    |#memb cases (Hind … memb) #a * #mema #eqb
+     @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … a) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+    ]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_map_forward"\ 6lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l. 
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a l → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 B (f a) (\ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? f l).
+ #A #B #f #a #l elim l
+  [normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+  |#b #tl #Hind * 
+    [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+  ]
+qed.
+
+(****************************** fitler ******************************)
+
+\ 5img class="anchor" src="icons/tick.png" id="filter"\ 6definition filter ≝ 
+  λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+  \ 5a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.if p x then x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l0 else l0) (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
+
+\ 5img class="anchor" src="icons/tick.png" id="filter_true"\ 6lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="filter_false"\ 6lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+(****************************** mem filter ***************************)
+\ 5img class="anchor" src="icons/tick.png" id="mem_filter"\ 6lemma mem_filter: ∀S,f,a,l. 
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 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.
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_filter_true"\ 6lemma mem_filter_true: ∀S,f,a,l. 
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 S f l)  → f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#S #f #a #l elim l [normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 ]
+#b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #H
+normalize >H normalize [2:@Hind]
+* [#eqab // | @Hind]
+qed. 
+
+\ 5img class="anchor" src="icons/tick.png" id="mem_filter_l"\ 6lemma mem_filter_l: ∀S,f,x,l. (f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 S x l →
+\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 S x (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? f l).
+#S #f #x #l #fx elim l [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6]
+#b #tl #Hind * 
+  [#eqxb <eqxb >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? fx) %1 % 
+  |#Htl cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #fb 
+    [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? fb) %2 @Hind @Htl
+    |>(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 ???? fb) @Hind @Htl
+    ]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="filter_case"\ 6lemma filter_case: ∀A,p,l,x. \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? x l → 
+  \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? x (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p l) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? x (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A (λx.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 p x) l).
+#A #p #l elim l 
+  [#x @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 
+  |#a #tl #Hind #x * 
+    [#eqxa >eqxa cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
+      [%1 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a p Hcase) %1 % 
+      |%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a ??) [%1 % | >Hcase %]
+      ]
+    |#memx cases (Hind … memx) -memx #memx
+      [%1 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hpa 
+        [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a p Hpa) %2 @memx
+        |>(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a p Hpa) @memx
+        ]
+      |cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
+        [%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a) [@memx |>Hcase %]
+        |%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a) [%2 @memx|>Hcase %]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="filter_length2"\ 6lemma filter_length2: ∀A,p,l. |\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A p l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 A (λx.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 p x) l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A #p #l elim l //
+#a #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
+  [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a p Hcase) >(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a ??) 
+    [@(\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 ?? \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6) @Hind | >Hcase %]
+  |>(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a p Hcase) >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a ??) 
+    [<\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 ?? \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6) @Hind | >Hcase %]
+  ]
+qed.
+
+(***************************** unique *******************************)
+\ 5img class="anchor" src="icons/tick.png" id="unique"\ 6let rec unique A (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
+  match l with 
+  [nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6
+  |cons a tl ⇒ \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 A a tl \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 unique A tl].
+
+\ 5img class="anchor" src="icons/tick.png" id="unique_filter"\ 6lemma unique_filter : ∀S,l,f.
+ \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 S l → \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 S f l).
+#S #l #f elim l //
+#a #tl #Hind * 
+#memba #uniquetl cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (f a)) #Hfa
+  [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? Hfa) % 
+    [@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … memba) @\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ ]
+  |>\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="filter_eqb"\ 6lemma filter_eqb : ∀m,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → 
+  (\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? m l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6m\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6(\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6\ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? m l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
+#m #l elim l
+  [#_ %2 % [% @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 | //]
+  |#a #tl #Hind * #Hmema #Hunique
+   cases (Hind Hunique)
+    [* #Hmemm #Hind %1 % [%2 //]
+     >\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 % #eqma @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ? Hmemm) //
+    |* #Hmemm #Hind cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_eq_nat.def(5)"\ 6decidable_eq_nat\ 5/a\ 6 m a) #eqma 
+      [%1 <eqma % [%1 //] >\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 [2: @\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6 //] >Hind //
+      |%2 % 
+        [@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … Hmemm) * // #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6  @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … H) //
+        |>\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 @eqma
+        ]
+      ]
+    ]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="length_filter_eqb"\ 6lemma length_filter_eqb: ∀m,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → 
+  |\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
+#m #l #Huni cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m l Huni) * #_ #H >H // 
+qed. 
+
+(***************************** split *******************************)
+\ 5img class="anchor" src="icons/tick.png" id="split_rev"\ 6let rec split_rev A (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) acc n on n ≝ 
+  match n with 
+  [O ⇒ 〈acc,l\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+  |S m ⇒ match l with 
+    [nil ⇒ 〈acc,[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+    |cons a tl ⇒ split_rev A tl (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6acc) m
+    ]
+  ].
+  
+\ 5img class="anchor" src="icons/tick.png" id="split"\ 6definition split ≝ λA,l,n.
+  let 〈l1,l2〉 ≝ \ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 A l [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 n in 〈\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ? l1,l2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
+
+\ 5img class="anchor" src="icons/tick.png" id="split_rev_len"\ 6lemma split_rev_len: ∀A,n,l,acc. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 →
+  |\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 A l acc n)\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|acc\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#A #n elim n // #m #Hind *
+  [normalize #acc #Hfalse @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |#a #tl #acc #Hlen normalize >Hind 
+    [normalize // |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="split_len"\ 6lemma split_len: ∀A,n,l. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 →
+  |\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split.def(3)"\ 6split\ 5/a\ 6 A l n)\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+#A #n #l #Hlen normalize >(\ 5a href="cic:/matita/basics/types/eq_pair_fst_snd.def(2)"\ 6eq_pair_fst_snd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 …))
+normalize >\ 5a href="cic:/matita/basics/lists/length/length_reverse.def(7)"\ 6length_reverse\ 5/a\ 6  >(\ 5a href="cic:/matita/basics/lists/search/split_rev_len.def(6)"\ 6split_rev_len\ 5/a\ 6 … [ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 Hlen) normalize //
+qed.
+  
+\ 5img class="anchor" src="icons/tick.png" id="split_rev_eq"\ 6lemma split_rev_eq: ∀A,n,l,acc. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ? acc\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ? (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 A l acc n))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 A l acc n)).
+ #A #n elim n //
+ #m #Hind * 
+   [#acc whd in ⊢ ((??%)→?); #False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
+   |#a #tl #acc #Hlen >\ 5a href="cic:/matita/basics/lists/append/append_cons.def(5)"\ 6append_cons\ 5/a\ 6 <\ 5a href="cic:/matita/basics/lists/reverse/reverse_single.def(3)"\ 6reverse_single\ 5/a\ 6 <\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 
+    @(Hind tl) @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Hlen
+   ]
+qed.
+ 
+\ 5img class="anchor" src="icons/tick.png" id="split_eq"\ 6lemma split_eq: ∀A,n,l. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → 
+  l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split.def(3)"\ 6split\ 5/a\ 6 A l n))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split.def(3)"\ 6split\ 5/a\ 6 A l n)).
+#A #n #l #Hlen change with ((\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 ? [ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l) in ⊢ (??%?);
+>(\ 5a href="cic:/matita/basics/lists/search/split_rev_eq.def(8)"\ 6split_rev_eq\ 5/a\ 6 … Hlen) normalize 
+>(\ 5a href="cic:/matita/basics/types/eq_pair_fst_snd.def(2)"\ 6eq_pair_fst_snd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/basics/lists/search/split_rev.fix(0,3,1)"\ 6split_rev\ 5/a\ 6 A l [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 n)) %
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="split_exists"\ 6lemma split_exists: ∀A,n.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → 
+  \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l1,l2\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 |l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+#A #n #l #Hlen @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split.def(3)"\ 6split\ 5/a\ 6 A l n)))
+@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/search/split.def(3)"\ 6split\ 5/a\ 6 A l n))) % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/lists/search/split_len.def(8)"\ 6split_len\ 5/a\ 6, \ 5a href="cic:/matita/basics/lists/search/split_eq.def(9)"\ 6split_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+  
+(****************************** flatten ******************************)
+\ 5img class="anchor" src="icons/tick.png" id="flatten"\ 6definition flatten ≝ λA.\ 5a href="cic:/matita/basics/lists/iterators/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A) [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+
+\ 5img class="anchor" src="icons/tick.png" id="flatten_to_mem"\ 6lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
+  (∀x. \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? x l → |x\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n) → |a\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/lists/search/flatten.def(2)"\ 6flatten\ 5/a\ 6 ? l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6a\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2  →
+    (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6q.|l1\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q)  → \ 5a href="cic:/matita/basics/lists/search/mem.fix(0,2,1)"\ 6mem\ 5/a\ 6 ? a l.
+#A #n #l elim l
+  [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+   cut (|a\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) [@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_n_O_to_eq.def(4)"\ 6le_n_O_to_eq\ 5/a\ 6 
+   @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (|\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) // >Hnil >\ 5a href="cic:/matita/basics/lists/length/length_append.def(2)"\ 6length_append\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/length/length_append.def(2)"\ 6length_append\ 5/a\ 6 //] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha 
+   whd in match (\ 5a href="cic:/matita/basics/lists/search/flatten.def(2)"\ 6flatten\ 5/a\ 6 A (hd:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl)); #Hflat * #q cases q
+    [<\ 5a href="cic:/matita/arithmetics/nat/times_n_O.def(4)"\ 6times_n_O\ 5/a\ 6 #Hl1 
+     cut (a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 hd) [>(\ 5a href="cic:/matita/basics/lists/length/lenght_to_nil.def(3)"\ 6lenght_to_nil\ 5/a\ 6… Hl1) in Hflat; 
+     whd in ⊢ ((???%)→?); #Hflat @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"\ 6append_l1_injective\ 5/a\ 6 … Hflat)
+     >Ha >Hlen // %1 //   
+     ] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+    |#q1 #Hl1 lapply (\ 5a href="cic:/matita/basics/lists/search/split_exists.def(10)"\ 6split_exists\ 5/a\ 6 … n l1 ?) //
+     * #l11 * #l12 * #Heql1 #Hlenl11 %2
+     @(Hind l12 l2 … posn ? Ha) 
+      [#x #memx @Hlen %2 //
+      |@(\ 5a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"\ 6append_l2_injective\ 5/a\ 6 ? hd l11) 
+        [>Hlenl11 @Hlen %1 %
+        |>Hflat >Heql1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 %
+        ]
+      |@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 …q1) @(\ 5a href="cic:/matita/arithmetics/nat/injective_plus_r.def(5)"\ 6injective_plus_r\ 5/a\ 6 n) 
+       <Hlenl11 in ⊢ (??%?); <\ 5a href="cic:/matita/basics/lists/length/length_append.def(2)"\ 6length_append\ 5/a\ 6 <Heql1 >Hl1 //
+      ]
+    ]
+  ]
+qed.
+
+(****************************** nth ********************************)
+\ 5img class="anchor" src="icons/tick.png" id="nth"\ 6let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
+  match n with
+    [O ⇒ \ 5a href="cic:/matita/basics/lists/lists/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
+    |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/lists/lists/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
+
+\ 5img class="anchor" src="icons/tick.png" id="nth_nil"\ 6lemma nth_nil: ∀A,a,i. \ 5a href="cic:/matita/basics/lists/search/nth.fix(0,0,2)"\ 6nth\ 5/a\ 6 i A ([\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+#A #a #i elim i normalize //
+qed.
+