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 "« 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}}.
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_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) ].
70 definition len_list ≝ λT:Type.λl:list T.len_list_aux T l O.
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) ].
75 definition len_neList ≝ λT:Type.λl:ne_list T.len_neList_aux T l O.
78 let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
81 | cons h t ⇒ match n with
82 [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
85 let rec nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
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' ]
93 let rec abs_nth_neList (T:Type) (l:ne_list T) (n:nat) on l ≝
96 | ne_cons h t ⇒ match n with
97 [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
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) ].
104 definition reverse_list ≝ λT:Type.λl:list T.reverse_list_aux T l (nil T).
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) ].
109 definition reverse_neList ≝ λT:Type.λl:ne_list T.
112 | ne_cons h t ⇒ reverse_neList_aux T t (ne_nil T h)
116 definition get_last_list ≝
117 λT:Type.λl:list T.match reverse_list T l with
119 | cons h _ ⇒ Some ? h ].
121 definition get_last_neList ≝
122 λT:Type.λl:ne_list T.match reverse_neList T l with
127 definition cut_last_list ≝
128 λT:Type.λl:list T.match reverse_list T l with
130 | cons _ t ⇒ reverse_list T t ].
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 ].
138 definition get_first_list ≝
139 λT:Type.λl:list T.match l with
141 | cons h _ ⇒ Some ? h ].
143 definition get_first_neList ≝
144 λT:Type.λl:ne_list T.match l with
149 definition cut_first_list ≝
150 λT:Type.λl:list T.match l with
154 definition cut_first_neList ≝
155 λT:Type.λl:ne_list T.match l with
156 [ ne_nil h ⇒ ne_nil T h
160 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
163 | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
165 let rec apply_f_neList (T1,T2:Type) (l:ne_list T1) (f:T1 → T2) on l ≝
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) ].
171 definition fold_right_list ≝
172 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
173 let rec aux (l:list T1) on l ≝
176 | cons h t ⇒ f h (aux t)
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 ≝
185 | ne_cons h t ⇒ f h (aux t)
190 definition is_empty_list ≝
191 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
193 definition isb_empty_list ≝
194 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
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;
201 [ normalize; autobatch |
202 normalize; autobatch ]
209 definition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
211 definition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
213 lemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
218 [ normalize; autobatch |
219 normalize; autobatch ]
222 definition ltb ≝ λn1,n2:nat.(leb n1 n2) ⊗ (⊖ (eqb n1 n2)).
224 definition geb ≝ λn1,n2:nat.(⊖ (leb n1 n2)) ⊕ (eqb n1 n2).
226 definition gtb ≝ λn1,n2:nat.⊖ (leb n1 n2).