matita/matita/lib/basics/lists/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 "basics/types.ma".
  13 include "arithmetics/nat.ma".
  14
  15 inductive list (A:Type[0]) : Type[0] :=
  16   | nil: list A
  17   | cons: A -> list A -> list A.
  18
  19 notation "hvbox(hd break :: tl)"
  20   right associative with precedence 47
  21   for @{'cons $hd $tl}.
  22
  23 notation "[ list0 term 19 x sep ; ]"
  24   non associative with precedence 90
  25   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  26
  27 notation "hvbox(l1 break @ l2)"
  28   right associative with precedence 47
  29   for @{'append $l1 $l2 }.
  30
  31 interpretation "nil" 'nil = (nil ?).
  32 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  33
  34 definition is_nil: ∀A:Type[0].list A → Prop ≝
  35  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
  36
  37 theorem nil_cons:
  38   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
  39   #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
  40 qed.
  41
  42 (*
  43 let rec id_list A (l: list A) on l :=
  44   match l with
  45   [ nil => []
  46   | (cons hd tl) => hd :: id_list A tl ]. *)
  47
  48 let rec append A (l1: list A) l2 on l1 ≝
  49   match l1 with
  50   [ nil ⇒  l2
  51   | cons hd tl ⇒  hd :: append A tl l2 ].
  52
  53 definition hd ≝ λA.λl: list A.λd:A.
  54   match l with [ nil ⇒ d | cons a _ ⇒ a].
  55
  56 definition tail ≝  λA.λl: list A.
  57   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
  58
  59 definition option_hd ≝
  60   λA.λl:list A. match l with
  61   [ nil ⇒ None ?
  62   | cons a _ ⇒ Some ? a ].
  63
  64 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  65
  66 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
  67 #A #l (elim l) normalize // qed.
  68
  69 theorem associative_append:
  70  ∀A.associative (list A) (append A).
  71 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  72
  73 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
  74 #A #a #l #l1 >associative_append // qed.
  75
  76 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
  77   l1@l2=[] → P (nil A) (nil 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:list A.
  83   l1@l2 = [] → l1 = [] ∧ l2 = [].
  84 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
  85 qed.
  86
  87 lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
  88 #A #a1 #a2 #l1 #l2 #Heq destruct //
  89 qed.
  90
  91 lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
  92 #A #a1 #a2 #l1 #l2 #Heq destruct //
  93 qed.
  94
  95 (**************************** iterators ******************************)
  96
  97 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
  98  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
  99
 100 lemma map_append : ∀A,B,f,l1,l2.
 101   (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
 102 #A #B #f #l1 elim l1
 103 [ #l2 @refl
 104 | #h #t #IH #l2 normalize //
 105 ] qed.
 106
 107 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
 108  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
 109
 110 definition filter ≝
 111   λT.λp:T → bool.
 112   foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
 113
 114 (* compose f [a1;...;an] [b1;...;bm] =
 115   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
 116
 117 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
 118     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
 119
 120 lemma filter_true : ∀A,l,a,p. p a = true →
 121   filter A p (a::l) = a :: filter A p l.
 122 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 123
 124 lemma filter_false : ∀A,l,a,p. p a = false →
 125   filter A p (a::l) = filter A p l.
 126 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 127
 128 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 129 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 130
 131 (**************************** reverse *****************************)
 132 let rec rev_append S (l1,l2:list S) on l1 ≝
 133   match l1 with
 134   [ nil ⇒ l2
 135   | cons a tl ⇒ rev_append S tl (a::l2)
 136   ]
 137 .
 138
 139 definition reverse ≝λS.λl.rev_append S l [].
 140
 141 lemma reverse_single : ∀S,a. reverse S [a] = [a].
 142 // qed.
 143
 144 lemma rev_append_def : ∀S,l1,l2.
 145   rev_append S l1 l2 = (reverse S l1) @ l2 .
 146 #S #l1 elim l1 normalize //
 147 qed.
 148
 149 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
 150 #S #a #l whd in ⊢ (??%?); //
 151 qed.
 152
 153 lemma reverse_append: ∀S,l1,l2.
 154   reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
 155 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
 156 >reverse_cons // qed.
 157
 158 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
 159 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
 160 normalize // qed.
 161
 162 (* an elimination principle for lists working on the tail;
 163 useful for strings *)
 164 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
 165 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
 166 #S #P #Pnil #Pstep #l <(reverse_reverse … l)
 167 generalize in match (reverse S l); #l elim l //
 168 #a #tl #H >reverse_cons @Pstep //
 169 qed.
 170
 171 (**************************** length ******************************)
 172
 173 let rec length (A:Type[0]) (l:list A) on l ≝
 174   match l with
 175     [ nil ⇒ 0
 176     | cons a tl ⇒ S (length A tl)].
 177
 178 interpretation "list length" 'card l = (length ? l).
 179
 180 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 181 #A #l elim l //
 182 qed.
 183
 184 lemma length_append: ∀A.∀l1,l2:list A.
 185   |l1@l2| = |l1|+|l2|.
 186 #A #l1 elim l1 // normalize /2/
 187 qed.
 188
 189 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
 190 #A #B #l #f elim l // #a #tl #Hind normalize //
 191 qed.
 192
 193 lemma length_reverse: ∀A.∀l:list A.
 194   |reverse A l| = |l|.
 195 #A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
 196 qed.
 197
 198 lemma lenght_to_nil: ∀A.∀l:list A.
 199   |l| = 0 → l = [ ].
 200 #A * // #a #tl normalize #H destruct
 201 qed.
 202
 203 (****************** traversing two lists in parallel *****************)
 204 lemma list_ind2 :
 205   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 206   length ? l1 = length ? l2 →
 207   (P [] []) →
 208   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 209   P l1 l2.
 210 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
 211 generalize in match Hl; generalize in match l2;
 212 elim l1
 213 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
 214 |#t1 #tl1 #IH #l2 cases l2
 215    [normalize #H destruct
 216    |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
 217 ]
 218 qed.
 219
 220 lemma list_cases2 :
 221   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
 222   length ? l1 = length ? l2 →
 223   (l1 = [] → l2 = [] → P) →
 224   (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
 225 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
 226 [ #Pnil #Pcons @Pnil //
 227 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
 228 qed.
 229
 230 (*********************** properties of append ***********************)
 231 lemma append_l1_injective :
 232   ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
 233 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
 234 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
 235 qed.
 236
 237 lemma append_l2_injective :
 238   ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
 239 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
 240 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
 241 qed.
 242
 243 lemma append_l1_injective_r :
 244   ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
 245 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
 246 >reverse_append >reverse_append #Heq1
 247 lapply (append_l2_injective … Heq1) [ // ] #Heq2
 248 lapply (eq_f … (reverse ?) … Heq2) //
 249 qed.
 250
 251 lemma append_l2_injective_r :
 252   ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
 253 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
 254 >reverse_append >reverse_append #Heq1
 255 lapply (append_l1_injective … Heq1) [ // ] #Heq2
 256 lapply (eq_f … (reverse ?) … Heq2) //
 257 qed.
 258
 259 lemma length_rev_append: ∀A.∀l,acc:list A.
 260   |rev_append ? l acc| = |l|+|acc|.
 261 #A #l elim l // #a #tl #Hind normalize
 262 #acc >Hind normalize //
 263 qed.
 264
 265 (****************************** mem ********************************)
 266 let rec mem A (a:A) (l:list A) on l ≝
 267   match l with
 268   [ nil ⇒ False
 269   | cons hd tl ⇒ a=hd ∨ mem A a tl
 270   ].
 271
 272 lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
 273   mem ? a l1 ∨ mem ? a l2.
 274 #A #a #l1 elim l1
 275   [#l2 #mema %2 @mema
 276   |#b #tl #Hind #l2 *
 277     [#eqab %1 %1 @eqab
 278     |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
 279     ]
 280   ]
 281 qed.
 282
 283 lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
 284 #A #a #l1 #l2 elim l1
 285   [whd in ⊢ (%→?); @False_ind
 286   |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
 287   ]
 288 qed.
 289
 290 lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
 291 #A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
 292 qed.
 293
 294 lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
 295 #A #a #b * // @False_ind
 296 qed.
 297
 298 lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
 299   mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
 300 #A #B #f #l elim l
 301   [#b normalize @False_ind
 302   |#a #tl #Hind #b normalize *
 303     [#eqb @(ex_intro … a) /3/
 304     |#memb cases (Hind … memb) #a * #mema #eqb
 305      @(ex_intro … a) /3/
 306     ]
 307   ]
 308 qed.
 309
 310 lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
 311   mem A a l → mem B (f a) (map ?? f l).
 312  #A #B #f #a #l elim l
 313   [normalize @False_ind
 314   |#b #tl #Hind *
 315     [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
 316   ]
 317 qed.
 318
 319 (***************************** split *******************************)
 320 let rec split_rev A (l:list A) acc n on n ≝
 321   match n with
 322   [O ⇒ 〈acc,l〉
 323   |S m ⇒ match l with
 324     [nil ⇒ 〈acc,[]〉
 325     |cons a tl ⇒ split_rev A tl (a::acc) m
 326     ]
 327   ].
 328
 329 definition split ≝ λA,l,n.
 330   let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
 331
 332 lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
 333   |\fst (split_rev A l acc n)| = n+|acc|.
 334 #A #n elim n // #m #Hind *
 335   [normalize #acc #Hfalse @False_ind /2/
 336   |#a #tl #acc #Hlen normalize >Hind
 337     [normalize // |@le_S_S_to_le //]
 338   ]
 339 qed.
 340
 341 lemma split_len: ∀A,n,l. n ≤ |l| →
 342   |\fst (split A l n)| = n.
 343 #A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
 344 normalize >length_reverse  >(split_rev_len … [ ] Hlen) normalize //
 345 qed.
 346
 347 lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
 348   reverse ? acc@ l =
 349     reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
 350  #A #n elim n //
 351  #m #Hind *
 352    [#acc whd in ⊢ ((??%)→?); #False_ind /2/
 353    |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append
 354     @(Hind tl) @le_S_S_to_le @Hlen
 355    ]
 356 qed.
 357
 358 lemma split_eq: ∀A,n,l. n ≤ |l| →
 359   l = (\fst (split A l n))@(\snd (split A l n)).
 360 #A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
 361 >(split_rev_eq … Hlen) normalize
 362 >(eq_pair_fst_snd ?? (split_rev A l [] n)) %
 363 qed.
 364
 365 lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
 366   ∃l1,l2. l = l1@l2 ∧ |l1| = n.
 367 #A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
 368 @(ex_intro … (\snd (split A l n))) % /2/
 369 qed.
 370
 371 (****************************** flatten ******************************)
 372 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
 373
 374 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
 375   (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2  →
 376     (∃q.|l1| = n*q)  → mem ? a l.
 377 #A #n #l elim l
 378   [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
 379    cut (|a|=0) [@sym_eq @le_n_O_to_eq
 380    @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
 381   |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
 382    whd in match (flatten ??); #Hflat * #q cases q
 383     [<times_n_O #Hl1
 384      cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat;
 385      whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
 386      >Ha >Hlen // %1 //
 387      ] /2/
 388     |#q1 #Hl1 lapply (split_exists … n l1 ?) //
 389      * #l11 * #l12 * #Heql1 #Hlenl11 %2
 390      @(Hind l12 l2 … posn ? Ha)
 391       [#x #memx @Hlen %2 //
 392       |@(append_l2_injective ? hd l11)
 393         [>Hlenl11 @Hlen %1 %
 394         |>Hflat >Heql1 >associative_append %
 395         ]
 396       |@(ex_intro …q1) @(injective_plus_r n)
 397        <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
 398       ]
 399     ]
 400   ]
 401 qed.
 402
 403 (****************************** nth ********************************)
 404 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
 405   match n with
 406     [O ⇒ hd A l d
 407     |S m ⇒ nth m A (tail A l) d].
 408
 409 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
 410 #A #a #i elim i normalize //
 411 qed.
 412
 413 (****************************** nth_opt ********************************)
 414 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
 415 match l with
 416 [ nil ⇒ None ?
 417 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
 418 ].
 419
 420 (**************************** All *******************************)
 421
 422 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 423 match l with
 424 [ nil ⇒ True
 425 | cons h t ⇒ P h ∧ All A P t
 426 ].
 427
 428 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
 429 #A #P #Q #H #l elim l normalize //
 430 #h #t #IH * /3/
 431 qed.
 432
 433 lemma All_nth : ∀A,P,n,l.
 434   All A P l →
 435   ∀a.
 436   nth_opt A n l = Some A a →
 437   P a.
 438 #A #P #n elim n
 439 [ * [ #_ #a #E whd in E:(??%?); destruct
 440     | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
 441     ]
 442 | #m #IH *
 443   [ #_ #a #E whd in E:(??%?); destruct
 444   | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
 445   ]
 446 ] qed.
 447
 448 lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
 449 #A #P #l1 elim l1 -l1 //
 450 #a #l1 #IHl1 #l2 * /3 width=1/
 451 qed.
 452
 453 lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
 454 #A #P #l1 elim l1 -l1 /2 width=1/
 455 #a #l1 #IHl1 #l2 * #Ha #Hl12
 456 elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
 457 qed-.
 458
 459 (**************************** Allr ******************************)
 460
 461 let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
 462 match l with
 463 [ nil       ⇒ True
 464 | cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
 465 ].
 466
 467 lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
 468 #A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
 469 qed-.
 470
 471 lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
 472 #A #R #a * // #a0 #l * //
 473 qed-.
 474
 475 (**************************** Exists *******************************)
 476
 477 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 478 match l with
 479 [ nil ⇒ False
 480 | cons h t ⇒ (P h) ∨ (Exists A P t)
 481 ].
 482
 483 lemma Exists_append : ∀A,P,l1,l2.
 484   Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
 485 #A #P #l1 elim l1
 486 [ normalize /2/
 487 | #h #t #IH #l2 *
 488   [ #H /3/
 489   | #H cases (IH l2 H) /3/
 490   ]
 491 ] qed.
 492
 493 lemma Exists_append_l : ∀A,P,l1,l2.
 494   Exists A P l1 → Exists A P (l1@l2).
 495 #A #P #l1 #l2 elim l1
 496 [ *
 497 | #h #t #IH *
 498   [ #H %1 @H
 499   | #H %2 @IH @H
 500   ]
 501 ] qed.
 502
 503 lemma Exists_append_r : ∀A,P,l1,l2.
 504   Exists A P l2 → Exists A P (l1@l2).
 505 #A #P #l1 #l2 elim l1
 506 [ #H @H
 507 | #h #t #IH #H %2 @IH @H
 508 ] qed.
 509
 510 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
 511 #A #P #l1 #x #l2 elim l1
 512 [ normalize #H %2 @H
 513 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
 514 qed.
 515
 516 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
 517 #A #P #l1 #x #l2 #H elim l1
 518 [ %1 @H
 519 | #h #t #IH %2 @IH
 520 ] qed.
 521
 522 lemma Exists_map : ∀A,B,P,Q,f,l.
 523 Exists A P l →
 524 (∀a.P a → Q (f a)) →
 525 Exists B Q (map A B f l).
 526 #A #B #P #Q #f #l elim l //
 527 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
 528
 529 lemma Exists_All : ∀A,P,Q,l.
 530   Exists A P l →
 531   All A Q l →
 532   ∃x. P x ∧ Q x.
 533 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
 534 qed.
 535
 536 (**************************** fold *******************************)
 537
 538 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
 539  match l with
 540   [ nil ⇒ b
 541   | cons a l ⇒
 542      if p a then op (f a) (fold A B op b p f l)
 543      else fold A B op b p f l].
 544
 545 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 546   with precedence 80
 547 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 548
 549 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 550   with precedence 80
 551 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 552
 553 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 554
 555 theorem fold_true:
 556 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
 557   \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 558     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
 559 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 560
 561 theorem fold_false:
 562 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 563 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 564   \fold[op,nil]_{i ∈ l| p i} (f i).
 565 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 566
 567 theorem fold_filter:
 568 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 569   \fold[op,nil]_{i ∈ l| p i} (f i) =
 570     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
 571 #A #B #a #l #p #op #nil #f elim l //
 572 #a #tl #Hind cases(true_or_false (p a)) #pa
 573   [ >filter_true // > fold_true // >fold_true //
 574   | >filter_false // >fold_false // ]
 575 qed.
 576
 577 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 578   {op :2> A → A → A;
 579    nill:∀a. op nil a = a;
 580    nilr:∀a. op a nil = a;
 581    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 582   }.
 583
 584 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
 585   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
 586     \fold[op,nil]_{i∈(I@J)} (f i).
 587 #A #B #I #J #nil #op #f (elim I) normalize
 588   [>nill //|#a #tl #Hind <assoc //]
 589 qed.
 590
 591 (********************** lhd and ltl ******************************)
 592
 593 let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
 594    [ O   ⇒ nil …
 595    | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
 596    ].
 597
 598 let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
 599    [ O   ⇒ l
 600    | S n ⇒ ltl A (tail … l) n
 601    ].
 602
 603 lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
 604 #A #n elim n //
 605 qed.
 606
 607 lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
 608 #A #n elim n normalize //
 609 qed.
 610
 611 lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 612 #A #n elim n -n //
 613 #n #IHn #l elim l normalize //
 614 qed.
 615
 616 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 617 #A #n elim n -n //
 618 #n #IHn *; normalize /2/
 619 qed.
 620
 621 (********************** find ******************************)
 622 let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
 623 match l with
 624 [ nil ⇒ None B
 625 | cons h t ⇒
 626     match f h with
 627     [ None ⇒ find A B f t
 628     | Some b ⇒ Some B b
 629     ]
 630 ].
 631
 632 (********************** position_of ******************************)
 633 let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
 634 match l with
 635 [ nil ⇒ None ?
 636 | cons h t ⇒
 637    match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
 638
 639 definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
 640  λA,found,l. position_of_aux A found l 0.
 641
 642
 643 (********************** make_list ******************************)
 644 let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
 645 match n with
 646 [ O ⇒ [ ]
 647 | S m ⇒ a::(make_list A a m)
 648 ].