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 "arithmetics/nat.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 ntheorem nil_cons:
  37   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
  38 #A;#l;#a; @; #H; ndestruct;
  39 nqed.
  40
  41 nlet rec id_list A (l: list A) on l ≝
  42   match l with
  43   [ nil ⇒ []
  44   | cons hd tl ⇒ hd :: id_list A tl ].
  45
  46 nlet rec append A (l1: list A) l2 on l1 ≝
  47   match l1 with
  48   [ nil ⇒ l2
  49   | cons hd tl ⇒ hd :: append A tl l2 ].
  50
  51 ndefinition tail ≝ λA:Type[0].λl:list A.
  52   match l with
  53   [ nil ⇒  []
  54   | cons hd tl ⇒  tl].
  55
  56 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  57
  58 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
  59 #A;#l;nelim l;//;
  60 #a;#l1;#IH;nnormalize;//;
  61 nqed.
  62
  63 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
  64 #A;#x;#y;#z;nelim x
  65 ##[//
  66 ##|#a;#x1;#H;nnormalize;//]
  67 nqed.
  68
  69 ntheorem cons_append_commute:
  70   ∀A:Type[0].∀l1,l2:list A.∀a:A.
  71     a :: (l1 @ l2) = (a :: l1) @ l2.
  72 //;
  73 nqed.
  74
  75 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
  76 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
  77 nqed.
  78
  79 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
  80   | refl : \forall l:list A. permutation ? l l
  81   | swap : \forall l:list A. \forall x,y:A.
  82               permutation ? (x :: y :: l) (y :: x :: l)
  83   | trans : \forall l1,l2,l3:list A.
  84               permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
  85 with permut1 : list A -> list A -> Prop \def
  86   | step : \forall l1,l2:list A. \forall x,y:A.
  87       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
  88
  89 (*
  90
  91 definition x1 \def S O.
  92 definition x2 \def S x1.
  93 definition x3 \def S x2.
  94
  95 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
  96   apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
  97   apply refl.
  98   apply (step ? (x1::[]) [] x2 x3).
  99   qed.
 100
 101 theorem nil_append_nil_both:
 102   \forall A:Type.\forall l1,l2:list A.
 103     l1 @ l2 = [] \to l1 = [] \land l2 = [].
 104
 105 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
 106 reflexivity.
 107 qed.
 108
 109 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 110 simplify.
 111 reflexivity.
 112 qed.
 113
 114 *)
 115
 116 nlet rec nth A l d n on n ≝
 117   match n with
 118   [ O ⇒ match l with
 119         [ nil ⇒ d
 120         | cons (x : A) _ ⇒ x ]
 121   | S n' ⇒ nth A (tail ? l) d n'].
 122
 123 nlet rec map A B f l on l ≝
 124   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
 125
 126 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
 127   match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
 128
 129 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
 130
 131 ndefinition filter ≝
 132   λT:Type[0].λl:list T.λp:T → bool.
 133   foldr T (list T)
 134     (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
 135
 136 ndefinition iota : nat → nat → list nat ≝
 137   λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
 138
 139 (* ### induction principle for functions visiting 2 lists in parallel *)
 140 nlemma list_ind2 :
 141   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 142   length ? l1 = length ? l2 →
 143   (P (nil ?) (nil ?)) →
 144   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 145   P l1 l2.
 146 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
 147 ngeneralize in match Hl; ngeneralize in match l2;
 148 nelim l1
 149 ##[#l2;ncases l2;//;
 150    nnormalize;#t2;#tl2;#H;ndestruct;
 151 ##|#t1;#tl1;#IH;#l2;ncases l2
 152    ##[nnormalize;#H;ndestruct
 153    ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
 154 ##]
 155 nqed.
 156
 157 nlemma 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;#Efg;
 159 nelim l; nnormalize;//;
 160 nqed.
 161
 162 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
 163 #A;#l;#p;nelim l;nnormalize
 164 ##[//
 165 ##|#a;#tl;#IH;ncases (p a);nnormalize;
 166    ##[napply le_S_S;//;
 167    ##|@2;//]
 168 ##]
 169 nqed.
 170
 171 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
 172 #A;#l;#m;nelim l;
 173 ##[//
 174 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
 175 nqed.
 176
 177 ninductive in_list (A:Type): A → (list A) → Prop ≝
 178 | in_list_head : ∀ x,l.(in_list A x (x::l))
 179 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
 180
 181 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
 182   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
 183
 184 notation "hvbox(a break ∉ b)" non associative with precedence 45
 185 for @{ 'notmem $a $b }.
 186
 187 interpretation "list member" 'mem x l = (in_list ? x l).
 188 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 189 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
 190
 191 naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
 192 (*intros.unfold.intro.inversion H
 193   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
 194   |intros;destruct H4]
 195 qed.*)
 196
 197 naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
 198                           x = a \lor in_list A x l.
 199 (*intros;inversion H;intros
 200   [destruct H2;left;reflexivity
 201   |destruct H4;right;assumption]
 202 qed.*)
 203
 204 naxiom in_list_tail : \forall l,x,y.
 205       in_list nat x (y::l) \to x \neq y \to in_list nat x l.
 206 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
 207   [elim (H2 H1)
 208   |assumption]
 209 qed.*)
 210
 211 naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
 212 (*intros;elim (in_list_cons_case ? ? ? ? H)
 213   [assumption
 214   |elim (not_in_list_nil ? ? H1)]
 215 qed.*)
 216
 217 naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
 218 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
 219 (*intros.
 220 elim H;simplify
 221   [apply in_list_head
 222   |apply in_list_cons;assumption
 223   ]
 224 qed.*)
 225
 226 naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
 227 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
 228 (*intros 3.
 229 elim l1;simplify
 230   [assumption
 231   |apply in_list_cons;apply H;assumption
 232   ]
 233 qed.*)
 234
 235 naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
 236 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
 237 (*intros 3.
 238 elim l
 239   [right.apply H
 240   |simplify in H1.inversion H1;intros; destruct;
 241     [left.apply in_list_head
 242     | elim (H l2)
 243       [left.apply in_list_cons. assumption
 244       |right.assumption
 245       |assumption
 246       ]
 247     ]
 248   ]
 249 qed.*)
 250
 251 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 252  match l with
 253   [ nil ⇒ false
 254   | (cons a l') ⇒
 255     match eq x a with
 256      [ true ⇒ true
 257      | false ⇒ mem A eq x l'
 258      ]
 259   ].
 260
 261 naxiom mem_true_to_in_list :
 262   \forall A,equ.
 263   (\forall x,y.equ x y = true \to x = y) \to
 264   \forall x,l.mem A equ x l = true \to in_list A x l.
 265 (* intros 5.elim l
 266   [simplify in H1;destruct H1
 267   |simplify in H2;apply (bool_elim ? (equ x a))
 268      [intro;rewrite > (H ? ? H3);apply in_list_head
 269      |intro;rewrite > H3 in H2;simplify in H2;
 270       apply in_list_cons;apply H1;assumption]]
 271 qed.*)
 272
 273 naxiom in_list_to_mem_true :
 274   \forall A,equ.
 275   (\forall x.equ x x = true) \to
 276   \forall x,l.in_list A x l \to mem A equ x l = true.
 277 (*intros 5.elim l
 278   [elim (not_in_list_nil ? ? H1)
 279   |elim H2
 280     [simplify;rewrite > H;reflexivity
 281     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 282 qed.*)
 283
 284 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
 285 in_list A x (filter A l p) \to p x = true.
 286 (* intros 4;elim l
 287   [simplify in H;elim (not_in_list_nil ? ? H)
 288   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 289    simplify in H1
 290      [elim (in_list_cons_case ? ? ? ? H1)
 291         [rewrite > H3;assumption
 292         |apply (H H3)]
 293      |apply (H H1)]]
 294 qed.*)
 295
 296 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 297 (*intros 4;elim l
 298   [simplify in H;elim (not_in_list_nil ? ? H)
 299   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 300    simplify in H1
 301      [elim (in_list_cons_case ? ? ? ? H1)
 302         [rewrite > H3;apply in_list_head
 303         |apply in_list_cons;apply H;assumption]
 304      |apply in_list_cons;apply H;assumption]]
 305 qed.*)
 306
 307 naxiom in_list_filter_r : \forall A,l,p,x.
 308               in_list A x l \to p x = true \to in_list A x (filter A l p).
 309 (* intros 4;elim l
 310   [elim (not_in_list_nil ? ? H)
 311   |elim (in_list_cons_case ? ? ? ? H1)
 312      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 313      |simplify;apply (bool_elim ? (p a));intro;simplify;
 314         [apply in_list_cons;apply H;assumption
 315         |apply H;assumption]]]
 316 qed.*)
 317
 318 naxiom incl_A_A: ∀T,A.incl T A A.
 319 (*intros.unfold incl.intros.assumption.
 320 qed.*)
 321
 322 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
 323 (*unfold incl; intros;autobatch.
 324 qed.*)
 325
 326 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
 327 (*unfold incl; intros;autobatch.
 328 qed.*)
 329
 330 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 331 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 332 qed.*)
 333