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