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