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 ; »"
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 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
141 | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
143 let rec apply_f_neList (T1,T2:Type) (l:ne_list T1) (f:T1 → T2) on l ≝
145 [ ne_nil h ⇒ ne_nil T2 (f h)
146 | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
149 definition fold_right_list ≝
150 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
151 let rec aux (l:list T1) on l ≝
154 | cons h t ⇒ f h (aux t)
158 definition fold_right_neList ≝
159 λT1,T2:Type.λf:T1 → T2 → T2.λacc:T2.
160 let rec aux (nel:ne_list T1) on nel ≝
163 | ne_cons h t ⇒ f h (aux t)
168 definition is_empty_list ≝
169 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
171 definition isb_empty_list ≝
172 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
174 lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
175 unfold isb_empty_list;
176 unfold is_empty_list;
179 [ normalize; autobatch |
180 normalize; autobatch ]
187 definition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
189 definition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
191 lemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
196 [ normalize; autobatch |
197 normalize; autobatch ]
200 definition ltb ≝ λn1,n2:nat.(leb n1 n2) ⊗ (⊖ (eqb n1 n2)).
202 definition geb ≝ λn1,n2:nat.(⊖ (leb n1 n2)) ⊕ (eqb n1 n2).
204 definition gtb ≝ λn1,n2:nat.⊖ (leb n1 n2).