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

Last change on this file since 373 was 373, checked in by sacerdot, 10 years ago

Order of declaration of notations changed to put more precise notations first.

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