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

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

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File size: 13.8 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 | nlapply (S_inj … K); //]
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 | nlapply (S_inj … K); //]
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##[##1,2: ndestruct | ##3,4: nlapply (S_inj … prf); // ]
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        | nlapply (S_inj … e); #H; nrewrite > H;
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,2: ndestruct
400      | nlapply (S_inj … prf); #X; nrewrite < X;
401        napply tl' ]
402nqed.
403   
404(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
405(* Lemmas.                                                                    *)
406(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
407   
408nlemma map_fusion:
409  ∀A, B, C: Type[0].
410  ∀n: Nat.
411  ∀v: Vector A n.
412  ∀f: A → B.
413  ∀g: B → C.
414    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
415  #A B C n v f g.
416  nelim v.
417  nnormalize.
418  @.
419  #N H V H2.
420  nnormalize.
421  nrewrite > H2.
422  @.
423nqed.
424
425nlemma length_correct:
426  ∀A: Type[0].
427  ∀n: Nat.
428  ∀v: Vector A n.
429    length A n v = n.
430  #A n v.
431  nelim v.
432  nnormalize.
433  @.
434  #N H V H2.
435  nnormalize.
436  nrewrite > H2.
437  @.
438nqed.
439
440nlemma map_length:
441  ∀A, B: Type[0].
442  ∀n: Nat.
443  ∀v: Vector A n.
444  ∀f: A → B.
445    length A n v = length B n (map A B n f v).
446  #A B n v f.
447  nelim v.
448  nnormalize.
449  @.
450  #N H V H2.
451  nnormalize.
452  nrewrite > H2.
453  @.
454nqed.
Note: See TracBrowser for help on using the repository browser.