]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/compiler/utility.ma
- exclusion binder in local environments allows to complete lfsx_lfsx !
[helm.git] / matita / 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).