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 "« y break £ list0 x sep ; 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_aux (T:Type) (p_l:list T) (c:nat) on p_l ≝
  68  match p_l with [ nil ⇒ c | cons _ t ⇒ len_list_aux T t (S c) ].
  69
  70 definition len_list ≝ λT:Type.λl:list T.len_list_aux T l O.
  71
  72 let rec len_neList_aux (T:Type) (p_l:ne_list T) (c:nat) on p_l ≝
  73  match p_l with [ ne_nil _ ⇒ (S c) | ne_cons _ t ⇒ len_neList_aux T t (S c) ].
  74
  75 definition len_neList ≝ λT:Type.λl:ne_list T.len_neList_aux T l O.
  76
  77 (* nth elem *)
  78 let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
  79  match l with
  80   [ nil ⇒ None ?
  81   | cons h t ⇒ match n with
  82    [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
  83   ].
  84
  85 let rec nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
  86  match l with
  87   [ ne_nil h ⇒ match n with
  88    [ O ⇒ Some ? h | S _ ⇒ None ? ]
  89   | ne_cons h t ⇒ match n with
  90    [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
  91   ].
  92
  93 let rec abs_nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
  94  match l with
  95   [ ne_nil h ⇒ h
  96   | ne_cons h t ⇒ match n with
  97    [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
  98   ].
  99
 100 (* reverse *)
 101 let rec reverse_list_aux (T:Type) (lin:list T) (lout:list T) on lin ≝
 102  match lin with [ nil ⇒ lout | cons h t ⇒ reverse_list_aux T t (h::lout) ].
 103
 104 definition reverse_list ≝ λT:Type.λl:list T.reverse_list_aux T l (nil T).
 105
 106 let rec reverse_neList_aux (T:Type) (lin:ne_list T) (lout:ne_list T) on lin ≝
 107  match lin with [ ne_nil h ⇒ h§§lout | ne_cons h t ⇒ reverse_neList_aux T t (h§§lout) ].
 108
 109 definition reverse_neList ≝ λT:Type.λl:ne_list T.
 110  match l with
 111   [ ne_nil h ⇒ l
 112   | ne_cons h t ⇒ reverse_neList_aux T t (ne_nil T h)
 113   ].
 114
 115 (* getLast *)
 116 definition get_last_list ≝
 117 λT:Type.λl:list T.match reverse_list T l with
 118  [ nil ⇒ None ?
 119  | cons h _ ⇒ Some ? h ].
 120
 121 definition get_last_neList ≝
 122 λT:Type.λl:ne_list T.match reverse_neList T l with
 123  [ ne_nil h ⇒ h
 124  | ne_cons h _ ⇒ h ].
 125
 126 (* cutLast *)
 127 definition cut_last_list ≝
 128 λT:Type.λl:list T.match reverse_list T l with
 129  [ nil ⇒ nil T
 130  | cons _ t ⇒ reverse_list T t ].
 131
 132 definition cut_last_neList ≝
 133 λT:Type.λl:ne_list T.match reverse_neList T l with
 134  [ ne_nil h ⇒ ne_nil T h
 135  | ne_cons _ t ⇒ reverse_neList T t ].
 136
 137 (* getFirst *)
 138 definition get_first_list ≝
 139 λT:Type.λl:list T.match l with
 140  [ nil ⇒ None ?
 141  | cons h _ ⇒ Some ? h ].
 142
 143 definition get_first_neList ≝
 144 λT:Type.λl:ne_list T.match l with
 145  [ ne_nil h ⇒ h
 146  | ne_cons h _ ⇒ h ].
 147
 148 (* cutFirst *)
 149 definition cut_first_list ≝
 150 λT:Type.λl:list T.match l with
 151  [ nil ⇒ nil T
 152  | cons _ t ⇒ t ].
 153
 154 definition cut_first_neList ≝
 155 λT:Type.λl:ne_list T.match l with
 156  [ ne_nil h ⇒ ne_nil T h
 157  | ne_cons _ t ⇒ t ].
 158
 159 (* apply f *)
 160 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
 161 match l with
 162  [ nil ⇒ nil T2
 163  | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
 164
 165 let rec apply_f_neList (T1,T2:Type) (l:ne_list T1) (f:T1 → T2) on l ≝
 166 match l with
 167  [ ne_nil h ⇒ ne_nil T2 (f h)
 168  | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
 169
 170 (* fold right *)
 171 definition fold_right_list ≝
 172 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
 173  let rec aux (l:list T1) on l ≝
 174   match l with
 175    [ nil ⇒ acc
 176    | cons h t ⇒ f h (aux t)
 177    ] in
 178   aux.
 179
 180 definition fold_right_neList ≝
 181 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
 182  let rec aux (nel:ne_list T1) on nel ≝
 183   match nel with
 184    [ ne_nil h ⇒ f h acc
 185    | ne_cons h t ⇒ f h (aux t)
 186    ] in
 187   aux.
 188
 189 (* vuota? *)
 190 definition is_empty_list ≝
 191 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
 192
 193 definition isb_empty_list ≝
 194 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
 195
 196 lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 197  unfold isb_empty_list;
 198  unfold is_empty_list;
 199  intros;
 200  elim l;
 201  [ normalize; autobatch |
 202    normalize; autobatch ]
 203 qed.
 204
 205 (* ******** *)
 206 (* naturali *)
 207 (* ******** *)
 208
 209 definition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
 210
 211 definition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
 212
 213 lemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
 214  unfold isZerob;
 215  unfold isZero;
 216  intros;
 217  elim n;
 218  [ normalize; autobatch |
 219    normalize; autobatch ]
 220 qed.
 221
 222 definition ltb ≝ λn1,n2:nat.(leb n1 n2) ⊗ (⊖ (eqb n1 n2)).
 223
 224 definition geb ≝ λn1,n2:nat.(⊖ (leb n1 n2)) ⊕ (eqb n1 n2).
 225
 226 definition gtb ≝ λn1,n2:nat.⊖ (leb n1 n2).