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

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

More work on fetch.

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