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

Last change on this file since 362 was 362, checked in by sacerdot, 9 years ago

Less ambiguous definitions.

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