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