weblib/basics/lists/length.ma

   1 (**************************** length ******************************)
   2
   3 include "basics/lists/iterators.ma".
   4 include "basics/lists/reverse.ma".
   5 include "arithmetics/nat.ma".
   6
   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 ≝
   8   match l with
   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)].
  11
  12 interpretation "list length" 'card l = (length ? l).
  13
  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).
  15 #A #l elim l //
  16 qed.
  17
  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.
  19 #A * normalize //
  20 qed.
  21
  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/
  25 qed.
  26
  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 //
  29 qed.
  30
  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 //
  34 qed.
  35
  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
  39 qed.
  40
  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).
  43 #A #l1 elim l1
  44 [ #l2 %{[ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6} %{l2} % % %
  45 | #hd1 #tl1 #IH *
  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 % // ]
  50   ]
  51 ]
  52 qed.
  53
  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)) →
  60   P l1 l2.
  61 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
  62 generalize in match Hl; generalize in match l2;
  63 elim l1
  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 // ]
  68   ]
  69 qed.
  70
  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 // ]
  79 qed.
  80
  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/
  86 qed.
  87
  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/
  92 qed.
  93
  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) //
 100 qed.
 101
 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) //
 108 qed.
 109
 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 //
 114 qed.
 115