1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "common/list.ma".
24 include "common/option.ma".
25 include "common/nat_lemmas.ma".
32 nlet rec len_list (T:Type) (l:list T) on l ≝
33 match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
36 ndefinition is_empty_list ≝
37 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
39 ndefinition isb_empty_list ≝
40 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
42 ndefinition isnot_empty_list ≝
43 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
45 ndefinition isnotb_empty_list ≝
46 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
49 nlet rec reverse_list (T:Type) (l:list T) on l ≝
52 | cons h t ⇒ (reverse_list T t)@[h]
56 ndefinition get_first_list ≝
57 λT:Type.λl:list T.match l with
59 | cons h _ ⇒ Some ? h ].
62 ndefinition get_last_list ≝
63 λT:Type.λl:list T.match reverse_list T l with
65 | cons h _ ⇒ Some ? h ].
68 ndefinition cut_first_list ≝
69 λT:Type.λl:list T.match l with
74 ndefinition cut_last_list ≝
75 λT:Type.λl:list T.match reverse_list T l with
77 | cons _ t ⇒ reverse_list T t ].
80 nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
83 | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
86 nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
89 | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
92 (* double fold right *)
93 nlemma fold_right_list2_aux1 :
94 ∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
98 napply (nat_destruct_0_S ? H).
101 nlemma fold_right_list2_aux2 :
102 ∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
106 napply (nat_destruct_S_0 ? H).
109 nlemma fold_right_list2_aux3 :
110 ∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
111 #T; #h; #h'; #t; #t';
114 ##[ ##1: nnormalize; #H; napply refl_eq
115 ##| ##2: #a; #l'; #H; #H1;
116 nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
117 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
118 ##| ##3: #a; #l'; #H; #H1;
119 nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
120 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
121 ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
122 nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
123 nchange with ((S (len_list T l1)) = (S (len_list T l)));
124 nrewrite > (nat_destruct_S_S … H2);
129 nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
131 return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
133 [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
134 [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
135 | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
136 False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
138 | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
139 [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
140 False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
141 | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
142 f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
146 nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝
148 [ nil ⇒ match l2 with
149 [ nil ⇒ true | cons h t ⇒ false ]
150 | cons h t ⇒ match l2 with
151 [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t')
156 nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
159 | cons h t ⇒ match n with
160 [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
164 ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
165 #T; nnormalize; #n; #H; napply (bool_destruct … H). nqed.
167 ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
168 #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
170 nlet rec abs_list (T:Type) (l:list T) on l ≝
172 return λl.Πn.(((len_list T l) > n) = true) → T
174 [ nil ⇒ λn.λp:(((len_list T []) > n) = true).False_rect_Type0 ? (abs_list_aux1 T n p)
177 [ O ⇒ λp:(((len_list T (h::t)) > O) = true).h
178 | S n' ⇒ λp:(((len_list T (h::t)) > (S n')) = true).
179 abs_list T t n' (abs_list_aux2 T h t n' p)
183 (* esempio: abs_list ? [ 1; 2; 3; 4 ] 2 (refl_eq …) = 0. *)
190 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
191 match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
194 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
196 [ ne_nil h ⇒ ne_nil T h
197 | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
201 ndefinition get_first_neList ≝
202 λT:Type.λnl:ne_list T.match nl with
207 ndefinition get_last_neList ≝
208 λT:Type.λnl:ne_list T.match reverse_neList T nl with
213 ndefinition cut_first_neList ≝
214 λT:Type.λnl:ne_list T.match nl with
215 [ ne_nil h ⇒ ne_nil T h
219 ndefinition cut_last_neList ≝
220 λT:Type.λnl:ne_list T.match reverse_neList T nl with
221 [ ne_nil h ⇒ ne_nil T h
222 | ne_cons _ t ⇒ reverse_neList T t ].
225 nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
227 [ ne_nil h ⇒ ne_nil T2 (f h)
228 | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
231 nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
234 | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
237 (* double fold right *)
238 nlemma fold_right_neList2_aux1 :
239 ∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
244 ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
245 ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
249 nlemma fold_right_neList2_aux2 :
250 ∀T.∀h,h',t.len_neList T (h§§t) = len_neList T «£h'» → False.
255 ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
256 ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
260 nlemma fold_right_neList2_aux3 :
261 ∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
262 #T; #h; #h'; #t; #t';
265 ##[ ##1: nnormalize; #x; #y; #H; napply refl_eq
266 ##| ##2: #a; #l'; #H; #x; #H1;
267 nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
268 nrewrite > (nat_destruct_S_S … H1);
270 ##| ##3: #x; #a; #l'; #H; #H1;
271 nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
272 nrewrite > (nat_destruct_S_S … H1);
274 ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
275 nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
276 nrewrite > (nat_destruct_S_S … H2);
281 nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:ne_list T1) on l1 ≝
283 return λl1.Πl2.len_neList T1 l1 = len_neList T1 l2 → T2
285 [ ne_nil h ⇒ λl2.match l2 return λl2.len_neList T1 «£h» = len_neList T1 l2 → T2 with
286 [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
288 | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
289 False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
291 | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
292 [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
293 False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
294 | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
295 f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
299 nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝
301 [ ne_nil h ⇒ match l2 with
302 [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ]
303 | ne_cons h t ⇒ match l2 with
304 [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t')
309 nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
311 [ ne_nil h ⇒ match n with
312 [ O ⇒ Some ? h | S _ ⇒ None ? ]
313 | ne_cons h t ⇒ match n with
314 [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
318 ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
319 #T; #h; #n; nnormalize; #H; napply (bool_destruct … H). nqed.
321 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
322 #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
324 naxiom daemon : False.
326 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
328 return λl.Πn.(((len_neList T l) > n) = true) → T
332 return λn.(((len_neList T (ne_nil T h)) > n) = true) → T
334 [ O ⇒ λp:(((len_neList T (ne_nil T h)) > O) = true).h
335 | S n' ⇒ λp:(((len_neList T (ne_nil T h)) > (S n')) = true).
336 False_rect_Type0 ? (abs_neList_aux1 T h n' p)
340 [ O ⇒ λp:(((len_neList T (ne_cons T h t)) > O) = true).h
341 | S n' ⇒ λp:(((len_neList T (ne_cons T h t)) > (S n')) = true).
342 abs_neList T t n' (abs_neList_aux2 T h t n' p)
346 (* esempio: abs_neList ? « 1; 2; 3 £ 4 » 0 (refl_eq …) = 0. *)
349 nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
350 match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].