--- /dev/null
+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.
+
projects / helm.git / blobdiff