1 include "basics/lists/length.ma".
2 include "basics/types.ma".
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 ≝
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
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.
17 |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
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).
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 //]
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 //]
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
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.
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/
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).
52 [normalize @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6
54 [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
58 (****************************** fitler ******************************)
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).
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.
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.
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]
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]
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]
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
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).
104 [#x @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6
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 %]
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
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 %]
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.
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 %]
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 ≝
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].
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).
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/
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).
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
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 //
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
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 //
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 ≝
178 [O ⇒ 〈acc,l
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6
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
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.
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 //]
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 //
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)).
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
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)) %
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/
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.
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.
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)
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)
250 |>Hflat >Heql1 >
\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"
\ 6associative_append
\ 5/a
\ 6 %
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 //
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) ≝
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].
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 //