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