matita/matita/contribs/ng_assembly/common/list_utility.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 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/list.ma".
  24 include "common/option.ma".
  25 include "common/nat_lemmas.ma".
  26
  27 (* *************** *)
  28 (* LISTE GENERICHE *)
  29 (* *************** *)
  30
  31 (* listlen *)
  32 nlet rec len_list (T:Type) (l:list T) on l ≝
  33  match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
  34
  35 (* vuota? *)
  36 ndefinition is_empty_list ≝
  37 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
  38
  39 ndefinition isb_empty_list ≝
  40 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
  41
  42 ndefinition isnot_empty_list ≝
  43 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
  44
  45 ndefinition isnotb_empty_list ≝
  46 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
  47
  48 (* reverse *)
  49 nlet rec reverse_list (T:Type) (l:list T) on l ≝
  50  match l with
  51   [ nil ⇒ nil T
  52   | cons h t ⇒ (reverse_list T t)@[h]
  53   ].
  54
  55 (* getFirst *)
  56 ndefinition get_first_list ≝
  57 λT:Type.λl:list T.match l with
  58  [ nil ⇒ None ?
  59  | cons h _ ⇒ Some ? h ].
  60
  61 (* getLast *)
  62 ndefinition get_last_list ≝
  63 λT:Type.λl:list T.match reverse_list T l with
  64  [ nil ⇒ None ?
  65  | cons h _ ⇒ Some ? h ].
  66
  67 (* cutFirst *)
  68 ndefinition cut_first_list ≝
  69 λT:Type.λl:list T.match l with
  70  [ nil ⇒ nil T
  71  | cons _ t ⇒ t ].
  72
  73 (* cutLast *)
  74 ndefinition cut_last_list ≝
  75 λT:Type.λl:list T.match reverse_list T l with
  76  [ nil ⇒ nil T
  77  | cons _ t ⇒ reverse_list T t ].
  78
  79 (* apply f *)
  80 nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
  81 match l with
  82  [ nil ⇒ nil T2
  83  | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
  84
  85 (* fold right *)
  86 nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
  87   match l with
  88    [ nil ⇒ acc
  89    | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
  90    ].
  91
  92 (* double fold right *)
  93 nlemma fold_right_list2_aux1 :
  94 ∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
  95  #T; #h; #t;
  96  nnormalize;
  97  #H;
  98  ndestruct (*napply (nat_destruct_0_S ? H)*).
  99 nqed.
 100
 101 nlemma fold_right_list2_aux2 :
 102 ∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
 103  #T; #h; #t;
 104  nnormalize;
 105  #H;
 106  ndestruct (*napply (nat_destruct_S_0 ? H)*).
 107 nqed.
 108
 109 nlemma fold_right_list2_aux3 :
 110 ∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
 111  #T; #h; #h'; #t; #t';
 112  nelim t;
 113  nelim t';
 114  ##[ ##1: nnormalize; #H; napply refl_eq
 115  ##| ##2: #a; #l'; #H; #H1;
 116           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
 117           ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
 118  ##| ##3: #a; #l'; #H; #H1;
 119           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
 120           ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
 121  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
 122           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
 123           nchange with ((S (len_list T l1)) = (S (len_list T l)));
 124           nrewrite > (nat_destruct_S_S … H2);
 125           napply refl_eq
 126  ##]
 127 nqed.
 128
 129 nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
 130  match l1
 131   return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
 132  with
 133   [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
 134    [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
 135    | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
 136     False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
 137    ]
 138   | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
 139    [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
 140     False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
 141    | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
 142     f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
 143    ]
 144   ].
 145
 146 nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝
 147  match l1 with
 148   [ nil ⇒ match l2 with
 149    [ nil ⇒ true | cons h t ⇒ false ]
 150   | cons h t ⇒ match l2 with
 151    [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t')
 152    ]
 153   ].
 154
 155 (* nth elem *)
 156 nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
 157  match l with
 158   [ nil ⇒ None ?
 159   | cons h t ⇒ match n with
 160    [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
 161   ].
 162
 163 (* abs elem *)
 164 ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
 165  #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
 166
 167 ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
 168  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 169
 170 nlet rec abs_list (T:Type) (l:list T) on l ≝
 171  match l
 172   return λl.Πn.(((len_list T l) > n) = true) → T
 173  with
 174   [ nil ⇒ λn.λp:(((len_list T []) > n) = true).False_rect_Type0 ? (abs_list_aux1 T n p)
 175   | cons h t ⇒ λn.
 176    match n with
 177     [ O ⇒ λp:(((len_list T (h::t)) > O) = true).h
 178     | S n' ⇒ λp:(((len_list T (h::t)) > (S n')) = true).
 179      abs_list T t n' (abs_list_aux2 T h t n' p)
 180     ]
 181   ].
 182
 183 (* esempio: abs_list ? [ 1; 2; 3; 4 ] 2 (refl_eq …) = 0. *)
 184
 185 (* ************** *)
 186 (* NON-EMPTY LIST *)
 187 (* ************** *)
 188
 189 (* listlen *)
 190 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
 191  match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
 192
 193 (* reverse *)
 194 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
 195  match nl with
 196   [ ne_nil h ⇒ ne_nil T h
 197   | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
 198   ].
 199
 200 (* getFirst *)
 201 ndefinition get_first_neList ≝
 202 λT:Type.λnl:ne_list T.match nl with
 203  [ ne_nil h ⇒ h
 204  | ne_cons h _ ⇒ h ].
 205
 206 (* getLast *)
 207 ndefinition get_last_neList ≝
 208 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 209  [ ne_nil h ⇒ h
 210  | ne_cons h _ ⇒ h ].
 211
 212 (* cutFirst *)
 213 ndefinition cut_first_neList ≝
 214 λT:Type.λnl:ne_list T.match nl with
 215  [ ne_nil h ⇒ ne_nil T h
 216  | ne_cons _ t ⇒ t ].
 217
 218 (* cutLast *)
 219 ndefinition cut_last_neList ≝
 220 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 221  [ ne_nil h ⇒ ne_nil T h
 222  | ne_cons _ t ⇒ reverse_neList T t ].
 223
 224 (* apply f *)
 225 nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
 226 match nl with
 227  [ ne_nil h ⇒ ne_nil T2 (f h)
 228  | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
 229
 230 (* fold right *)
 231 nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
 232   match nl with
 233    [ ne_nil h ⇒ f h acc
 234    | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
 235    ].
 236
 237 (* double fold right *)
 238 nlemma fold_right_neList2_aux1 :
 239 ∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
 240  #T; #h; #h'; #t';
 241  nnormalize;
 242  ncases t';
 243  nnormalize;
 244  ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
 245  ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
 246  ##]
 247 nqed.
 248
 249 nlemma fold_right_neList2_aux2 :
 250 ∀T.∀h,h',t.len_neList T (h§§t) = len_neList T «£h'» → False.
 251  #T; #h; #h'; #t;
 252  nnormalize;
 253  ncases t;
 254  nnormalize;
 255  ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
 256  ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
 257  ##]
 258 nqed.
 259
 260 nlemma fold_right_neList2_aux3 :
 261 ∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
 262  #T; #h; #h'; #t; #t';
 263  nelim t;
 264  nelim t';
 265  ##[ ##1: nnormalize; #x; #y; #H; napply refl_eq
 266  ##| ##2: #a; #l'; #H; #x; #H1;
 267           nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
 268           nrewrite > (nat_destruct_S_S … H1);
 269           napply refl_eq
 270  ##| ##3: #x; #a; #l'; #H; #H1;
 271           nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
 272           nrewrite > (nat_destruct_S_S … H1);
 273           napply refl_eq
 274  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
 275           nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
 276           nrewrite > (nat_destruct_S_S … H2);
 277           napply refl_eq
 278  ##]
 279 nqed.
 280
 281 nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:ne_list T1) on l1 ≝
 282  match l1
 283   return λl1.Πl2.len_neList T1 l1 = len_neList T1 l2 → T2
 284  with
 285   [ ne_nil h ⇒ λl2.match l2 return λl2.len_neList T1 «£h» = len_neList T1 l2 → T2 with
 286    [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
 287     f h h' acc
 288    | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
 289     False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
 290    ]
 291   | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
 292    [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
 293     False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
 294    | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
 295     f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
 296    ]
 297   ].
 298
 299 nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝
 300  match l1 with
 301   [ ne_nil h ⇒ match l2 with
 302    [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ]
 303   | ne_cons h t ⇒ match l2 with
 304    [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t')
 305    ]
 306   ].
 307
 308 (* nth elem *)
 309 nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 310  match nl with
 311   [ ne_nil h ⇒ match n with
 312    [ O ⇒ Some ? h | S _ ⇒ None ? ]
 313   | ne_cons h t ⇒ match n with
 314    [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
 315   ].
 316
 317 (* abs elem *)
 318 ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
 319  #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
 320
 321 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
 322  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 323
 324 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
 325  match l
 326   return λl.Πn.(((len_neList T l) > n) = true) → T
 327  with
 328   [ ne_nil h ⇒ λn.
 329    match n
 330     return λn.(((len_neList T (ne_nil T h)) > n) = true) → T
 331    with
 332     [ O ⇒ λp:(((len_neList T (ne_nil T h)) > O) = true).h
 333     | S n' ⇒ λp:(((len_neList T (ne_nil T h)) > (S n')) = true).
 334      False_rect_Type0 ? (abs_neList_aux1 T h n' p)
 335     ]
 336   | ne_cons h t ⇒ λn.
 337    match n with
 338     [ O ⇒ λp:(((len_neList T (ne_cons T h t)) > O) = true).h
 339     | S n' ⇒ λp:(((len_neList T (ne_cons T h t)) > (S n')) = true).
 340      abs_neList T t n' (abs_neList_aux2 T h t n' p)
 341     ]
 342   ].
 343
 344 (* esempio: abs_neList ? « 1; 2; 3 £ 4 » 0 (refl_eq …) = 0. *)
 345
 346 (* conversione *)
 347 nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
 348  match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].