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 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 (**************************** iterators ******************************)
  88
  89 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
  90  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
  91
  92 lemma map_append : ∀A,B,f,l1,l2.
  93   (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
  94 #A #B #f #l1 elim l1
  95 [ #l2 @refl
  96 | #h #t #IH #l2 normalize //
  97 ] qed.
  98
  99 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list 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 → bool.
 104   foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
 105
 106 (* compose f [a1;...;an] [b1;...;bm] =
 107   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
 108
 109 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
 110     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
 111
 112 lemma filter_true : ∀A,l,a,p. p a = true →
 113   filter A p (a::l) = a :: filter A p l.
 114 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 115
 116 lemma filter_false : ∀A,l,a,p. p a = false →
 117   filter A p (a::l) = filter A p l.
 118 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 119
 120 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 121 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 122
 123 (**************************** reverse *****************************)
 124 let rec rev_append S (l1,l2:list S) on l1 ≝
 125   match l1 with
 126   [ nil ⇒ l2
 127   | cons a tl ⇒ rev_append S tl (a::l2)
 128   ]
 129 .
 130
 131 definition reverse ≝λS.λl.rev_append S l [].
 132
 133 lemma reverse_single : ∀S,a. reverse S [a] = [a].
 134 // qed.
 135
 136 lemma rev_append_def : ∀S,l1,l2.
 137   rev_append S l1 l2 = (reverse S l1) @ l2 .
 138 #S #l1 elim l1 normalize //
 139 qed.
 140
 141 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
 142 #S #a #l whd in ⊢ (??%?); //
 143 qed.
 144
 145 lemma reverse_append: ∀S,l1,l2.
 146   reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
 147 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
 148 >reverse_cons // qed.
 149
 150 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
 151 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
 152 normalize // qed.
 153
 154 (* an elimination principle for lists working on the tail;
 155 useful for strings *)
 156 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
 157 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
 158 #S #P #Pnil #Pstep #l <(reverse_reverse … l)
 159 generalize in match (reverse S l); #l elim l //
 160 #a #tl #H >reverse_cons @Pstep //
 161 qed.
 162
 163 (**************************** length ******************************)
 164
 165 let rec length (A:Type[0]) (l:list A) on l ≝
 166   match l with
 167     [ nil ⇒ 0
 168     | cons a tl ⇒ S (length A tl)].
 169
 170 notation "|M|" non associative with precedence 65 for @{'norm $M}.
 171 interpretation "norm" 'norm l = (length ? l).
 172
 173 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 174 #A #l elim l //
 175 qed.
 176
 177 lemma length_append: ∀A.∀l1,l2:list A.
 178   |l1@l2| = |l1|+|l2|.
 179 #A #l1 elim l1 // normalize /2/
 180 qed.
 181
 182 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
 183 #A #B #l #f elim l // #a #tl #Hind normalize //
 184 qed.
 185
 186 lemma length_rev_append: ∀A.∀l,acc:list A.
 187   |rev_append ? l acc| = |l|+|acc|.
 188 #A #l elim l // #a #tl #Hind normalize
 189 #acc >Hind normalize //
 190 qed.
 191
 192 lemma length_reverse: ∀A.∀l:list A.
 193   |reverse A l| = |l|.
 194 // qed.
 195
 196 (****************************** mem ********************************)
 197 let rec mem A (a:A) (l:list A) on l ≝
 198   match l with
 199   [ nil ⇒ False
 200   | cons hd tl ⇒ a=hd ∨ mem A a tl
 201   ].
 202
 203 (***************************** split *******************************)
 204 let rec split_rev A (l:list A) acc n on n ≝
 205   match n with
 206   [O ⇒ 〈acc,l〉
 207   |S m ⇒ match l with
 208     [nil ⇒ 〈acc,[]〉
 209     |cons a tl ⇒ split_rev A tl (a::acc) m
 210     ]
 211   ].
 212
 213 definition split ≝ λA,l,n.
 214   let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
 215
 216 lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
 217   |\fst (split_rev A l acc n)| = n+|acc|.
 218 #A #n elim n // #m #Hind *
 219   [normalize #acc #Hfalse @False_ind /2/
 220   |#a #tl #acc #Hlen normalize >Hind
 221     [normalize // |@le_S_S_to_le //]
 222   ]
 223 qed.
 224
 225 lemma split_len: ∀A,n,l. n ≤ |l| →
 226   |\fst (split A l n)| = n.
 227 #A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
 228 normalize >lenght_reverse  >(split_rev_len … [ ] Hlen) normalize //
 229 qed.
 230
 231 lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
 232   reverse ? acc@ l =
 233     reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
 234  #A #n elim n //
 235  #m #Hind *
 236    [#acc whd in ⊢ ((??%)→?); #False_ind /2/
 237    |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append
 238     @(Hind tl) @le_S_S_to_le @Hlen
 239    ]
 240 qed.
 241
 242 lemma split_eq: ∀A,n,l. n ≤ |l| →
 243   l = (\fst (split A l n))@(\snd (split A l n)).
 244 #A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
 245 >(split_rev_eq … Hlen) normalize
 246 >(eq_pair_fst_snd ?? (split_rev A l [] n)) %
 247 qed.
 248
 249 lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
 250   ∃l1,l2. l = l1@l2 ∧ |l1| = n.
 251 #A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
 252 @(ex_intro … (\snd (split A l n))) % /2/
 253 qed.
 254
 255 (****************************** nth ********************************)
 256 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
 257   match n with
 258     [O ⇒ hd A l d
 259     |S m ⇒ nth m A (tail A l) d].
 260
 261 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
 262 #A #a #i elim i normalize //
 263 qed.
 264
 265 (****************************** nth_opt ********************************)
 266 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
 267 match l with
 268 [ nil ⇒ None ?
 269 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
 270 ].
 271
 272 (**************************** All *******************************)
 273
 274 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 275 match l with
 276 [ nil ⇒ True
 277 | cons h t ⇒ P h ∧ All A P t
 278 ].
 279
 280 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
 281 #A #P #Q #H #l elim l normalize //
 282 #h #t #IH * /3/
 283 qed.
 284
 285 lemma All_nth : ∀A,P,n,l.
 286   All A P l →
 287   ∀a.
 288   nth_opt A n l = Some A a →
 289   P a.
 290 #A #P #n elim n
 291 [ * [ #_ #a #E whd in E:(??%?); destruct
 292     | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
 293     ]
 294 | #m #IH *
 295   [ #_ #a #E whd in E:(??%?); destruct
 296   | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
 297   ]
 298 ] qed.
 299
 300 (**************************** Exists *******************************)
 301
 302 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 303 match l with
 304 [ nil ⇒ False
 305 | cons h t ⇒ (P h) ∨ (Exists A P t)
 306 ].
 307
 308 lemma Exists_append : ∀A,P,l1,l2.
 309   Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
 310 #A #P #l1 elim l1
 311 [ normalize /2/
 312 | #h #t #IH #l2 *
 313   [ #H /3/
 314   | #H cases (IH l2 H) /3/
 315   ]
 316 ] qed.
 317
 318 lemma Exists_append_l : ∀A,P,l1,l2.
 319   Exists A P l1 → Exists A P (l1@l2).
 320 #A #P #l1 #l2 elim l1
 321 [ *
 322 | #h #t #IH *
 323   [ #H %1 @H
 324   | #H %2 @IH @H
 325   ]
 326 ] qed.
 327
 328 lemma Exists_append_r : ∀A,P,l1,l2.
 329   Exists A P l2 → Exists A P (l1@l2).
 330 #A #P #l1 #l2 elim l1
 331 [ #H @H
 332 | #h #t #IH #H %2 @IH @H
 333 ] qed.
 334
 335 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
 336 #A #P #l1 #x #l2 elim l1
 337 [ normalize #H %2 @H
 338 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
 339 qed.
 340
 341 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
 342 #A #P #l1 #x #l2 #H elim l1
 343 [ %1 @H
 344 | #h #t #IH %2 @IH
 345 ] qed.
 346
 347 lemma Exists_map : ∀A,B,P,Q,f,l.
 348 Exists A P l →
 349 (∀a.P a → Q (f a)) →
 350 Exists B Q (map A B f l).
 351 #A #B #P #Q #f #l elim l //
 352 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
 353
 354 lemma Exists_All : ∀A,P,Q,l.
 355   Exists A P l →
 356   All A Q l →
 357   ∃x. P x ∧ Q x.
 358 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
 359 qed.
 360
 361 (**************************** fold *******************************)
 362
 363 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 ≝
 364  match l with
 365   [ nil ⇒ b
 366   | cons a l ⇒
 367      if p a then op (f a) (fold A B op b p f l)
 368      else fold A B op b p f l].
 369
 370 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 371   with precedence 80
 372 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 373
 374 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 375   with precedence 80
 376 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 377
 378 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 379
 380 theorem fold_true:
 381 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
 382   \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 383     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
 384 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 385
 386 theorem fold_false:
 387 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 388 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 389   \fold[op,nil]_{i ∈ l| p i} (f i).
 390 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 391
 392 theorem fold_filter:
 393 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 394   \fold[op,nil]_{i ∈ l| p i} (f i) =
 395     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
 396 #A #B #a #l #p #op #nil #f elim l //
 397 #a #tl #Hind cases(true_or_false (p a)) #pa
 398   [ >filter_true // > fold_true // >fold_true //
 399   | >filter_false // >fold_false // ]
 400 qed.
 401
 402 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 403   {op :2> A → A → A;
 404    nill:∀a. op nil a = a;
 405    nilr:∀a. op a nil = a;
 406    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 407   }.
 408
 409 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
 410   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
 411     \fold[op,nil]_{i∈(I@J)} (f i).
 412 #A #B #I #J #nil #op #f (elim I) normalize
 413   [>nill //|#a #tl #Hind <assoc //]
 414 qed.
 415
 416 (********************** lhd and ltl ******************************)
 417
 418 let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
 419    [ O   ⇒ nil …
 420    | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
 421    ].
 422
 423 let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
 424    [ O   ⇒ l
 425    | S n ⇒ ltl A (tail … l) n
 426    ].
 427
 428 lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
 429 #A #n elim n //
 430 qed.
 431
 432 lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
 433 #A #n elim n normalize //
 434 qed.
 435
 436 lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 437 #A #n elim n -n //
 438 #n #IHn #l elim l normalize //
 439 qed.
 440
 441 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 442 #A #n elim n -n //
 443 #n #IHn *; normalize /2/
 444 qed.
 445
 446 (********************** find ******************************)
 447 let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
 448 match l with
 449 [ nil ⇒ None B
 450 | cons h t ⇒
 451     match f h with
 452     [ None ⇒ find A B f t
 453     | Some b ⇒ Some B b
 454     ]
 455 ].
 456
 457 (********************** position_of ******************************)
 458 let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
 459 match l with
 460 [ nil ⇒ None ?
 461 | cons h t ⇒
 462    match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
 463
 464 definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
 465  λA,found,l. position_of_aux A found l 0.
 466
 467
 468 (********************** make_list ******************************)
 469 let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
 470 match n with
 471 [ O ⇒ [ ]
 472 | S m ⇒ a::(make_list A a m)
 473 ].