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

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

Moved over to standard library.

File size: 14.1 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "datatypes/list.ma".
7include "basics/bool.ma".
8include "datatypes/sums.ma".
9
10include "Util.ma".
11
12include "arithmetics/nat.ma".
13
14
15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* The datatype.                                                              *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
19ninductive Vector (A: Type[0]): nat → Type[0] ≝
20  VEmpty: Vector A O
21| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
22
23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
24(* Syntax.                                                                    *)
25(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
26
27notation "hvbox(hd break ::: tl)"
28  right associative with precedence 52
29  for @{ 'vcons $hd $tl }.
30
31notation "[[ list0 x sep ; ]]"
32  non associative with precedence 90
33  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
34
35interpretation "Vector vnil" 'vnil = (VEmpty ?).
36interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
37
38notation "hvbox(l break !!! break n)"
39  non associative with precedence 90
40  for @{ 'get_index_v $l $n }.
41
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45
46nlet rec get_index_v (A: Type[0]) (n: nat)
47                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
48  (match m with
49    [ O ⇒
50      match v return λx.λ_. O < x → A with
51        [ VEmpty ⇒ λabsd1: O < O. ?
52        | VCons p hd tl ⇒ λprf1: O < S p. hd
53        ]
54    | S o ⇒
55      (match v return λx.λ_. S o < x → A with
56        [ VEmpty ⇒ λprf: S o < O. ?
57        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
58        ])
59    ]) lt.
60    ##[ ncases (not_le_Sn_O O); nnormalize in absd1; #H; ncases (H absd1);
61    ##| ncases (not_le_Sn_O (S o)); nnormalize in prf; #H; ncases (H prf);
62    ##| nnormalize; nnormalize in prf; napply le_S_S_to_le; nassumption;
63    ##]
64nqed.
65
66ndefinition get_index' ≝
67  λA: Type[0].
68  λn, m: nat.
69  λb: Vector A (S (n + m)).
70    get_index_v A (S (n + m)) b n ?.
71  nnormalize;
72  //;
73nqed.
74
75nlet rec get_index_weak_v (A: Type[0]) (n: nat)
76                          (v: Vector A n) (m: nat) on m ≝
77  match m with
78    [ O ⇒
79      match v with
80        [ VEmpty ⇒ None A
81        | VCons p hd tl ⇒ Some A hd
82        ]
83    | S o ⇒
84      match v with
85        [ VEmpty ⇒ None A
86        | VCons p hd tl ⇒ get_index_weak_v A p tl o
87        ]
88    ].
89   
90interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
91
92nlet rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
93  (match m with
94    [ O ⇒
95      match v return λx.λ_. O < x → Vector A x with
96        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
97        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
98        ]
99    | S o ⇒
100      (match v return λx.λ_. S o < x → Vector A x with
101        [ VEmpty ⇒ λprf: S o < O. [[ ]]
102        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
103        ])
104    ]) lt.
105    nnormalize in prf ⊢ %;
106    /2/;
107nqed.
108   
109nlet rec set_index_weak (A: Type[0]) (n: nat)
110                        (v: Vector A n) (m: nat) (a: A) on m ≝
111  match m with
112    [ O ⇒
113      match v with
114        [ VEmpty ⇒ None (Vector A n)
115        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
116        ]
117    | S o ⇒
118      match v with
119        [ VEmpty ⇒ None (Vector A n)
120        | VCons p hd tl ⇒
121            let settail ≝ set_index_weak A p tl o a in
122              match settail with
123                [ None ⇒ None (Vector A n)
124                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
125                ]
126        ]
127    ].
128    //.
129nqed.
130
131nlet rec drop (A: Type[0]) (n: nat)
132              (v: Vector A n) (m: nat) on m ≝
133  match m with
134    [ O ⇒ Some (Vector A n) v
135    | S o ⇒
136      match v with
137        [ VEmpty ⇒ None (Vector A n)
138        | VCons p hd tl ⇒ ? (drop A p tl o)
139        ]
140    ].
141    //.
142nqed.
143
144nlet rec split (A: Type[0]) (m,n: nat) on m
145             : Vector A (plus m n) → (Vector A m) × (Vector A n)
146
147 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
148  [ O ⇒ λv.〈[[ ]], v〉
149  | S m' ⇒ λv.
150     match v return λl.λ_:Vector A l.l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
151      [ VEmpty ⇒ λK.⊥
152      | VCons o he tl ⇒ λK.
153         match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with
154          [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
155// [ ndestruct | nlapply (injective_S … K); //]
156nqed.
157
158ndefinition head: ∀A:Type[0]. ∀n. Vector A (S n) → A × (Vector A n)
159≝ λA,n,v.
160 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with
161  [ VEmpty ⇒ λK.⊥
162  | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉
163  ] (? : S ? = S ?).
164// [ ndestruct | nlapply (injective_S … K); //]
165nqed.
166
167ndefinition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
168 λA,v. fst … (head … v).
169   
170(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
171(* Folds and builds.                                                          *)
172(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
173   
174nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
175                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
176  match v with
177    [ VEmpty ⇒ x
178    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
179    ].
180
181nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
182                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
183                      (v: Vector A n) (q: Vector B n) on v : C n ≝
184  (match v return λx.λ_. x = n → C n with
185    [ VEmpty ⇒
186      match q return λx.λ_. O = x → C x with
187        [ VEmpty ⇒ λprf: O = O. c
188        | VCons o hd tl ⇒ λabsd. ⊥
189        ]
190    | VCons o hd tl ⇒
191      match q return λx.λ_. S o = x → C x with
192        [ VEmpty ⇒ λabsd: S o = O. ⊥
193        | VCons p hd' tl' ⇒ λprf: S o = S p.
194           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
195        ]
196    ]) (refl ? n).
197##[##1,2: ndestruct | ##3,4: nlapply (injective_S … prf); // ]
198nqed.
199 
200nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
201                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
202  match v with
203    [ VEmpty ⇒ x
204    | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
205    ].
206   
207(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
208(* Maps and zips.                                                             *)
209(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
210
211nlet rec map (A: Type[0]) (B: Type[0]) (n: nat)
212             (f: A → B) (v: Vector A n) on v ≝
213  match v with
214    [ VEmpty ⇒ [[ ]]
215    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
216    ].
217
218nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
219             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
220  (match v return (λx.λr. x = n → Vector C x) with
221    [ VEmpty ⇒ λ_. [[ ]]
222    | VCons n hd tl ⇒
223      match q return (λy.λr. S n = y → Vector C (S n)) with
224        [ VEmpty ⇒ ?
225        | VCons m hd' tl' ⇒
226            λe: S n = S m.
227              (f hd hd') ::: (zip_with A B C n f tl ?)
228        ]
229    ])
230    (refl ? n).
231      ##
232        [ #e;
233          ndestruct(e);
234          ##
235        | nlapply (injective_S … e); #H; nrewrite > H;
236          napply tl'
237          ##
238        ]
239nqed.
240
241ndefinition zip ≝
242  λA, B: Type[0].
243  λn: nat.
244  λv: Vector A n.
245  λq: Vector B n.
246    zip_with A B (A × B) n (mk_pair A B) v q.
247
248(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
249(* Building vectors from scratch                                              *)
250(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
251
252nlet rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
253  match n return λn. Vector A n with
254    [ O ⇒ [[ ]]
255    | S m ⇒ h ::: (replicate A m h)
256    ].
257
258(* DPM: fixme.  Weird matita bug in base case. *)
259nlet rec append (A: Type[0]) (n: nat) (m: nat)
260                (v: Vector A n) (q: Vector A m) on v ≝
261  match v return (λn.λv. Vector A (n + m)) with
262    [ VEmpty ⇒ (? q)
263    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
264    ].
265    #H; nassumption;
266nqed.
267   
268notation "hvbox(l break @@ r)"
269  right associative with precedence 47
270  for @{ 'vappend $l $r }.
271   
272interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
273   
274nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
275                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
276  a :::
277    (match v with
278       [ VEmpty ⇒ VEmpty A
279       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
280       ]).
281
282nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
283                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
284  match v with
285    [ VEmpty ⇒ ?
286    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
287    ].
288    //.
289nqed.
290   
291(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
292(* Other manipulations.                                                       *)
293(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
294
295nlet rec reverse (A: Type[0]) (n: nat)
296                 (v: Vector A n) on v ≝
297  match v return (λm.λv. Vector A m) with
298    [ VEmpty ⇒ [[ ]]
299    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
300    ].
301    //;
302nqed.
303
304(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
305(* Conversions to and from lists.                                             *)
306(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
307
308nlet rec list_of_vector (A: Type[0]) (n: nat)
309                        (v: Vector A n) on v ≝
310  match v return λn.λv. list A with
311    [ VEmpty ⇒ []
312    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
313    ].
314
315nlet rec vector_of_list (A: Type[0]) (l: list A) on l ≝
316  match l return λl. Vector A (length A l) with
317    [ nil ⇒ [[ ]]
318    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
319    ].
320
321(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
322(* Rotates and shifts.                                                        *)
323(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
324   
325nlet rec rotate_left (A: Type[0]) (n: nat)
326                     (m: nat) (v: Vector A n) on m: Vector A n ≝
327  match m with
328    [ O ⇒ v
329    | S o ⇒
330        match v with
331          [ VEmpty ⇒ [[ ]]
332          | VCons p hd tl ⇒
333             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
334          ]
335    ].
336 //.
337nqed.
338
339ndefinition rotate_right ≝
340  λA: Type[0].
341  λn, m: nat.
342  λv: Vector A n.
343    reverse A n (rotate_left A n m (reverse A n v)).
344
345ndefinition shift_left_1 ≝
346  λA: Type[0].
347  λn: nat.
348  λv: Vector A (S n).
349  λa: A.
350   match v return λy.λ_. y = S n → Vector A y with
351     [ VEmpty ⇒ λH.⊥
352     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
353     ] (refl ? (S n)).
354 ndestruct.
355nqed.
356
357ndefinition shift_right_1 ≝
358  λA: Type[0].
359  λn: nat.
360  λv: Vector A (S n).
361  λa: A.
362    reverse … (shift_left_1 … (reverse … v) a).
363   
364ndefinition shift_left ≝
365  λA: Type[0].
366  λn, m: nat.
367  λv: Vector A (S n).
368  λa: A.
369    iterate … (λx. shift_left_1 … x a) v m.
370   
371ndefinition shift_right ≝
372  λA: Type[0].
373  λn, m: nat.
374  λv: Vector A (S n).
375  λa: A.
376    iterate … (λx. shift_right_1 … x a) v m.
377
378(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
379(* Decidable equality.                                                        *)
380(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
381
382nlet rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
383  (match b return λx.λ_. n = x → bool with
384    [ VEmpty ⇒
385      match c return λx.λ_. x = O → bool with
386        [ VEmpty ⇒ λ_. true
387        | VCons p hd tl ⇒ λabsd.⊥
388        ]
389    | VCons o hd tl ⇒
390        match c return λx.λ_. x = S o → bool with
391          [ VEmpty ⇒ λabsd.⊥
392          | VCons p hd' tl' ⇒
393            λprf.
394              if (f hd hd') then
395                (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
396              else
397                false
398          ]
399    ]) (refl ? n).
400    ##[##1,2: ndestruct
401      | nlapply (injective_S … prf); #X; nrewrite < X; @]
402nqed.
403
404(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
405(* Subvectors.                                                                *)
406(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
407
408ndefinition mem ≝
409 λA: Type[0].
410 λeq_a : A → A → bool.
411 λn: nat.
412 λl: Vector A n.
413 λx: A.
414  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
415
416ndefinition subvector_with ≝
417  λA: Type[0].
418  λn: nat.
419  λm: nat.
420  λf: A → A → bool.
421  λv: Vector A n.
422  λq: Vector A m.
423    fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
424   
425(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
426(* Lemmas.                                                                    *)
427(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
428   
429nlemma map_fusion:
430  ∀A, B, C: Type[0].
431  ∀n: nat.
432  ∀v: Vector A n.
433  ∀f: A → B.
434  ∀g: B → C.
435    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
436  #A B C n v f g.
437  nelim v.
438  nnormalize.
439  @.
440  #N H V H2.
441  nnormalize.
442  nrewrite > H2.
443  @.
444nqed.
Note: See TracBrowser for help on using the repository browser.