weblib/basics/lists/search.ma

   1 include "basics/lists/length.ma".
   2 include "basics/types.ma".
   3
   4 (****************************** mem ********************************)
   5 \ 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 ≝
   6   match l with
   7   [ nil ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6
   8   | 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
   9   ].
  10
  11 \ 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) →
  12   \ 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.
  13 #A #a #l1 elim l1
  14   [#l2 #mema %2 @mema
  15   |#b #tl #Hind #l2 *
  16     [#eqab %1 %1 @eqab
  17     |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
  18     ]
  19   ]
  20 qed.
  21
  22 \ 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).
  23 #A #a #l1 #l2 elim l1
  24   [whd in ⊢ (%→?); @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
  25   |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
  26   ]
  27 qed.
  28
  29 \ 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).
  30 #A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
  31 qed.
  32
  33 \ 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.
  34 #A #a #b * // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
  35 qed.
  36
  37 \ 5img class="anchor" src="icons/tick.png" id="mem_map"\ 6lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
  38   \ 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.
  39 #A #B #f #l elim l
  40   [#b normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
  41   |#a #tl #Hind #b normalize *
  42     [#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/
  43     |#memb cases (Hind … memb) #a * #mema #eqb
  44      @(\ 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/
  45     ]
  46   ]
  47 qed.
  48
  49 \ 5img class="anchor" src="icons/tick.png" id="mem_map_forward"\ 6lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
  50   \ 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).
  51  #A #B #f #a #l elim l
  52   [normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
  53   |#b #tl #Hind *
  54     [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
  55   ]
  56 qed.
  57
  58 (****************************** fitler ******************************)
  59
  60 \ 5img class="anchor" src="icons/tick.png" id="filter"\ 6definition filter ≝
  61   λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
  62   \ 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).
  63
  64 \ 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 →
  65   \ 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.
  66 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
  67
  68 \ 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 →
  69   \ 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.
  70 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
  71
  72 (****************************** mem filter ***************************)
  73 \ 5img class="anchor" src="icons/tick.png" id="mem_filter"\ 6lemma mem_filter: ∀S,f,a,l.
  74   \ 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.
  75 #S #f #a #l elim l [normalize //]
  76 #b #tl #Hind normalize (cases (f b)) normalize
  77   [* [#eqab %1 @eqab | #H %2 @Hind @H]
  78   |#H %2 @Hind @H]
  79 qed.
  80
  81 \ 5img class="anchor" src="icons/tick.png" id="mem_filter_true"\ 6lemma mem_filter_true: ∀S,f,a,l.
  82   \ 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.
  83 #S #f #a #l elim l [normalize @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 ]
  84 #b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #H
  85 normalize >H normalize [2:@Hind]
  86 * [#eqab // | @Hind]
  87 qed.
  88
  89 \ 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 →
  90 \ 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).
  91 #S #f #x #l #fx elim l [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6]
  92 #b #tl #Hind *
  93   [#eqxb <eqxb >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? fx) %1 %
  94   |#Htl cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #fb
  95     [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? fb) %2 @Hind @Htl
  96     |>(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 ???? fb) @Hind @Htl
  97     ]
  98   ]
  99 qed.
 100
 101 \ 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 →
 102   \ 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).
 103 #A #p #l elim l
 104   [#x @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
 105   |#a #tl #Hind #x *
 106     [#eqxa >eqxa cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
 107       [%1 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a p Hcase) %1 %
 108       |%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a ??) [%1 % | >Hcase %]
 109       ]
 110     |#memx cases (Hind … memx) -memx #memx
 111       [%1 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hpa
 112         [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a p Hpa) %2 @memx
 113         |>(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a p Hpa) @memx
 114         ]
 115       |cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
 116         [%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 A tl a) [@memx |>Hcase %]
 117         |%2 >(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 A tl a) [%2 @memx|>Hcase %]
 118         ]
 119       ]
 120     ]
 121   ]
 122 qed.
 123
 124 \ 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.
 125 #A #p #l elim l //
 126 #a #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #Hcase
 127   [>(\ 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 ??)
 128     [@(\ 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 %]
 129   |>(\ 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 ??)
 130     [<\ 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 %]
 131   ]
 132 qed.
 133
 134 (***************************** unique *******************************)
 135 \ 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 ≝
 136   match l with
 137   [nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6
 138   |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].
 139
 140 \ 5img class="anchor" src="icons/tick.png" id="unique_filter"\ 6lemma unique_filter : ∀S,l,f.
 141  \ 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).
 142 #S #l #f elim l //
 143 #a #tl #Hind *
 144 #memba #uniquetl cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (f a)) #Hfa
 145   [>(\ 5a href="cic:/matita/basics/lists/search/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 ???? Hfa) %
 146     [@(\ 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/ ]
 147   |>\ 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/
 148   ]
 149 qed.
 150
 151 \ 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 →
 152   (\ 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).
 153 #m #l elim l
 154   [#_ %2 % [% @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 | //]
 155   |#a #tl #Hind * #Hmema #Hunique
 156    cases (Hind Hunique)
 157     [* #Hmemm #Hind %1 % [%2 //]
 158      >\ 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) //
 159     |* #Hmemm #Hind cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_eq_nat.def(5)"\ 6decidable_eq_nat\ 5/a\ 6 m a) #eqma
 160       [%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 //
 161       |%2 %
 162         [@(\ 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) //
 163         |>\ 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
 164         ]
 165       ]
 166     ]
 167   ]
 168 qed.
 169
 170 \ 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 →
 171   |\ 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.
 172 #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 //
 173 qed.
 174
 175 (***************************** split *******************************)
 176 \ 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 ≝
 177   match n with
 178   [O ⇒ 〈acc,l\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
 179   |S m ⇒ match l with
 180     [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
 181     |cons a tl ⇒ split_rev A tl (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6acc) m
 182     ]
 183   ].
 184
 185 \ 5img class="anchor" src="icons/tick.png" id="split"\ 6definition split ≝ λA,l,n.
 186   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.
 187
 188 \ 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 →
 189   |\ 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.
 190 #A #n elim n // #m #Hind *
 191   [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/
 192   |#a #tl #acc #Hlen normalize >Hind
 193     [normalize // |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //]
 194   ]
 195 qed.
 196
 197 \ 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 →
 198   |\ 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.
 199 #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 …))
 200 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 //
 201 qed.
 202
 203 \ 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 →
 204   \ 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
 205     \ 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)).
 206  #A #n elim n //
 207  #m #Hind *
 208    [#acc whd in ⊢ ((??%)→?); #False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 209    |#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
 210     @(Hind tl) @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Hlen
 211    ]
 212 qed.
 213
 214 \ 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 →
 215   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)).
 216 #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 ⊢ (??%?);
 217 >(\ 5a href="cic:/matita/basics/lists/search/split_rev_eq.def(8)"\ 6split_rev_eq\ 5/a\ 6 … Hlen) normalize
 218 >(\ 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)) %
 219 qed.
 220
 221 \ 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 →
 222   \ 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.
 223 #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)))
 224 @(\ 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/
 225 qed.
 226
 227 (****************************** flatten ******************************)
 228 \ 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.
 229
 230 \ 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 →
 231   (∀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  →
 232     (\ 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.
 233 #A #n #l elim l
 234   [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
 235    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
 236    @(\ 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/
 237   |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
 238    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
 239     [<\ 5a href="cic:/matita/arithmetics/nat/times_n_O.def(4)"\ 6times_n_O\ 5/a\ 6 #Hl1
 240      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;
 241      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)
 242      >Ha >Hlen // %1 //
 243      ] /\ 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/
 244     |#q1 #Hl1 lapply (\ 5a href="cic:/matita/basics/lists/search/split_exists.def(10)"\ 6split_exists\ 5/a\ 6 … n l1 ?) //
 245      * #l11 * #l12 * #Heql1 #Hlenl11 %2
 246      @(Hind l12 l2 … posn ? Ha)
 247       [#x #memx @Hlen %2 //
 248       |@(\ 5a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"\ 6append_l2_injective\ 5/a\ 6 ? hd l11)
 249         [>Hlenl11 @Hlen %1 %
 250         |>Hflat >Heql1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 %
 251         ]
 252       |@(\ 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)
 253        <Hlenl11 in ⊢ (??%?); <\ 5a href="cic:/matita/basics/lists/length/length_append.def(2)"\ 6length_append\ 5/a\ 6 <Heql1 >Hl1 //
 254       ]
 255     ]
 256   ]
 257 qed.
 258
 259 (****************************** nth ********************************)
 260 \ 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)  ≝
 261   match n with
 262     [O ⇒ \ 5a href="cic:/matita/basics/lists/lists/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
 263     |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/lists/lists/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
 264
 265 \ 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.
 266 #A #a #i elim i normalize //
 267 qed.
 268