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

Last change on this file since 246 was 246, checked in by mulligan, 9 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.