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 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "freescale/extra.ma".
29 inductive ne_list (A:Type) : Type ≝
30 | ne_nil: A → ne_list A
31 | ne_cons: A → ne_list A → ne_list A.
34 let rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
36 [ ne_nil hd => ne_cons A hd l2
37 | ne_cons hd tl => ne_cons A hd (ne_append A tl l2) ].
39 notation "hvbox(hd break §§ tl)"
40 right associative with precedence 46
41 for @{'ne_cons $hd $tl}.
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}}.
47 notation "hvbox(l1 break & l2)"
48 right associative with precedence 47
49 for @{'ne_append $l1 $l2 }.
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).
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 ].
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') ]].
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) ].
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) ].
74 let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
77 | cons h t ⇒ match n with
78 [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
81 let rec nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
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' ]
89 let rec abs_nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
92 | ne_cons h t ⇒ match n with
93 [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
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) ].
100 definition reverse_list ≝ λT:Type.λl:list T.reverse_list_aux T l (nil T).
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) ].
105 definition reverse_neList ≝ λT:Type.λl:ne_list T.
108 | ne_cons h t ⇒ reverse_neList_aux T t (ne_nil T h)
112 definition get_last_list ≝
113 λT:Type.λl:list T.match reverse_list T l with
115 | cons h _ ⇒ Some ? h ].
117 definition get_last_neList ≝
118 λT:Type.λl:ne_list T.match reverse_neList T l with
123 definition cut_last_list ≝
124 λT:Type.λl:list T.match reverse_list T l with
126 | cons _ t ⇒ reverse_list T t ].
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 ].
134 definition get_first_list ≝
135 λT:Type.λl:list T.match l with
137 | cons h _ ⇒ Some ? h ].
139 definition get_first_neList ≝
140 λT:Type.λl:ne_list T.match l with
145 definition cut_first_list ≝
146 λT:Type.λl:list T.match l with
150 definition cut_first_neList ≝
151 λT:Type.λl:ne_list T.match l with
152 [ ne_nil h ⇒ ne_nil T h
156 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
159 | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
161 let rec apply_f_neList (T1,T2:Type) (l:ne_list T1) (f:T1 → T2) on l ≝
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) ].
167 definition fold_right_list ≝
168 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
169 let rec aux (l:list T1) on l ≝
172 | cons h t ⇒ f h (aux t)
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 ≝
181 | ne_cons h t ⇒ f h (aux t)
186 definition is_empty_list ≝
187 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
189 definition isb_empty_list ≝
190 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
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;
197 [ normalize; autobatch |
198 normalize; autobatch ]
201 definition isnot_empty_list ≝
202 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
204 definition isnotb_empty_list ≝
205 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
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;
212 [ normalize; autobatch |
213 normalize; autobatch ]
216 lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
219 [ 1: intro; reflexivity
220 | 2: intros; normalize in H1:(%); destruct H1
224 lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true.
227 [ 1: intro; reflexivity
228 | 2: intros; destruct H1
236 definition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
238 definition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
240 lemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
245 [ normalize; autobatch |
246 normalize; autobatch ]
249 definition ltb ≝ λn1,n2:nat.(leb n1 n2) ⊗ (⊖ (eqb n1 n2)).
251 definition geb ≝ λn1,n2:nat.(⊖ (leb n1 n2)) ⊕ (eqb n1 n2).
253 definition gtb ≝ λn1,n2:nat.⊖ (leb n1 n2).