source: Deliverables/D4.1/Matita/Vector.ma @ 246

Last change on this file since 246 was 246, checked in by mulligan, 10 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.
File size: 10.0 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "Util.ma".
7
8include "Universes.ma".
9
10include "Nat.ma".
11include "List.ma".
12include "Cartesian.ma".
13
14include "Equality.ma".
15
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17(* The datatype.                                                              *)
18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19
20ninductive Vector (A: Type[0]): Nat → Type[0] ≝
21  Empty: Vector A Z
22| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
23
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25(* Syntax.                                                                    *)
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27
28notation "hvbox(hd break :: tl)"
29  right associative with precedence 52
30  for @{ 'Cons $hd $tl }.
31 
32interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
33
34notation "hvbox (v break !! n)"
35  non associative with precedence 90
36  for @{ 'get_index $v $n }.
37
38(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
39(* Lookup.                                                                    *)
40(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
41
42nlet rec get_index (A: Type[0]) (n: Nat)
43                   (v: Vector A n) (m: Nat) on m ≝
44  match m with
45    [ Z ⇒
46      match v with
47        [ Empty ⇒ Nothing A
48        | Cons p hd tl ⇒ Just A hd
49        ]
50    | S o ⇒
51      match v with
52        [ Empty ⇒ Nothing A
53        | Cons p hd tl ⇒ get_index A p tl o
54        ]
55    ].
56   
57interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
58   
59nlet rec set_index (A: Type[0]) (n: Nat)
60                   (v: Vector A n) (m: Nat) (a: A) on m ≝
61  match m with
62    [ Z ⇒
63      match v with
64        [ Empty ⇒ Nothing (Vector A n)
65        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
66        ]
67    | S o ⇒
68      match v with
69        [ Empty ⇒ Nothing (Vector A n)
70        | Cons p hd tl ⇒
71            let settail ≝ set_index A p tl o a in
72              match settail with
73                [ Nothing ⇒ Nothing (Vector A n)
74                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
75                ]
76        ]
77    ].
78    //.
79nqed.
80
81nlet rec drop (A: Type[0]) (n: Nat)
82              (v: Vector A n) (m: Nat) on m ≝
83  match m with
84    [ Z ⇒ Just (Vector A n) v
85    | S o ⇒
86      match v with
87        [ Empty ⇒ Nothing (Vector A n)
88        | Cons p hd tl ⇒ ? (drop A p tl o)
89        ]
90    ].
91    //.
92nqed.
93   
94(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
95(* Folds and builds.                                                          *)
96(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
97   
98nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
99                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
100  match v with
101    [ Empty ⇒ x
102    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
103    ].
104   
105nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
106                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
107  match v with
108    [ Empty ⇒ x
109    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
110    ].
111   
112(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
113(* Maps and zips.                                                             *)
114(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
115
116nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
117             (f: A → B) (v: Vector A n) on v ≝
118  match v with
119    [ Empty ⇒ Empty B
120    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
121    ].
122
123(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
124   currently in there.
125*)
126nlemma eq_rect_Type0_r :
127  ∀A: Type[0].
128  ∀a:A.
129  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
130  #A a P H x p.
131  ngeneralize in match H.
132  ngeneralize in match P.
133  ncases p.
134  //.
135nqed.
136
137nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
138             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
139  (match v return (λx.λr. x = n → Vector C x) with
140    [ Empty ⇒ λ_. Empty C
141    | Cons n hd tl ⇒
142      match q return (λy.λr. S n = y → Vector C (S n)) with
143        [ Empty ⇒ ?
144        | Cons m hd' tl' ⇒
145            λe: S n = S m.
146              (f hd hd') :: (zip_with A B C n f tl ?)
147        ]
148    ])
149    (refl ? n).
150      ##
151        [ #e;
152          ndestruct(e);
153          ##
154        | ndestruct(e);
155          napply tl'
156          ##
157        ]
158nqed.
159
160ndefinition zip ≝
161  λA, B: Type[0].
162  λn: Nat.
163  λv: Vector A n.
164  λq: Vector B n.
165    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
166
167(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
168(* Building vectors from scratch                                              *)
169(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
170
171nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
172  match n return λn. Vector A n with
173    [ Z ⇒ Empty A
174    | S m ⇒ h :: (replicate A m h)
175    ].
176
177nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
178                (v: Vector A n) (q: Vector A m) on v ≝
179  match v return (λn.λv. Vector A (n + m)) with
180    [ Empty ⇒ q
181    | Cons o hd tl ⇒ hd :: (append A o m tl q)
182    ].
183   
184notation "v break @ q"
185  right associative with precedence 47
186  for @{ 'append $v $q }.
187 
188interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
189   
190nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
191                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
192  a ::
193    (match v with
194       [ Empty ⇒ Empty A
195       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
196       ]).
197
198nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
199                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
200  match v with
201    [ Empty ⇒ ?
202    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
203    ].
204    //.
205nqed.
206   
207(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
208(* Other manipulations.                                                       *)
209(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
210   
211nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
212  match v with
213    [ Empty ⇒ Z
214    | Cons n hd tl ⇒ S $ length A n tl
215    ].
216
217nlet rec reverse (A: Type[0]) (n: Nat)
218                 (v: Vector A n) on v ≝
219  match v return (λm.λv. Vector A m) with
220    [ Empty ⇒ Empty A
221    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
222    ].
223    //.
224nqed.
225
226(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
227(* Conversions to and from lists.                                             *)
228(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
229
230nlet rec list_of_vector (A: Type[0]) (n: Nat)
231                        (v: Vector A n) on v ≝
232  match v return λn.λv. List A with
233    [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
234    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
235    ].
236    //.
237nqed.
238
239nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
240  match l return λl. Vector A (length A l) with
241    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
242    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
243    ].
244    nnormalize.
245    //.
246    //.
247nqed.
248
249(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
250(* Rotates and shifts.                                                        *)
251(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
252   
253nlet rec rotate_left (A: Type[0]) (n: Nat)
254                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
255  match m with
256    [ Z ⇒ v
257    | S o ⇒
258        match v with
259          [ Empty ⇒ Empty A
260          | Cons p hd tl ⇒
261             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
262          ]
263    ].
264    //.
265nqed.
266
267ndefinition rotate_right ≝
268  λA: Type[0].
269  λn, m: Nat.
270  λv: Vector A n.
271    reverse A n (rotate_left A n m (reverse A n v)).
272   
273ndefinition shift_left_1 ≝
274  λA: Type[0].
275  λn: Nat.
276  λv: Vector A n.
277  λa: A.
278    match v with
279      [ Empty ⇒ ?
280      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
281      ].
282      //.
283nqed.
284
285ndefinition shift_right_1 ≝
286  λA: Type[0].
287  λn: Nat.
288  λv: Vector A n.
289  λa: A.
290    reverse A n (shift_left_1 A n (reverse A n v) a).
291   
292ndefinition shift_left ≝
293  λA: Type[0].
294  λn, m: Nat.
295  λv: Vector A n.
296  λa: A.
297    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
298   
299ndefinition shift_right ≝
300  λA: Type[0].
301  λn, m: Nat.
302  λv: Vector A n.
303  λa: A.
304    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
305   
306(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
307(* Lemmas.                                                                    *)
308(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
309   
310nlemma map_fusion:
311  ∀A, B, C: Type[0].
312  ∀n: Nat.
313  ∀v: Vector A n.
314  ∀f: A → B.
315  ∀g: B → C.
316    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
317  #A B C n v f g.
318  nelim v.
319  nnormalize.
320  @.
321  #N H V H2.
322  nnormalize.
323  nrewrite > H2.
324  @.
325nqed.
326
327nlemma length_correct:
328  ∀A: Type[0].
329  ∀n: Nat.
330  ∀v: Vector A n.
331    length A n v = n.
332  #A n v.
333  nelim v.
334  nnormalize.
335  @.
336  #N H V H2.
337  nnormalize.
338  nrewrite > H2.
339  @.
340nqed.
341
342nlemma map_length:
343  ∀A, B: Type[0].
344  ∀n: Nat.
345  ∀v: Vector A n.
346  ∀f: A → B.
347    length A n v = length B n (map A B n f v).
348  #A B n v f.
349  nelim v.
350  nnormalize.
351  @.
352  #N H V H2.
353  nnormalize.
354  nrewrite > H2.
355  @.
356nqed.
Note: See TracBrowser for help on using the repository browser.