1 (**************************** length ******************************)
3 include "basics/lists/iterators.ma".
4 include "basics/lists/reverse.ma".
5 include "arithmetics/nat.ma".
7 \ 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 ≝
9 [ nil ⇒
\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6
10 | cons a tl ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (length A tl)].
12 interpretation "list length" 'card l = (length ? l).
14 \ 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).
18 \ 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.
22 \ 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.
23 |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.
24 #A #l1 elim l1 // normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
27 \ 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.
28 #A #B #l #f elim l // #a #tl #Hind normalize //
31 \ 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.
32 |
\ 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.
33 #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 //
36 \ 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.
37 |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.
38 #A * // #a #tl normalize #H destruct
41 \ 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
42 (|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).
44 [ #l2 %{[
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6]
\ 5/a
\ 6} %{l2} % % %
46 [ %{[
\ 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 % %
47 | #hd2 #tl2 cases (IH tl2) #x * #y *
48 [ * #IH1 #IH2 %{(hd2:
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6x)} %{y} % normalize % //
49 | * #IH1 #IH2 %{(hd1:
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6x)} %{y} %2 normalize % // ]
54 (****************** traversing two lists in parallel *****************)
55 \ 5img class="anchor" src="icons/tick.png" id="list_ind2"
\ 6lemma list_ind2 :
56 ∀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.
57 |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 →
58 (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) →
59 (∀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)) →
61 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
62 generalize in match Hl; generalize in match l2;
64 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
65 |#t1 #tl1 #IH #l2 cases l2
66 [normalize #H destruct
67 |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
71 \ 5img class="anchor" src="icons/tick.png" id="list_cases2"
\ 6lemma list_cases2 :
72 ∀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.
73 |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 →
74 (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) →
75 (∀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.
76 #T1 #T2 #l1 #l2 #P #Hl @(
\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"
\ 6list_ind2
\ 5/a
\ 6 … Hl)
77 [ #Pnil #Pcons @Pnil //
78 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
81 (*********************** properties of append ***********************)
82 \ 5img class="anchor" src="icons/tick.png" id="append_l1_injective"
\ 6lemma append_l1_injective :
83 ∀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.
84 #a #l1 #l2 #l3 #l4 #Hlen @(
\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"
\ 6list_ind2
\ 5/a
\ 6 … Hlen) //
85 #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/
88 \ 5img class="anchor" src="icons/tick.png" id="append_l2_injective"
\ 6lemma append_l2_injective :
89 ∀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.
90 #a #l1 #l2 #l3 #l4 #Hlen @(
\ 5a href="cic:/matita/basics/lists/length/list_ind2.def(3)"
\ 6list_ind2
\ 5/a
\ 6 … Hlen) normalize //
91 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
94 \ 5img class="anchor" src="icons/tick.png" id="append_l1_injective_r"
\ 6lemma append_l1_injective_r :
95 ∀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.
96 #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)
97 >
\ 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
98 lapply (
\ 5a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"
\ 6append_l2_injective
\ 5/a
\ 6 … Heq1) [ // ] #Heq2
99 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) //
102 \ 5img class="anchor" src="icons/tick.png" id="append_l2_injective_r"
\ 6lemma append_l2_injective_r :
103 ∀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.
104 #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)
105 >
\ 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
106 lapply (
\ 5a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"
\ 6append_l1_injective
\ 5/a
\ 6 … Heq1) [ // ] #Heq2
107 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) //
110 \ 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.
111 |
\ 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.
112 #A #l elim l // #a #tl #Hind normalize
113 #acc >Hind normalize //