matita/matita/re_complete/basics/list.ma

   1 include "basics/types.ma".
   2 include "basics/nat.ma".
   3
   4 inductive list (A:Type[0]) : Type[0] :=
   5   | nil: list A
   6   | cons: A -> list A -> list A.
   7
   8 notation "hvbox(hd break :: tl)"
   9   right associative with precedence 47
  10   for @{'cons $hd $tl}.
  11
  12 notation "[ list0 x sep ; ]"
  13   non associative with precedence 90
  14   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  15
  16 notation "hvbox(l1 break @ l2)"
  17   right associative with precedence 47
  18   for @{'append $l1 $l2 }.
  19
  20 interpretation "nil" 'nil = (nil ?).
  21 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  22
  23 definition not_nil: ∀A:Type[0].list A → Prop ≝
  24  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
  25
  26 theorem nil_cons:
  27   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
  28   #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
  29 qed.
  30
  31 (*
  32 let rec id_list A (l: list A) on l :=
  33   match l with
  34   [ nil => []
  35   | (cons hd tl) => hd :: id_list A tl ]. *)
  36
  37 let rec append A (l1: list A) l2 on l1 ≝
  38   match l1 with
  39   [ nil ⇒  l2
  40   | cons hd tl ⇒  hd :: append A tl l2 ].
  41
  42 definition hd ≝ λA.λl: list A.λd:A.
  43   match l with [ nil ⇒ d | cons a _ ⇒ a].
  44
  45 definition tail ≝  λA.λl: list A.
  46   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
  47
  48 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  49
  50 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
  51 #A #l (elim l) normalize // qed.
  52
  53 theorem associative_append:
  54  ∀A.associative (list A) (append A).
  55 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  56
  57 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
  58 #A #a #l #l1 >associative_append // qed.
  59
  60 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
  61   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
  62 #A #l1 #l2 #P (cases l1) normalize //
  63 #a #l3 #heq destruct
  64 qed.
  65
  66 theorem nil_to_nil:  ∀A.∀l1,l2:list A.
  67   l1@l2 = [] → l1 = [] ∧ l2 = [].
  68 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
  69 qed.
  70
  71 (**************************** iterators ******************************)
  72
  73 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
  74  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
  75
  76 lemma map_append : ∀A,B,f,l1,l2.
  77   (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
  78 #A #B #f #l1 elim l1
  79 [ #l2 @refl
  80 | #h #t #IH #l2 normalize //
  81 ] qed.
  82
  83 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
  84  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  85
  86 definition filter ≝
  87   λT.λp:T → bool.
  88   foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
  89
  90 (* compose f [a1;...;an] [b1;...;bm] =
  91   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
  92
  93 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
  94     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
  95
  96 lemma filter_true : ∀A,l,a,p. p a = true →
  97   filter A p (a::l) = a :: filter A p l.
  98 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
  99
 100 lemma filter_false : ∀A,l,a,p. p a = false →
 101   filter A p (a::l) = filter A p l.
 102 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 103
 104 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 105 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 106
 107 (**************************** reverse *****************************)
 108 let rec rev_append S (l1,l2:list S) on l1 ≝
 109   match l1 with
 110   [ nil ⇒ l2
 111   | cons a tl ⇒ rev_append S tl (a::l2)
 112   ]
 113 .
 114
 115 definition reverse ≝λS.λl.rev_append S l [].
 116
 117 lemma reverse_single : ∀S,a. reverse S [a] = [a].
 118 // qed.
 119
 120 lemma rev_append_def : ∀S,l1,l2.
 121   rev_append S l1 l2 = (reverse S l1) @ l2 .
 122 #S #l1 elim l1 normalize //
 123 qed.
 124
 125 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
 126 #S #a #l whd in ⊢ (??%?); //
 127 qed.
 128
 129 lemma reverse_append: ∀S,l1,l2.
 130   reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
 131 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
 132 >reverse_cons // qed.
 133
 134 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
 135 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
 136 normalize // qed.
 137
 138 (* an elimination principle for lists working on the tail;
 139 useful for strings *)
 140 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
 141 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
 142 #S #P #Pnil #Pstep #l <(reverse_reverse … l)
 143 generalize in match (reverse S l); #l elim l //
 144 #a #tl #H >reverse_cons @Pstep //
 145 qed.
 146
 147 (**************************** length ******************************)
 148
 149 let rec length (A:Type[0]) (l:list A) on l ≝
 150   match l with
 151     [ nil ⇒ O
 152     | cons a tl ⇒ S (length A tl)].
 153
 154 notation "|M|" non associative with precedence 65 for @{'norm $M}.
 155 interpretation "norm" 'norm l = (length ? l).
 156
 157 lemma length_append: ∀A.∀l1,l2:list A.
 158   |l1@l2| = |l1|+|l2|.
 159 #A #l1 elim l1 // normalize /2/
 160 qed.
 161
 162 (****************************** nth ********************************)
 163 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
 164   match n with
 165     [O ⇒ hd A l d
 166     |S m ⇒ nth m A (tail A l) d].
 167
 168 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
 169 #A #a #i elim i normalize //
 170 qed.
 171
 172 (****************************** nth_opt ********************************)
 173 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
 174 match l with
 175 [ nil ⇒ None ?
 176 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
 177 ].
 178
 179 (**************************** All *******************************)
 180
 181 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 182 match l with
 183 [ nil ⇒ True
 184 | cons h t ⇒ P h ∧ All A P t
 185 ].
 186
 187 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
 188 #A #P #Q #H #l elim l normalize //
 189 #h #t #IH * /3/
 190 qed.
 191
 192 lemma All_nth : ∀A,P,n,l.
 193   All A P l →
 194   ∀a.
 195   nth_opt A n l = Some A a →
 196   P a.
 197 #A #P #n elim n
 198 [ * [ #_ #a #E whd in E:(??%?); destruct
 199     | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
 200     ]
 201 | #m #IH *
 202   [ #_ #a #E whd in E:(??%?); destruct
 203   | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
 204   ]
 205 ] qed.
 206
 207 (**************************** Exists *******************************)
 208
 209 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
 210 match l with
 211 [ nil ⇒ False
 212 | cons h t ⇒ (P h) ∨ (Exists A P t)
 213 ].
 214
 215 lemma Exists_append : ∀A,P,l1,l2.
 216   Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
 217 #A #P #l1 elim l1
 218 [ normalize /2/
 219 | #h #t #IH #l2 *
 220   [ #H /3/
 221   | #H cases (IH l2 H) /3/
 222   ]
 223 ] qed.
 224
 225 lemma Exists_append_l : ∀A,P,l1,l2.
 226   Exists A P l1 → Exists A P (l1@l2).
 227 #A #P #l1 #l2 elim l1
 228 [ *
 229 | #h #t #IH *
 230   [ #H %1 @H
 231   | #H %2 @IH @H
 232   ]
 233 ] qed.
 234
 235 lemma Exists_append_r : ∀A,P,l1,l2.
 236   Exists A P l2 → Exists A P (l1@l2).
 237 #A #P #l1 #l2 elim l1
 238 [ #H @H
 239 | #h #t #IH #H %2 @IH @H
 240 ] qed.
 241
 242 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
 243 #A #P #l1 #x #l2 elim l1
 244 [ normalize #H %2 @H
 245 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
 246 qed.
 247
 248 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
 249 #A #P #l1 #x #l2 #H elim l1
 250 [ %1 @H
 251 | #h #t #IH %2 @IH
 252 ] qed.
 253
 254 lemma Exists_map : ∀A,B,P,Q,f,l.
 255 Exists A P l →
 256 (∀a.P a → Q (f a)) →
 257 Exists B Q (map A B f l).
 258 #A #B #P #Q #f #l elim l //
 259 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
 260
 261 lemma Exists_All : ∀A,P,Q,l.
 262   Exists A P l →
 263   All A Q l →
 264   ∃x. P x ∧ Q x.
 265 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
 266 qed.
 267
 268 (**************************** fold *******************************)
 269
 270 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 ≝
 271  match l with
 272   [ nil ⇒ b
 273   | cons a l ⇒
 274      if p a then op (f a) (fold A B op b p f l)
 275      else fold A B op b p f l].
 276
 277 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 278   with precedence 80
 279 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 280
 281 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 282   with precedence 80
 283 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 284
 285 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 286
 287 theorem fold_true:
 288 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
 289   \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 290     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
 291 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 292
 293 theorem fold_false:
 294 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 295 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
 296   \fold[op,nil]_{i ∈ l| p i} (f i).
 297 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 298
 299 theorem fold_filter:
 300 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 301   \fold[op,nil]_{i ∈ l| p i} (f i) =
 302     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
 303 #A #B #a #l #p #op #nil #f elim l //
 304 #a #tl #Hind cases(true_or_false (p a)) #pa
 305   [ >filter_true // > fold_true // >fold_true //
 306   | >filter_false // >fold_false // ]
 307 qed.
 308
 309 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 310   {op :2> A → A → A;
 311    nill:∀a. op nil a = a;
 312    nilr:∀a. op a nil = a;
 313    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 314   }.
 315
 316 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
 317   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
 318     \fold[op,nil]_{i∈(I@J)} (f i).
 319 #A #B #I #J #nil #op #f (elim I) normalize
 320   [>nill //|#a #tl #Hind <assoc //]
 321 qed.
 322