helm/software/matita/nlibrary/datatypes/list.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/pts.ma".
  16
  17 ninductive list (A:Type[0]) : Type[0] ≝
  18   | nil: list A
  19   | cons: A -> list A -> list A.
  20
  21 notation "hvbox(hd break :: tl)"
  22   right associative with precedence 47
  23   for @{'cons $hd $tl}.
  24
  25 notation "[ list0 x sep ; ]"
  26   non associative with precedence 90
  27   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  28
  29 notation "hvbox(l1 break @ l2)"
  30   right associative with precedence 47
  31   for @{'append $l1 $l2 }.
  32
  33 interpretation "nil" 'nil = (nil ?).
  34 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  35
  36 nlet rec append A (l1: list A) l2 on l1 ≝
  37   match l1 with
  38   [ nil ⇒ l2
  39   | cons hd tl ⇒ hd :: append A tl l2 ].
  40
  41 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  42
  43 nlet 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
  49 ndefinition tail ≝ λA:Type[0].λl:list A.
  50   match l with
  51   [ nil ⇒  []
  52   | cons hd tl ⇒  tl].
  53
  54 nlet rec flatten S (l : list (list S)) on l : list S ≝
  55 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
  56
  57 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
  58 #A;#l;nelim l;//;
  59 #a;#l1;#IH;nnormalize;//;
  60 nqed.
  61
  62 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
  63 #A;#x;#y;#z;nelim x
  64 ##[//
  65 ##|#a;#x1;#H;nnormalize;//]
  66 nqed.
  67
  68 ntheorem cons_append_commute:
  69   ∀A:Type[0].∀l1,l2:list A.∀a:A.
  70     a :: (l1 @ l2) = (a :: l1) @ l2.
  71 //;
  72 nqed.
  73
  74 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
  75 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
  76 nqed.
  77
  78 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
  79   | refl : \forall l:list A. permutation ? l l
  80   | swap : \forall l:list A. \forall x,y:A.
  81               permutation ? (x :: y :: l) (y :: x :: l)
  82   | trans : \forall l1,l2,l3:list A.
  83               permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
  84 with permut1 : list A -> list A -> Prop \def
  85   | step : \forall l1,l2:list A. \forall x,y:A.
  86       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
  87
  88 (*
  89
  90 definition x1 \def S O.
  91 definition x2 \def S x1.
  92 definition x3 \def S x2.
  93
  94 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
  95   apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
  96   apply refl.
  97   apply (step ? (x1::[]) [] x2 x3).
  98   qed.
  99
 100 theorem nil_append_nil_both:
 101   \forall A:Type.\forall l1,l2:list A.
 102     l1 @ l2 = [] \to l1 = [] \land l2 = [].
 103
 104 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
 105 reflexivity.
 106 qed.
 107
 108 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 109 simplify.
 110 reflexivity.
 111 qed.
 112
 113 *)
 114
 115 nlet rec nth A l d n on l ≝
 116   match l with
 117   [ nil ⇒ d
 118   | cons (x:A) tl ⇒ match n with
 119     [ O ⇒ x
 120     | S n' ⇒ nth A tl d n' ] ].
 121
 122 nlet rec map A B f l on l ≝
 123   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
 124
 125 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
 126   match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
 127
 128 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
 129
 130 ndefinition filter ≝
 131   λT:Type[0].λl:list T.λp:T → bool.
 132   foldr T (list T)
 133     (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
 134
 135 ndefinition iota : nat → nat → list nat ≝
 136   λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
 137
 138 (* ### induction principle for functions visiting 2 lists in parallel *)
 139 nlemma list_ind2 :
 140   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 141   length ? l1 = length ? l2 →
 142   (P (nil ?) (nil ?)) →
 143   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 144   P l1 l2.
 145 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
 146 ngeneralize in match Hl; ngeneralize in match l2;
 147 nelim l1
 148 ##[#l2;ncases l2;//;
 149    nnormalize;#t2;#tl2;#H;ndestruct;
 150 ##|#t1;#tl1;#IH;#l2;ncases l2
 151    ##[nnormalize;#H;ndestruct
 152    ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
 153 ##]
 154 nqed.
 155
 156 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 157 #A;#B;#f;#g;#l;#Efg;
 158 nelim l; nnormalize;//;
 159 nqed.
 160
 161 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
 162 #A;#l;#p;nelim l;nnormalize
 163 ##[//
 164 ##|#a;#tl;#IH;ncases (p a);nnormalize;
 165    ##[napply le_S_S;//;
 166    ##|@2;//]
 167 ##]
 168 nqed.
 169
 170 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
 171 #A;#l;#m;nelim l;
 172 ##[//
 173 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
 174 nqed.
 175
 176 ninductive in_list (A:Type): A → (list A) → Prop ≝
 177 | in_list_head : ∀ x,l.(in_list A x (x::l))
 178 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
 179
 180 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
 181   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
 182
 183 notation "hvbox(a break ∉ b)" non associative with precedence 45
 184 for @{ 'notmem $a $b }.
 185
 186 interpretation "list member" 'mem x l = (in_list ? x l).
 187 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 188 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
 189
 190 naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
 191 (*intros.unfold.intro.inversion H
 192   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
 193   |intros;destruct H4]
 194 qed.*)
 195
 196 naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
 197                           x = a \lor in_list A x l.
 198 (*intros;inversion H;intros
 199   [destruct H2;left;reflexivity
 200   |destruct H4;right;assumption]
 201 qed.*)
 202
 203 nlemma in_list_tail : \forall A,l,x,y.
 204       in_list A x (y::l) \to x \neq y \to in_list A x l.
 205 #A;#l;#x;#y;#H;#Hneq;
 206 ninversion H;
 207 ##[#x1;#l1;#Hx;#Hl;ndestruct;nelim Hneq;#Hfalse;
 208    nelim (Hfalse ?);@;
 209 ##|#x1;#y1;#l1;#H1;#_;#Hx;#Heq;ndestruct;//;
 210 ##]
 211 nqed.
 212
 213 naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
 214 (*intros;elim (in_list_cons_case ? ? ? ? H)
 215   [assumption
 216   |elim (not_in_list_nil ? ? H1)]
 217 qed.*)
 218
 219 naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
 220 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
 221 (*intros.
 222 elim H;simplify
 223   [apply in_list_head
 224   |apply in_list_cons;assumption
 225   ]
 226 qed.*)
 227
 228 naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
 229 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
 230 (*intros 3.
 231 elim l1;simplify
 232   [assumption
 233   |apply in_list_cons;apply H;assumption
 234   ]
 235 qed.*)
 236
 237 naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
 238 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
 239 (*intros 3.
 240 elim l
 241   [right.apply H
 242   |simplify in H1.inversion H1;intros; destruct;
 243     [left.apply in_list_head
 244     | elim (H l2)
 245       [left.apply in_list_cons. assumption
 246       |right.assumption
 247       |assumption
 248       ]
 249     ]
 250   ]
 251 qed.*)
 252
 253 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 254  match l with
 255   [ nil ⇒ false
 256   | (cons a l') ⇒
 257     match eq x a with
 258      [ true ⇒ true
 259      | false ⇒ mem A eq x l'
 260      ]
 261   ].
 262
 263 naxiom mem_true_to_in_list :
 264   \forall A,equ.
 265   (\forall x,y.equ x y = true \to x = y) \to
 266   \forall x,l.mem A equ x l = true \to in_list A x l.
 267 (* intros 5.elim l
 268   [simplify in H1;destruct H1
 269   |simplify in H2;apply (bool_elim ? (equ x a))
 270      [intro;rewrite > (H ? ? H3);apply in_list_head
 271      |intro;rewrite > H3 in H2;simplify in H2;
 272       apply in_list_cons;apply H1;assumption]]
 273 qed.*)
 274
 275 naxiom in_list_to_mem_true :
 276   \forall A,equ.
 277   (\forall x.equ x x = true) \to
 278   \forall x,l.in_list A x l \to mem A equ x l = true.
 279 (*intros 5.elim l
 280   [elim (not_in_list_nil ? ? H1)
 281   |elim H2
 282     [simplify;rewrite > H;reflexivity
 283     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 284 qed.*)
 285
 286 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
 287 in_list A x (filter A l p) \to p x = true.
 288 (* intros 4;elim l
 289   [simplify in H;elim (not_in_list_nil ? ? H)
 290   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 291    simplify in H1
 292      [elim (in_list_cons_case ? ? ? ? H1)
 293         [rewrite > H3;assumption
 294         |apply (H H3)]
 295      |apply (H H1)]]
 296 qed.*)
 297
 298 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 299 (*intros 4;elim l
 300   [simplify in H;elim (not_in_list_nil ? ? H)
 301   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 302    simplify in H1
 303      [elim (in_list_cons_case ? ? ? ? H1)
 304         [rewrite > H3;apply in_list_head
 305         |apply in_list_cons;apply H;assumption]
 306      |apply in_list_cons;apply H;assumption]]
 307 qed.*)
 308
 309 naxiom in_list_filter_r : \forall A,l,p,x.
 310               in_list A x l \to p x = true \to in_list A x (filter A l p).
 311 (* intros 4;elim l
 312   [elim (not_in_list_nil ? ? H)
 313   |elim (in_list_cons_case ? ? ? ? H1)
 314      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 315      |simplify;apply (bool_elim ? (p a));intro;simplify;
 316         [apply in_list_cons;apply H;assumption
 317         |apply H;assumption]]]
 318 qed.*)
 319
 320 naxiom incl_A_A: ∀T,A.incl T A A.
 321 (*intros.unfold incl.intros.assumption.
 322 qed.*)
 323
 324 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
 325 (*unfold incl; intros;autobatch.
 326 qed.*)
 327
 328 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
 329 (*unfold incl; intros;autobatch.
 330 qed.*)
 331
 332 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 333 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 334 qed.*)
 335
 336 nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝
 337  match l with
 338  [ nil ⇒ a
 339  | cons b bl ⇒ foldl A B f (f a b) bl ].
 340
 341 nlet rec foldl2 (A,B,C:Type[0]) (f:A → B → C → A) (a:A) (bl:list B) (cl:list C) on bl ≝
 342  match bl with
 343  [ nil ⇒ a
 344  | cons b0 bl0 ⇒ match cl with
 345    [ nil ⇒ a
 346    | cons c0 cl0 ⇒ foldl2 A B C f (f a b0 c0) bl0 cl0 ] ].
 347
 348 nlet rec foldr2 (A,B : Type[0]) (X : Type[0]) (f: A → B → X → X) (x:X)
 349                 (al : list A) (bl : list B) on al : X ≝
 350   match al with
 351   [ nil ⇒ x
 352   | cons a al1 ⇒ match bl with
 353     [ nil ⇒ x
 354     | cons b bl1 ⇒ f a b (foldr2 ??? f x al1 bl1) ] ].
 355
 356 nlet rec rev (A:Type[0]) (l:list A) on l ≝
 357  match l with
 358  [ nil ⇒ nil A
 359  | cons hd tl ⇒ (rev A tl)@[hd] ].
 360
 361 notation > "hvbox(a break \liff b)"
 362   left associative with precedence 25
 363 for @{ 'iff $a $b }.
 364
 365 notation "hvbox(a break \leftrightarrow b)"
 366   left associative with precedence 25
 367 for @{ 'iff $a $b }.
 368
 369 interpretation "logical iff" 'iff x y = (iff x y).
 370
 371 ndefinition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
 372
 373 notation > "hvbox(a break ≡ b)"
 374   non associative with precedence 45
 375 for @{'equiv $a $b}.
 376
 377 notation < "hvbox(term 46 a break ≡ term 46 b)"
 378   non associative with precedence 45
 379 for @{'equiv $a $b}.
 380
 381 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
 382
 383 nlemma refl_coincl : ∀A.∀l:list A.l ≡ l.
 384 #;@;#;//;
 385 nqed.
 386
 387 nlemma coincl_rev : ∀A.∀l:list A.l ≡ rev ? l.
 388 #A l x;@;nelim l
 389 ##[##1,3:#H;napply False_ind;ncases (not_in_list_nil ? x);
 390    #H1;napply (H1 H);
 391 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 392    ##[napply in_list_to_in_list_append_r;nrewrite > H1;@
 393    ##|napply in_list_to_in_list_append_l;/2/
 394    ##]
 395 ##|#a l0 IH H;ncases (in_list_append_to_or_in_list ???? H);#H1
 396    ##[/3/;
 397    ##|nrewrite > (in_list_singleton_to_eq ??? H1);@
 398    ##]
 399 ##]
 400 nqed.
 401
 402 nlemma not_in_list_nil_r : ∀A.∀l:list A.l = [] → ∀x.x ∉ l.
 403 #A l;nelim l
 404 ##[#;napply not_in_list_nil
 405 ##|#a l0 IH Hfalse;ndestruct (Hfalse)
 406 ##]
 407 nqed.
 408
 409 nlemma eq_filter_append :
 410  ∀A,p,l1,l2.filter A (l1@l2) p = filter A l1 p@filter A l2 p.
 411 #A p l1 l2;nelim l1
 412 ##[@
 413 ##|#a0 l0 IH;nwhd in ⊢ (??%(??%?));ncases (p a0)
 414    ##[nwhd in ⊢ (??%%);nrewrite < IH;@
 415    ##|nwhd in ⊢ (??%(??%?));nrewrite < IH;@
 416    ##]
 417 ##]
 418 nqed.
 419
 420 nlemma map_ind :
 421  ∀A,B:Type[0].∀f:A→B.∀P:B → Prop.
 422   ∀al.(∀a.a ∈ al → P (f a)) →
 423   ∀b. b ∈ map ?? f al → P b.
 424 #A B f P al;nelim al
 425 ##[#H1 b Hfalse;napply False_ind;
 426    ncases (not_in_list_nil ? b);#H2;napply H2;napply Hfalse;
 427 ##|#a1 al1 IH H1 b Hin;nwhd in Hin:(???%);ncases (in_list_cons_case ???? Hin);
 428    ##[#e;nrewrite > e;napply H1;@
 429    ##|#Hin1;napply IH;
 430       ##[#a2 Hin2;napply H1;@2;//;
 431       ##|//
 432       ##]
 433    ##]
 434 ##]
 435 nqed.
 436
 437 nlemma map_compose :
 438  ∀A,B,C,f,g,l.map B C f (map A B g l) = map A C (λx.f (g x)) l.
 439 #A B C f g l;nelim l
 440 ##[@
 441 ##|#a0 al0 IH;nchange in ⊢ (??%%) with (cons ???);
 442    napply eq_f2; //;
 443 ##]
 444 nqed.
 445
 446 naxiom incl_incl_to_incl_append :
 447   ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
 448
 449 naxiom eq_map_append : ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
 450
 451 naxiom not_in_list_to_mem_false :
 452   ∀A,equ.
 453   (∀x,y.equ x y = true → x = y) →
 454   ∀x:A.∀l. x ∉ l → mem A equ x l = false.
 455
 456 nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝
 457  match l with
 458  [ nil ⇒ (true:bool)
 459  | cons a al ⇒ p a ∧ list_forall A al p ].
 460
 461 nlemma eq_map_f_g :
 462  ∀A,B,f,g,xl.(∀x.x ∈ xl → f x = g x) → map A B f xl = map A B g xl.
 463 #A B f g xl;nelim xl
 464 ##[#;@
 465 ##|#a al IH H1;nwhd in ⊢ (??%%);napply eq_f2
 466    ##[napply H1;@;
 467    ##|napply IH;#x Hx;napply H1;@2;//
 468    ##]
 469 ##]
 470 nqed.
 471
 472 nlemma x_in_map_to_eq :
 473   ∀A,B,f,x,l.x ∈ map A B f l → ∃x'.x = f x' ∧ x' ∈ l.
 474 #A B f x l;nelim l
 475 ##[#H;ncases (not_in_list_nil ? x);#H1;napply False_ind;napply (H1 H)
 476 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 477    ##[nrewrite > H1;@ a;@;@
 478    ##|ncases (IH H1);#a0;*;#H2 H3;@a0;@
 479       ##[// ##|@2;// ##]
 480    ##]
 481 ##]
 482 nqed.
 483
 484 nlemma list_forall_false :
 485  ∀A:Type[0].∀x,xl,p. p x = false → x ∈ xl → list_forall A xl p = false.
 486 #A x xl p H1;nelim xl
 487 ##[#Hfalse;napply False_ind;ncases (not_in_list_nil ? x);#H2;napply (H2 Hfalse)
 488 ##|#x0 xl0 IH H2;ncases (in_list_cons_case ???? H2);#H3
 489    ##[nwhd in ⊢ (??%?);nrewrite < H3;nrewrite > H1;@
 490    ##|nwhd in ⊢ (??%?);ncases (p x0)
 491       ##[nrewrite > (IH H3);@
 492       ##|@
 493       ##]
 494    ##]
 495 ##]
 496 nqed.
 497
 498 nlemma list_forall_true :
 499  ∀A:Type[0].∀xl,p. (∀x.x ∈ xl → p x = true) → list_forall A xl p = true.
 500 #A xl p;nelim xl
 501 ##[#;@
 502 ##|#x0 xl0 IH H1;nwhd in ⊢ (??%?);nrewrite > (H1 …)
 503    ##[napply IH;#x Hx;napply H1;@2;//
 504    ##|@
 505    ##]
 506 ##]
 507 nqed.