helm/software/matita/contribs/assembly/compiler/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 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "freescale/extra.ma".
  23
  24 (* ************** *)
  25 (* Non-Empty List *)
  26 (* ************** *)
  27
  28 (* lista non vuota *)
  29 inductive ne_list (A:Type) : Type ≝
  30   | ne_nil: A → ne_list A
  31   | ne_cons: A → ne_list A → ne_list A.
  32
  33 (* append *)
  34 let rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
  35  match l1 with
  36   [ ne_nil hd => ne_cons A hd l2
  37   | ne_cons hd tl => ne_cons A hd (ne_append A tl l2) ].
  38
  39 notation "hvbox(hd break §§ tl)"
  40   right associative with precedence 46
  41   for @{'ne_cons $hd $tl}.
  42
  43 notation "« list0 x sep ; break £ y break »"
  44   non associative with precedence 90
  45   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
  46
  47 notation "hvbox(l1 break & l2)"
  48   right associative with precedence 47
  49   for @{'ne_append $l1 $l2 }.
  50
  51 interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
  52 interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
  53 interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
  54
  55 (* ************ *)
  56 (* List Utility *)
  57 (* ************ *)
  58
  59 (* conversione *)
  60 let rec neList_to_list (T:Type) (p_l:ne_list T) on p_l ≝
  61  match p_l with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@neList_to_list T t ].
  62
  63 let rec list_to_neList (T:Type) (p_l:list T) on p_l ≝
  64  match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «£h» | Some t' ⇒ Some ? («£h»&t') ]].
  65
  66 (* listlen *)
  67 let rec len_list (T:Type) (p_l:list T) on p_l ≝
  68  match p_l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
  69
  70 let rec len_neList (T:Type) (p_l:ne_list T) on p_l ≝
  71  match p_l with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
  72
  73 (* nth elem *)
  74 let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
  75  match l with
  76   [ nil ⇒ None ?
  77   | cons h t ⇒ match n with
  78    [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
  79   ].
  80
  81 let rec nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
  82  match l with
  83   [ ne_nil h ⇒ match n with
  84    [ O ⇒ Some ? h | S _ ⇒ None ? ]
  85   | ne_cons h t ⇒ match n with
  86    [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
  87   ].
  88
  89 let rec abs_nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
  90  match l with
  91   [ ne_nil h ⇒ h
  92   | ne_cons h t ⇒ match n with
  93    [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
  94   ].
  95
  96 (* reverse *)
  97 let rec reverse_list_aux (T:Type) (lin:list T) (lout:list T) on lin ≝
  98  match lin with [ nil ⇒ lout | cons h t ⇒ reverse_list_aux T t (h::lout) ].
  99
 100 definition reverse_list ≝ λT:Type.λl:list T.reverse_list_aux T l (nil T).
 101
 102 let rec reverse_neList_aux (T:Type) (lin:ne_list T) (lout:ne_list T) on lin ≝
 103  match lin with [ ne_nil h ⇒ h§§lout | ne_cons h t ⇒ reverse_neList_aux T t (h§§lout) ].
 104
 105 definition reverse_neList ≝ λT:Type.λl:ne_list T.
 106  match l with
 107   [ ne_nil h ⇒ l
 108   | ne_cons h t ⇒ reverse_neList_aux T t (ne_nil T h)
 109   ].
 110
 111 (* getLast *)
 112 definition get_last_list ≝
 113 λT:Type.λl:list T.match reverse_list T l with
 114  [ nil ⇒ None ?
 115  | cons h _ ⇒ Some ? h ].
 116
 117 definition get_last_neList ≝
 118 λT:Type.λl:ne_list T.match reverse_neList T l with
 119  [ ne_nil h ⇒ h
 120  | ne_cons h _ ⇒ h ].
 121
 122 (* cutLast *)
 123 definition cut_last_list ≝
 124 λT:Type.λl:list T.match reverse_list T l with
 125  [ nil ⇒ nil T
 126  | cons _ t ⇒ reverse_list T t ].
 127
 128 definition cut_last_neList ≝
 129 λT:Type.λl:ne_list T.match reverse_neList T l with
 130  [ ne_nil h ⇒ ne_nil T h
 131  | ne_cons _ t ⇒ reverse_neList T t ].
 132
 133 (* getFirst *)
 134 definition get_first_list ≝
 135 λT:Type.λl:list T.match l with
 136  [ nil ⇒ None ?
 137  | cons h _ ⇒ Some ? h ].
 138
 139 definition get_first_neList ≝
 140 λT:Type.λl:ne_list T.match l with
 141  [ ne_nil h ⇒ h
 142  | ne_cons h _ ⇒ h ].
 143
 144 (* cutFirst *)
 145 definition cut_first_list ≝
 146 λT:Type.λl:list T.match l with
 147  [ nil ⇒ nil T
 148  | cons _ t ⇒ t ].
 149
 150 definition cut_first_neList ≝
 151 λT:Type.λl:ne_list T.match l with
 152  [ ne_nil h ⇒ ne_nil T h
 153  | ne_cons _ t ⇒ t ].
 154
 155 (* apply f *)
 156 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
 157 match l with
 158  [ nil ⇒ nil T2
 159  | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
 160
 161 let rec apply_f_neList (T1,T2:Type) (l:ne_list T1) (f:T1 → T2) on l ≝
 162 match l with
 163  [ ne_nil h ⇒ ne_nil T2 (f h)
 164  | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
 165
 166 (* fold right *)
 167 definition fold_right_list ≝
 168 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
 169  let rec aux (l:list T1) on l ≝
 170   match l with
 171    [ nil ⇒ acc
 172    | cons h t ⇒ f h (aux t)
 173    ] in
 174   aux.
 175
 176 definition fold_right_neList ≝
 177 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
 178  let rec aux (nel:ne_list T1) on nel ≝
 179   match nel with
 180    [ ne_nil h ⇒ f h acc
 181    | ne_cons h t ⇒ f h (aux t)
 182    ] in
 183   aux.
 184
 185 (* vuota? *)
 186 definition is_empty_list ≝
 187 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
 188
 189 definition isb_empty_list ≝
 190 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
 191
 192 lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 193  unfold isb_empty_list;
 194  unfold is_empty_list;
 195  intros;
 196  elim l;
 197  [ normalize; autobatch |
 198    normalize; autobatch ]
 199 qed.
 200
 201 definition isnot_empty_list ≝
 202 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
 203
 204 definition isnotb_empty_list ≝
 205 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
 206
 207 lemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 208  unfold isnotb_empty_list;
 209  unfold isnot_empty_list;
 210  intros;
 211  elim l;
 212  [ normalize; autobatch |
 213    normalize; autobatch ]
 214 qed.
 215
 216 lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
 217  do 2 intro;
 218  elim l 0;
 219  [ 1: intro; reflexivity
 220  | 2: intros; normalize in H1:(%); destruct H1
 221  ].
 222 qed.
 223
 224 lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true.
 225  do 2 intro;
 226  elim l 0;
 227  [ 1: intro; reflexivity
 228  | 2: intros; destruct H1
 229  ]
 230 qed.
 231
 232 (* ******** *)
 233 (* naturali *)
 234 (* ******** *)
 235
 236 definition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
 237
 238 definition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
 239
 240 lemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
 241  unfold isZerob;
 242  unfold isZero;
 243  intros;
 244  elim n;
 245  [ normalize; autobatch |
 246    normalize; autobatch ]
 247 qed.
 248
 249 definition ltb ≝ λn1,n2:nat.(leb n1 n2) ⊗ (⊖ (eqb n1 n2)).
 250
 251 definition geb ≝ λn1,n2:nat.(⊖ (leb n1 n2)) ⊕ (eqb n1 n2).
 252
 253 definition gtb ≝ λn1,n2:nat.⊖ (leb n1 n2).