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

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

Changes to bitvector.

File size: 11.4 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 "Plogic/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 "[[ list0 x sep ; ]]"
29  non associative with precedence 90
30  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
31
32interpretation "Vector vnil" 'vnil = (Empty ?).
33interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
34interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
35
36(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
37(* Lookup.                                                                    *)
38(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
39
40naxiom succ_less_than_injective:
41  ∀m, n: Nat.
42    less_than_p (S m) (S n) → m < n.
43   
44naxiom nothing_less_than_Z:
45  ∀m: Nat.
46    ¬(m < Z).
47
48nlet rec get_index (A: Type[0]) (n: Nat)
49                   (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
50  (match m with
51    [ Z ⇒
52      match v return λx.λ_. Z < x → A with
53        [ Empty ⇒ λabsd1: Z < Z. ?
54        | Cons p hd tl ⇒ λprf1: Z < S p. hd
55        ]
56    | S o ⇒
57      (match v return λx.λ_. S o < x → A with
58        [ Empty ⇒ λprf: S o < Z. ?
59        | Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?
60        ])
61    ]) lt.
62    ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1)
63    ##| ncases (nothing_less_than_Z (S o)); #K; ncases (K prf)
64    ##| napply succ_less_than_injective; nassumption
65    ##]
66nqed.
67
68nlet rec get_index_weak (A: Type[0]) (n: Nat)
69                   (v: Vector A n) (m: Nat) on m ≝
70  match m with
71    [ Z ⇒
72      match v with
73        [ Empty ⇒ Nothing A
74        | Cons p hd tl ⇒ Just A hd
75        ]
76    | S o ⇒
77      match v with
78        [ Empty ⇒ Nothing A
79        | Cons p hd tl ⇒ get_index_weak A p tl o
80        ]
81    ].
82   
83interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
84
85nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
86  (match m with
87    [ Z ⇒
88      match v return λx.λ_. Z < x → Vector A x with
89        [ Empty ⇒ λabsd1: Z < Z. Empty A
90        | Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl)
91        ]
92    | S o ⇒
93      (match v return λx.λ_. S o < x → Vector A x with
94        [ Empty ⇒ λprf: S o < Z. Empty A
95        | Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?)
96        ])
97    ]) lt.
98    napply succ_less_than_injective.
99    nassumption.
100nqed.
101   
102nlet rec set_index_weak (A: Type[0]) (n: Nat)
103                        (v: Vector A n) (m: Nat) (a: A) on m ≝
104  match m with
105    [ Z ⇒
106      match v with
107        [ Empty ⇒ Nothing (Vector A n)
108        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
109        ]
110    | S o ⇒
111      match v with
112        [ Empty ⇒ Nothing (Vector A n)
113        | Cons p hd tl ⇒
114            let settail ≝ set_index_weak A p tl o a in
115              match settail with
116                [ Nothing ⇒ Nothing (Vector A n)
117                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
118                ]
119        ]
120    ].
121    //.
122nqed.
123
124nlet rec drop (A: Type[0]) (n: Nat)
125              (v: Vector A n) (m: Nat) on m ≝
126  match m with
127    [ Z ⇒ Just (Vector A n) v
128    | S o ⇒
129      match v with
130        [ Empty ⇒ Nothing (Vector A n)
131        | Cons p hd tl ⇒ ? (drop A p tl o)
132        ]
133    ].
134    //.
135nqed.
136   
137(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
138(* Folds and builds.                                                          *)
139(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
140   
141nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
142                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
143  match v with
144    [ Empty ⇒ x
145    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
146    ].
147   
148nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
149                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
150  match v with
151    [ Empty ⇒ x
152    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
153    ].
154   
155(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
156(* Maps and zips.                                                             *)
157(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
158
159nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
160             (f: A → B) (v: Vector A n) on v ≝
161  match v with
162    [ Empty ⇒ Empty B
163    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
164    ].
165
166(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
167   currently in there.
168*)
169nlemma eq_rect_Type0_r :
170  ∀A: Type[0].
171  ∀a:A.
172  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
173  #A a P H x p.
174  ngeneralize in match H.
175  ngeneralize in match P.
176  ncases p.
177  //.
178nqed.
179
180nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
181             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
182  (match v return (λx.λr. x = n → Vector C x) with
183    [ Empty ⇒ λ_. Empty C
184    | Cons n hd tl ⇒
185      match q return (λy.λr. S n = y → Vector C (S n)) with
186        [ Empty ⇒ ?
187        | Cons m hd' tl' ⇒
188            λe: S n = S m.
189              (f hd hd') :: (zip_with A B C n f tl ?)
190        ]
191    ])
192    (refl ? n).
193      ##
194        [ #e;
195          ndestruct(e);
196          ##
197        | ndestruct(e);
198          napply tl'
199          ##
200        ]
201nqed.
202
203ndefinition zip ≝
204  λA, B: Type[0].
205  λn: Nat.
206  λv: Vector A n.
207  λq: Vector B n.
208    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
209
210(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
211(* Building vectors from scratch                                              *)
212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
213
214nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
215  match n return λn. Vector A n with
216    [ Z ⇒ Empty A
217    | S m ⇒ h :: (replicate A m h)
218    ].
219
220nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
221                (v: Vector A n) (q: Vector A m) on v ≝
222  match v return (λn.λv. Vector A (n + m)) with
223    [ Empty ⇒ q
224    | Cons o hd tl ⇒ hd :: (append A o m tl q)
225    ].
226   
227interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
228   
229nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
230                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
231  a ::
232    (match v with
233       [ Empty ⇒ Empty A
234       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
235       ]).
236
237nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
238                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
239  match v with
240    [ Empty ⇒ ?
241    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
242    ].
243    //.
244nqed.
245   
246(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
247(* Other manipulations.                                                       *)
248(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
249   
250nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
251  match v with
252    [ Empty ⇒ Z
253    | Cons n hd tl ⇒ S $ length A n tl
254    ].
255
256nlet rec reverse (A: Type[0]) (n: Nat)
257                 (v: Vector A n) on v ≝
258  match v return (λm.λv. Vector A m) with
259    [ Empty ⇒ Empty A
260    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
261    ].
262    nrewrite < (succ_plus ? ?).
263    nrewrite > (plus_zero ?).
264    //.
265nqed.
266
267(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
268(* Conversions to and from lists.                                             *)
269(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
270
271nlet rec list_of_vector (A: Type[0]) (n: Nat)
272                        (v: Vector A n) on v ≝
273  match v return λn.λv. List A with
274    [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
275    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
276    ].
277    //.
278nqed.
279
280nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
281  match l return λl. Vector A (length A l) with
282    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
283    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
284    ].
285    nnormalize.
286    //.
287    //.
288nqed.
289
290(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
291(* Rotates and shifts.                                                        *)
292(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
293   
294nlet rec rotate_left (A: Type[0]) (n: Nat)
295                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
296  match m with
297    [ Z ⇒ v
298    | S o ⇒
299        match v with
300          [ Empty ⇒ Empty A
301          | Cons p hd tl ⇒
302             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
303          ]
304    ].
305    nrewrite < (succ_plus ? ?).
306    nrewrite > (plus_zero ?).
307    //.
308nqed.
309
310ndefinition rotate_right ≝
311  λA: Type[0].
312  λn, m: Nat.
313  λv: Vector A n.
314    reverse A n (rotate_left A n m (reverse A n v)).
315   
316ndefinition shift_left_1 ≝
317  λA: Type[0].
318  λn: Nat.
319  λv: Vector A n.
320  λa: A.
321    match v with
322      [ Empty ⇒ ?
323      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
324      ].
325      //.
326nqed.
327
328ndefinition shift_right_1 ≝
329  λA: Type[0].
330  λn: Nat.
331  λv: Vector A n.
332  λa: A.
333    reverse A n (shift_left_1 A n (reverse A n v) a).
334   
335ndefinition shift_left ≝
336  λA: Type[0].
337  λn, m: Nat.
338  λv: Vector A n.
339  λa: A.
340    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
341   
342ndefinition shift_right ≝
343  λA: Type[0].
344  λn, m: Nat.
345  λv: Vector A n.
346  λa: A.
347    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
348   
349(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
350(* Lemmas.                                                                    *)
351(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
352   
353nlemma map_fusion:
354  ∀A, B, C: Type[0].
355  ∀n: Nat.
356  ∀v: Vector A n.
357  ∀f: A → B.
358  ∀g: B → C.
359    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
360  #A B C n v f g.
361  nelim v.
362  nnormalize.
363  @.
364  #N H V H2.
365  nnormalize.
366  nrewrite > H2.
367  @.
368nqed.
369
370nlemma length_correct:
371  ∀A: Type[0].
372  ∀n: Nat.
373  ∀v: Vector A n.
374    length A n v = n.
375  #A n v.
376  nelim v.
377  nnormalize.
378  @.
379  #N H V H2.
380  nnormalize.
381  nrewrite > H2.
382  @.
383nqed.
384
385nlemma map_length:
386  ∀A, B: Type[0].
387  ∀n: Nat.
388  ∀v: Vector A n.
389  ∀f: A → B.
390    length A n v = length B n (map A B n f v).
391  #A B n v f.
392  nelim v.
393  nnormalize.
394  @.
395  #N H V H2.
396  nnormalize.
397  nrewrite > H2.
398  @.
399nqed.
Note: See TracBrowser for help on using the repository browser.