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

Last change on this file since 248 was 248, checked in by mulligan, 9 years ago

More changes. Added datatype for addressing modes.

File size: 10.1 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".
13include "Maybe.ma".
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    nrewrite < (succ_plus ? ?).
224    nrewrite > (plus_zero ?).
225    //.
226nqed.
227
228(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
229(* Conversions to and from lists.                                             *)
230(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
231
232nlet rec list_of_vector (A: Type[0]) (n: Nat)
233                        (v: Vector A n) on v ≝
234  match v return λn.λv. List A with
235    [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
236    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
237    ].
238    //.
239nqed.
240
241nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
242  match l return λl. Vector A (length A l) with
243    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
244    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
245    ].
246    nnormalize.
247    //.
248    //.
249nqed.
250
251(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
252(* Rotates and shifts.                                                        *)
253(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
254   
255nlet rec rotate_left (A: Type[0]) (n: Nat)
256                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
257  match m with
258    [ Z ⇒ v
259    | S o ⇒
260        match v with
261          [ Empty ⇒ Empty A
262          | Cons p hd tl ⇒
263             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
264          ]
265    ].
266    nrewrite < (succ_plus ? ?).
267    nrewrite > (plus_zero ?).
268    //.
269nqed.
270
271ndefinition rotate_right ≝
272  λA: Type[0].
273  λn, m: Nat.
274  λv: Vector A n.
275    reverse A n (rotate_left A n m (reverse A n v)).
276   
277ndefinition shift_left_1 ≝
278  λA: Type[0].
279  λn: Nat.
280  λv: Vector A n.
281  λa: A.
282    match v with
283      [ Empty ⇒ ?
284      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
285      ].
286      //.
287nqed.
288
289ndefinition shift_right_1 ≝
290  λA: Type[0].
291  λn: Nat.
292  λv: Vector A n.
293  λa: A.
294    reverse A n (shift_left_1 A n (reverse A n v) a).
295   
296ndefinition shift_left ≝
297  λA: Type[0].
298  λn, m: Nat.
299  λv: Vector A n.
300  λa: A.
301    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
302   
303ndefinition shift_right ≝
304  λA: Type[0].
305  λn, m: Nat.
306  λv: Vector A n.
307  λa: A.
308    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
309   
310(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
311(* Lemmas.                                                                    *)
312(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
313   
314nlemma map_fusion:
315  ∀A, B, C: Type[0].
316  ∀n: Nat.
317  ∀v: Vector A n.
318  ∀f: A → B.
319  ∀g: B → C.
320    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
321  #A B C n v f g.
322  nelim v.
323  nnormalize.
324  @.
325  #N H V H2.
326  nnormalize.
327  nrewrite > H2.
328  @.
329nqed.
330
331nlemma length_correct:
332  ∀A: Type[0].
333  ∀n: Nat.
334  ∀v: Vector A n.
335    length A n v = n.
336  #A n v.
337  nelim v.
338  nnormalize.
339  @.
340  #N H V H2.
341  nnormalize.
342  nrewrite > H2.
343  @.
344nqed.
345
346nlemma map_length:
347  ∀A, B: Type[0].
348  ∀n: Nat.
349  ∀v: Vector A n.
350  ∀f: A → B.
351    length A n v = length B n (map A B n f v).
352  #A B n v f.
353  nelim v.
354  nnormalize.
355  @.
356  #N H V H2.
357  nnormalize.
358  nrewrite > H2.
359  @.
360nqed.
Note: See TracBrowser for help on using the repository browser.