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 not_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 (not_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 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  60
  61 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
  62 #A #l (elim l) normalize // qed.
  63
  64 theorem associative_append:
  65  ∀A.associative (list A) (append A).
  66 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  67
  68 (* deleterio per auto
  69 ntheorem cons_append_commute:
  70   ∀A:Type.∀l1,l2:list A.∀a:A.
  71     a :: (l1 @ l2) = (a :: l1) @ l2.
  72 //; nqed. *)
  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 (* iterators *)
  89
  90 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
  91  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
  92
  93 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
  94  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  95
  96 definition filter ≝
  97   λT.λp:T → bool.
  98   foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
  99
 100 (* compose f [a1;...;an] [b1;...;bm] =
 101   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
 102
 103 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
 104     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
 105
 106 lemma filter_true : ∀A,l,a,p. p a = true →
 107   filter A p (a::l) = a :: filter A p l.
 108 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 109
 110 lemma filter_false : ∀A,l,a,p. p a = false →
 111   filter A p (a::l) = filter A p l.
 112 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 113
 114 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 115 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 116
 117 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 118 match l1 with
 119   [ nil ⇒ nil ?
 120   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
 121   ].
 122
 123 (**************************** length ******************************)
 124
 125 let rec length (A:Type[0]) (l:list A) on l ≝
 126   match l with
 127     [ nil ⇒ 0
 128     | cons a tl ⇒ S (length A tl)].
 129
 130 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 131 interpretation "norm" 'norm l = (length ? l).
 132
 133 lemma length_append: ∀A.∀l1,l2:list A.
 134   |l1@l2| = |l1|+|l2|.
 135 #A #l1 elim l1 // normalize /2/
 136 qed.
 137
 138 (****************************** nth ********************************)
 139 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
 140   match n with
 141     [O ⇒ hd A l d
 142     |S m ⇒ nth m A (tail A l) d].
 143
 144 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
 145 #A #a #i elim i normalize //
 146 qed.
 147
 148 (**************************** fold *******************************)
 149
 150 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 ≝
 151  match l with
 152   [ nil ⇒ b
 153   | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
 154       (fold A B op b p f l)].
 155
 156 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 157   with precedence 80
 158 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 159
 160 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 161   with precedence 80
 162 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 163
 164 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 165
 166 theorem fold_true:
 167 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
 168   \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 169     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
 170 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 171
 172 theorem fold_false:
 173 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 174 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 175   \fold[op,nil]_{i ∈ l| p i} (f i).
 176 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 177
 178 theorem fold_filter:
 179 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 180   \fold[op,nil]_{i ∈ l| p i} (f i) =
 181     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
 182 #A #B #a #l #p #op #nil #f elim l //
 183 #a #tl #Hind cases(true_or_false (p a)) #pa
 184   [ >filter_true // > fold_true // >fold_true //
 185   | >filter_false // >fold_false // ]
 186 qed.
 187
 188 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 189   {op :2> A → A → A;
 190    nill:∀a. op nil a = a;
 191    nilr:∀a. op a nil = a;
 192    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 193   }.
 194
 195 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
 196   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
 197     \fold[op,nil]_{i∈(I@J)} (f i).
 198 #A #B #I #J #nil #op #f (elim I) normalize
 199   [>nill //|#a #tl #Hind <assoc //]
 200 qed.
 201
 202 (********************** lhd and ltl ******************************)
 203
 204 let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
 205    [ O   ⇒ nil …
 206    | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
 207    ].
 208
 209 let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
 210    [ O   ⇒ l
 211    | S n ⇒ ltl A (tail … l) n
 212    ].
 213
 214 lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
 215 #A #n elim n //
 216 qed.
 217
 218 lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
 219 #A #n elim n normalize //
 220 qed.
 221
 222 lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 223 #A #n elim n -n //
 224 #n #IHn #l elim l normalize //
 225 qed.
 226
 227 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 228 #A #n elim n -n /2/
 229 #n #IHn *; normalize /2/
 230 qed.