weblib/basics/list.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 inductive list (A:Type[0]) : Type[0] :=
  15   | nil: list A
  16   | cons: A -> list A -> list A.
  17
  18 notation "hvbox(hd break :: tl)"
  19   right associative with precedence 47
  20   for @{'cons $hd $tl}.
  21
  22 notation "ref 'cons [ list0 x sep ; ref 'nil ]"
  23   non associative with precedence 90
  24   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  25
  26 notation "hvbox(l1 break @ l2)"
  27   right associative with precedence 47
  28   for @{'append $l1 $l2 }.
  29
  30 interpretation "nil" 'nil = (nil ?).
  31 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  32
  33 definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
  34  λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
  35
  36 theorem nil_cons:
  37   ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  38   #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))) >Heq //
  39 qed.
  40
  41 (*
  42 let rec id_list A (l: list A) on l :=
  43   match l with
  44   [ nil => []
  45   | (cons hd tl) => hd :: id_list A tl ]. *)
  46
  47 let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
  48   match l1 with
  49   [ nil ⇒  l2
  50   | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
  51
  52 definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
  53   match l with [ nil ⇒ d | cons a _ ⇒ a].
  54
  55 definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  56   match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒  tl].
  57
  58 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  59
  60 theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
  61 #A #l (elim l) normalize // qed.
  62
  63 theorem associative_append:
  64  ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
  65 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  66
  67 (* deleterio per auto
  68 ntheorem cons_append_commute:
  69   ∀A:Type.∀l1,l2:list A.∀a:A.
  70     a :: (l1 @ l2) = (a :: l1) @ l2.
  71 //; nqed. *)
  72
  73 theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 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\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
  74 #A #a #l1 #l2 >\ 5a href="cic:/matita/basics/list/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
  75
  76 theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop.
  77   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 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\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
  78 #A #l1 #l2 #P (cases l1) normalize //
  79 #a #l3 #heq destruct
  80 qed.
  81
  82 theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  83   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 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\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → 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\ 5a title="nil" 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 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  84 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  85 qed.
  86
  87 (* iterators *)
  88
  89 let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
  90  match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 (map A B f tl)].
  91
  92 lemma map_append : ∀A,B,f,l1,l2.
  93   (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
  94 #A #B #f #l1 elim l1
  95 [ #l2 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6
  96 | #h #t #IH #l2 normalize //
  97 ] qed.
  98
  99 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
 100  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
 101
 102 definition filter ≝
 103   λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
 104   \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/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\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l0) else l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
 105
 106 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
 107     \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 l1.
 108
 109 lemma 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 →
 110   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 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 title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 111 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 112
 113 lemma 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 →
 114   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 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/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 115 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 116
 117 theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 118 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 119
 120 (*
 121 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 122 match l1 with
 123   [ nil ⇒ nil ?
 124   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
 125   ]. *)
 126
 127 (**************************** reverse *****************************)
 128 let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
 129   match l1 with
 130   [ nil ⇒ l2
 131   | cons a tl ⇒ rev_append S tl (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2)
 132   ]
 133 .
 134
 135 definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
 136
 137 lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 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 title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
 138 // qed.
 139
 140 lemma rev_append_def : ∀S,l1,l2.
 141   \ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l1 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2 .
 142 #S #l1 elim l1 normalize //
 143 qed.
 144
 145 lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 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/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
 146 #S #a #l whd in ⊢ (??%?); //
 147 qed.
 148
 149 lemma reverse_append: ∀S,l1,l2.
 150   \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (l1 \ 5a title="append" 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 href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1).
 151 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6
 152 >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 // qed.
 153
 154 lemma reverse_reverse : ∀S,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
 155 #S #l elim l // #a #tl #Hind >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 >\ 5a href="cic:/matita/basics/list/reverse_append.def(8)"\ 6reverse_append\ 5/a\ 6
 156 normalize // qed.
 157
 158 (* an elimination principle for lists working on the tail;
 159 useful for strings *)
 160 lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
 161 (∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))) → ∀l. P l.
 162 #S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/list/reverse_reverse.def(9)"\ 6reverse_reverse\ 5/a\ 6 … l)
 163 generalize in match (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
 164 #a #tl #H >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 @Pstep //
 165 qed.
 166
 167 (**************************** length *******************************)
 168
 169 let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
 170   match l with
 171     [ nil ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6
 172     | cons a tl ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
 173
 174 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 175 interpretation "norm" 'norm l = (length ? l).
 176
 177 lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 178   \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="norm" 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="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 179 #A #l1 elim l1 // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 180 qed.
 181
 182 let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝
 183   match n with
 184     [O ⇒ \ 5a href="cic:/matita/basics/list/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
 185     |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/list/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
 186
 187 (***************************** fold *******************************)
 188
 189 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
 190  match l with
 191   [ nil ⇒ b
 192   | cons a l ⇒ if (p a) then (op (f a) (fold A B op b p f l))
 193       else (fold A B op b p f l)
 194   ].
 195
 196 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 197   with precedence 80
 198 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 199
 200 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 201   with precedence 80
 202 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 203
 204 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 205
 206 theorem fold_true:
 207 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. 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 →
 208   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 209     op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 210 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 211
 212 theorem fold_false:
 213 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 214 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 title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 215   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 216 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 217
 218 theorem fold_filter:
 219 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 220   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 221     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 222 #A #B #a #l #p #op #nil #f elim l //
 223 #a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa
 224   [ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
 225   | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
 226 qed.
 227
 228 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 229   {op :2> A → A → A;
 230    nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 231    nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 232    assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
 233   }.
 234
 235 theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
 236   op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 237     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 238 #A #B #I #J #nil #op #f (elim I) normalize
 239   [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
 240 qed.