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

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

less axioms

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