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

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

Updated Vector / BitVector? files taken from my Matita library.

File size: 10.2 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "Util.ma".
7
8include "Universes/Universes.ma".
9
10include "Datatypes/Nat/Nat.ma".
11include "Datatypes/Nat/Addition.ma".
12include "Datatypes/Nat/Order.ma".
13
14include "Datatypes/Listlike/List/List.ma".
15
16include "Datatypes/Cartesian.ma".
17
18include "Plogic/equality.ma".
19
20(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
21(* The datatype.                                                              *)
22(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
23
24ninductive Vector (A: Type[0]): Nat → Type[0] ≝
25  Empty: Vector A Z
26| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
27
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29(* Syntax.                                                                    *)
30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
31
32notation "hvbox(hd break :: tl)"
33  right associative with precedence 52
34  for @{ 'Cons $hd $tl }.
35 
36interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
37
38notation "hvbox (v break !! n)"
39  non associative with precedence 90
40  for @{ 'get_index $v $n }.
41
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45
46nlet rec get_index (A: Type[0]) (n: Nat)
47                   (v: Vector A n) (m: Nat) on m ≝
48  match m with
49    [ Z ⇒
50      match v with
51        [ Empty ⇒ Nothing A
52        | Cons p hd tl ⇒ Just A hd
53        ]
54    | S o ⇒
55      match v with
56        [ Empty ⇒ Nothing A
57        | Cons p hd tl ⇒ get_index A p tl o
58        ]
59    ].
60   
61interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
62   
63nlet rec set_index (A: Type[0]) (n: Nat)
64                   (v: Vector A n) (m: Nat) (a: A) on m ≝
65  match m with
66    [ Z ⇒
67      match v with
68        [ Empty ⇒ Nothing (Vector A n)
69        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
70        ]
71    | S o ⇒
72      match v with
73        [ Empty ⇒ Nothing (Vector A n)
74        | Cons p hd tl ⇒
75            let settail ≝ set_index A p tl o a in
76              match settail with
77                [ Nothing ⇒ Nothing (Vector A n)
78                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
79                ]
80        ]
81    ].
82    //.
83nqed.
84
85nlet rec drop (A: Type[0]) (n: Nat)
86              (v: Vector A n) (m: Nat) on m ≝
87  match m with
88    [ Z ⇒ Just (Vector A n) v
89    | S o ⇒
90      match v with
91        [ Empty ⇒ Nothing (Vector A n)
92        | Cons p hd tl ⇒ ? (drop A p tl o)
93        ]
94    ].
95    //.
96nqed.
97   
98(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
99(* Folds and builds.                                                          *)
100(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
101   
102nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
103                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
104  match v with
105    [ Empty ⇒ x
106    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
107    ].
108   
109nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
110                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
111  match v with
112    [ Empty ⇒ x
113    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
114    ].
115   
116(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
117(* Maps and zips.                                                             *)
118(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
119
120nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
121             (f: A → B) (v: Vector A n) on v ≝
122  match v with
123    [ Empty ⇒ Empty B
124    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
125    ].
126
127(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
128   currently in there.
129*)
130nlemma eq_rect_Type0_r :
131  ∀A: Type[0].
132  ∀a:A.
133  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
134  #A a P H x p.
135  ngeneralize in match H.
136  ngeneralize in match P.
137  ncases p.
138  //.
139nqed.
140
141nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
142             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
143  (match v return (λx.λr. x = n → Vector C x) with
144    [ Empty ⇒ λ_. Empty C
145    | Cons n hd tl ⇒
146      match q return (λy.λr. S n = y → Vector C (S n)) with
147        [ Empty ⇒ ?
148        | Cons m hd' tl' ⇒
149            λe: S n = S m.
150              (f hd hd') :: (zip_with A B C n f tl ?)
151        ]
152    ])
153    (refl ? n).
154      ##
155        [ #e;
156          ndestruct(e);
157          ##
158        | ndestruct(e);
159          napply tl'
160          ##
161        ]
162nqed.
163
164ndefinition zip ≝
165  λA, B: Type[0].
166  λn: Nat.
167  λv: Vector A n.
168  λq: Vector B n.
169    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
170
171(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
172(* Building vectors from scratch                                              *)
173(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
174
175nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
176  match n return λn. Vector A n with
177    [ Z ⇒ Empty A
178    | S m ⇒ h :: (replicate A m h)
179    ].
180
181nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
182                (v: Vector A n) (q: Vector A m) on v ≝
183  match v return (λn.λv. Vector A (n + m)) with
184    [ Empty ⇒ q
185    | Cons o hd tl ⇒ hd :: (append A o m tl q)
186    ].
187   
188notation "v break @ q"
189  right associative with precedence 47
190  for @{ 'append $v $q }.
191 
192interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
193   
194nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
195                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
196  a ::
197    (match v with
198       [ Empty ⇒ Empty A
199       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
200       ]).
201
202nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
203                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
204  match v with
205    [ Empty ⇒ ?
206    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
207    ].
208    //.
209nqed.
210   
211(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
212(* Other manipulations.                                                       *)
213(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
214   
215nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
216  match v with
217    [ Empty ⇒ Z
218    | Cons n hd tl ⇒ S $ length A n tl
219    ].
220
221nlet rec reverse (A: Type[0]) (n: Nat)
222                 (v: Vector A n) on v ≝
223  match v return (λm.λv. Vector A m) with
224    [ Empty ⇒ Empty A
225    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
226    ].
227    //.
228nqed.
229
230(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
231(* Conversions to and from lists.                                             *)
232(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
233
234nlet rec list_of_vector (A: Type[0]) (n: Nat)
235                        (v: Vector A n) on v ≝
236  match v return λn.λv. List A with
237    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/List/List/List.con(0,1,1) A)
238    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
239    ].
240    //.
241nqed.
242
243nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
244  match l return λl. Vector A (length A l) with
245    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)
246    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
247    ].
248    nnormalize.
249    //.
250    //.
251nqed.
252
253(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
254(* Rotates and shifts.                                                        *)
255(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
256   
257nlet rec rotate_left (A: Type[0]) (n: Nat)
258                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
259  match m with
260    [ Z ⇒ v
261    | S o ⇒
262        match v with
263          [ Empty ⇒ Empty A
264          | Cons p hd tl ⇒
265             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
266          ]
267    ].
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.