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

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