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

Last change on this file since 330 was 329, checked in by mulligan, 10 years ago

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