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 nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
  37  match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ].
  38
  39 nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
  40  match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ].
  41
  42 nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
  43  match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].
  44
  45 (* append *)
  46 nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
  47  match l1 with
  48   [ ne_nil hd ⇒ ne_cons A hd l2
  49   | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
  50
  51 notation "hvbox(hd break §§ tl)"
  52   right associative with precedence 46
  53   for @{'ne_cons $hd $tl}.
  54
  55 notation "« list0 x sep ; break £ y break »"
  56   non associative with precedence 90
  57   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
  58
  59 notation "hvbox(l1 break & l2)"
  60   right associative with precedence 47
  61   for @{'ne_append $l1 $l2 }.
  62
  63 interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
  64 interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
  65 interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
  66
  67 (* ************ *)
  68 (* List Utility *)
  69 (* ************ *)
  70
  71 (* listlen *)
  72 nlet rec len_list (T:Type) (l:list T) on l ≝
  73  match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
  74
  75 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
  76  match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
  77
  78 (* vuota? *)
  79 ndefinition is_empty_list ≝
  80 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
  81
  82 ndefinition isb_empty_list ≝
  83 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
  84
  85 ndefinition isnot_empty_list ≝
  86 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
  87
  88 ndefinition isnotb_empty_list ≝
  89 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
  90
  91 (* conversione *)
  92 nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
  93  match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].
  94
  95 nlet rec list_to_neList_aux (T:Type) (l:list T) on l : option (ne_list T) ≝
  96  match l with
  97   [ nil ⇒ None (ne_list T)
  98   | cons h t ⇒ match list_to_neList_aux T t with
  99    [ None ⇒ Some (ne_list T) «£h»
 100    | Some t' ⇒ Some (ne_list T) («£h»&t') ]].
 101
 102 ndefinition list_to_neList ≝
 103 λT:Type.λl:list T.
 104  match l
 105   return λl:list T.isnot_empty_list T l → ne_list T
 106  with
 107   [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect ? p
 108   | cons h t ⇒ λp:isnot_empty_list T (cons T h t).
 109    match list_to_neList_aux T t with
 110     [ None ⇒ «£h»
 111     | Some t' ⇒ «£h»&t'
 112     ]
 113   ].
 114
 115 (* nth elem *)
 116 nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
 117  match l with
 118   [ nil ⇒ None ?
 119   | cons h t ⇒ match n with
 120    [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
 121   ].
 122
 123 nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 124  match nl with
 125   [ ne_nil h ⇒ match n with
 126    [ O ⇒ Some ? h | S _ ⇒ None ? ]
 127   | ne_cons h t ⇒ match n with
 128    [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
 129   ].
 130
 131 nlet rec abs_nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 132  match nl with
 133   [ ne_nil h ⇒ h
 134   | ne_cons h t ⇒ match n with
 135    [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
 136   ].
 137
 138 (* reverse *)
 139 nlet rec reverse_list (T:Type) (l:list T) on l ≝
 140  match l with
 141   [ nil ⇒ nil T
 142   | cons h t ⇒ (reverse_list T t)@[h]
 143   ].
 144
 145 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
 146  match nl with
 147   [ ne_nil h ⇒ ne_nil T h
 148   | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
 149   ].
 150
 151 (* getLast *)
 152 ndefinition get_last_list ≝
 153 λT:Type.λl:list T.match reverse_list T l with
 154  [ nil ⇒ None ?
 155  | cons h _ ⇒ Some ? h ].
 156
 157 ndefinition get_last_neList ≝
 158 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 159  [ ne_nil h ⇒ h
 160  | ne_cons h _ ⇒ h ].
 161
 162 (* cutLast *)
 163 ndefinition cut_last_list ≝
 164 λT:Type.λl:list T.match reverse_list T l with
 165  [ nil ⇒ nil T
 166  | cons _ t ⇒ reverse_list T t ].
 167
 168 ndefinition cut_last_neList ≝
 169 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 170  [ ne_nil h ⇒ ne_nil T h
 171  | ne_cons _ t ⇒ reverse_neList T t ].
 172
 173 (* getFirst *)
 174 ndefinition get_first_list ≝
 175 λT:Type.λl:list T.match l with
 176  [ nil ⇒ None ?
 177  | cons h _ ⇒ Some ? h ].
 178
 179 ndefinition get_first_neList ≝
 180 λT:Type.λnl:ne_list T.match nl with
 181  [ ne_nil h ⇒ h
 182  | ne_cons h _ ⇒ h ].
 183
 184 (* cutFirst *)
 185 ndefinition cut_first_list ≝
 186 λT:Type.λl:list T.match l with
 187  [ nil ⇒ nil T
 188  | cons _ t ⇒ t ].
 189
 190 ndefinition cut_first_neList ≝
 191 λT:Type.λnl:ne_list T.match nl with
 192  [ ne_nil h ⇒ ne_nil T h
 193  | ne_cons _ t ⇒ t ].
 194
 195 (* apply f *)
 196 nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
 197 match l with
 198  [ nil ⇒ nil T2
 199  | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
 200
 201 nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
 202 match nl with
 203  [ ne_nil h ⇒ ne_nil T2 (f h)
 204  | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
 205
 206 (* fold right *)
 207 nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
 208   match l with
 209    [ nil ⇒ acc
 210    | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
 211    ].
 212
 213 nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
 214   match nl with
 215    [ ne_nil h ⇒ f h acc
 216    | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
 217    ].
 218
 219 (* double fold right *)
 220 nlemma fold_right_list2_aux1 :
 221 ∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
 222  #T; #h; #t;
 223  nnormalize;
 224  #H;
 225  napply (nat_destruct_0_S ? H).
 226 nqed.
 227
 228 nlemma fold_right_list2_aux2 :
 229 ∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
 230  #T; #h; #t;
 231  nnormalize;
 232  #H;
 233  napply (nat_destruct_S_0 ? H).
 234 nqed.
 235
 236 nlemma fold_right_list2_aux3 :
 237 ∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
 238  #T; #h; #h'; #t; #t';
 239  napply (list_ind T ??? t);
 240  napply (list_ind T ??? t');
 241  ##[ ##1: nnormalize; #H; napply (refl_eq ??)
 242  ##| ##2: #a; #l'; #H; #H1;
 243           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
 244           nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
 245  ##| ##3: #a; #l'; #H; #H1;
 246           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
 247           nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
 248  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
 249           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
 250           nchange with ((S (len_list T l1)) = (S (len_list T l)));
 251           nrewrite > (nat_destruct_S_S ?? H2);
 252           napply (refl_eq ??)
 253  ##]
 254 nqed.
 255
 256 nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
 257  match l1
 258   return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
 259  with
 260   [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
 261    [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
 262    | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
 263     False_rect ? (fold_right_list2_aux1 T1 h t p)
 264    ]
 265   | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
 266    [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
 267     False_rect ? (fold_right_list2_aux2 T1 h t p)
 268    | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
 269     f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
 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  napply (ne_list_ind T ??? t);
 299  napply (ne_list_ind T ??? 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 ? (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 ? (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 (* ******** *)
 335 (* naturali *)
 336 (* ******** *)
 337
 338 ndefinition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
 339
 340 ndefinition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
 341
 342 ndefinition ltb ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
 343
 344 ndefinition geb ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
 345
 346 ndefinition gtb ≝ λn1,n2:nat.⊖ (le_nat n1 n2).