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

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

REGISTER now takes a BitVector? 3

File size: 13.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 head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))).
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_left (A: Type[0]) (B: Type[0]) (n: Nat)
163                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
164  match v with
165    [ Empty ⇒ x
166    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
167    ].
168   
169(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
170(* Maps and zips.                                                             *)
171(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
172
173nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
174             (f: A → B) (v: Vector A n) on v ≝
175  match v with
176    [ Empty ⇒ Empty B
177    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
178    ].
179
180(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
181   currently in there.
182*)
183nlemma eq_rect_Type0_r :
184  ∀A: Type[0].
185  ∀a:A.
186  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
187  #A a P H x p.
188  ngeneralize in match H.
189  ngeneralize in match P.
190  ncases p.
191  //.
192nqed.
193
194nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
195             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
196  (match v return (λx.λr. x = n → Vector C x) with
197    [ Empty ⇒ λ_. Empty C
198    | Cons n hd tl ⇒
199      match q return (λy.λr. S n = y → Vector C (S n)) with
200        [ Empty ⇒ ?
201        | Cons m hd' tl' ⇒
202            λe: S n = S m.
203              (f hd hd') :: (zip_with A B C n f tl ?)
204        ]
205    ])
206    (refl ? n).
207      ##
208        [ #e;
209          ndestruct(e);
210          ##
211        | ndestruct(e);
212          napply tl'
213          ##
214        ]
215nqed.
216
217ndefinition zip ≝
218  λA, B: Type[0].
219  λn: Nat.
220  λv: Vector A n.
221  λq: Vector B n.
222    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
223
224(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
225(* Building vectors from scratch                                              *)
226(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
227
228nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
229  match n return λn. Vector A n with
230    [ Z ⇒ Empty A
231    | S m ⇒ h :: (replicate A m h)
232    ].
233
234nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
235                (v: Vector A n) (q: Vector A m) on v ≝
236  match v return (λn.λv. Vector A (n + m)) with
237    [ Empty ⇒ q
238    | Cons o hd tl ⇒ hd :: (append A o m tl q)
239    ].
240   
241notation "hvbox(l break @@ r)"
242  right associative with precedence 47
243  for @{ 'vappend $l $r }.
244   
245interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
246   
247nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
248                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
249  a ::
250    (match v with
251       [ Empty ⇒ Empty A
252       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
253       ]).
254
255nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
256                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
257  match v with
258    [ Empty ⇒ ?
259    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
260    ].
261    //.
262nqed.
263   
264(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
265(* Other manipulations.                                                       *)
266(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
267   
268nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
269  match v with
270    [ Empty ⇒ Z
271    | Cons n hd tl ⇒ S $ length A n tl
272    ].
273
274nlet rec reverse (A: Type[0]) (n: Nat)
275                 (v: Vector A n) on v ≝
276  match v return (λm.λv. Vector A m) with
277    [ Empty ⇒ Empty A
278    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
279    ].
280    nrewrite < (succ_plus ? ?).
281    nrewrite > (plus_zero ?).
282    //.
283nqed.
284
285(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
286(* Conversions to and from lists.                                             *)
287(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
288
289nlet rec list_of_vector (A: Type[0]) (n: Nat)
290                        (v: Vector A n) on v ≝
291  match v return λn.λv. List A with
292    [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
293    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
294    ].
295    //.
296nqed.
297
298nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
299  match l return λl. Vector A (length A l) with
300    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
301    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
302    ].
303    nnormalize.
304    //.
305    //.
306nqed.
307
308(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
309(* Rotates and shifts.                                                        *)
310(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
311   
312nlet rec rotate_left (A: Type[0]) (n: Nat)
313                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
314  match m with
315    [ Z ⇒ v
316    | S o ⇒
317        match v with
318          [ Empty ⇒ Empty A
319          | Cons p hd tl ⇒
320             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
321          ]
322    ].
323    nrewrite < (succ_plus ? ?).
324    nrewrite > (plus_zero ?).
325    //.
326nqed.
327
328ndefinition rotate_right ≝
329  λA: Type[0].
330  λn, m: Nat.
331  λv: Vector A n.
332    reverse A n (rotate_left A n m (reverse A n v)).
333   
334ndefinition shift_left_1 ≝
335  λA: Type[0].
336  λn: Nat.
337  λv: Vector A n.
338  λa: A.
339    match v with
340      [ Empty ⇒ ?
341      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
342      ].
343      //.
344nqed.
345
346ndefinition shift_right_1 ≝
347  λA: Type[0].
348  λn: Nat.
349  λv: Vector A n.
350  λa: A.
351    reverse A n (shift_left_1 A n (reverse A n v) a).
352   
353ndefinition shift_left ≝
354  λA: Type[0].
355  λn, m: Nat.
356  λv: Vector A n.
357  λa: A.
358    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
359   
360ndefinition shift_right ≝
361  λA: Type[0].
362  λn, m: Nat.
363  λv: Vector A n.
364  λa: A.
365    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
366
367(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
368(* Decidable equality.                                                        *)
369(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
370
371nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b ≝
372  (match b return λx.λ_. n = x → Bool with
373    [ Empty ⇒
374      match c return λx.λ_. x = Z → Bool with
375        [ Empty ⇒ λ_. true
376        | Cons p hd tl ⇒ λabsd.?
377        ]
378    | Cons o hd tl ⇒
379        match c return λx.λ_. x = S o → Bool with
380          [ Empty ⇒ λabsd. ?
381          | Cons p hd' tl' ⇒
382            λprf.
383              if (f hd hd') then
384                (eq_v A o f tl ?)
385              else
386                false
387          ]
388    ]) (refl ? n).
389    ##[##1, 3:
390        ndestruct (absd);
391        ndestruct (prf);
392        napply tl';
393    ##|##2:
394        ndestruct (absd);
395    ##]
396nqed.
397   
398(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
399(* Lemmas.                                                                    *)
400(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
401   
402nlemma map_fusion:
403  ∀A, B, C: Type[0].
404  ∀n: Nat.
405  ∀v: Vector A n.
406  ∀f: A → B.
407  ∀g: B → C.
408    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
409  #A B C n v f g.
410  nelim v.
411  nnormalize.
412  @.
413  #N H V H2.
414  nnormalize.
415  nrewrite > H2.
416  @.
417nqed.
418
419nlemma length_correct:
420  ∀A: Type[0].
421  ∀n: Nat.
422  ∀v: Vector A n.
423    length A n v = n.
424  #A n v.
425  nelim v.
426  nnormalize.
427  @.
428  #N H V H2.
429  nnormalize.
430  nrewrite > H2.
431  @.
432nqed.
433
434nlemma map_length:
435  ∀A, B: Type[0].
436  ∀n: Nat.
437  ∀v: Vector A n.
438  ∀f: A → B.
439    length A n v = length B n (map A B n f v).
440  #A B n v f.
441  nelim v.
442  nnormalize.
443  @.
444  #N H V H2.
445  nnormalize.
446  nrewrite > H2.
447  @.
448nqed.
449
450naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.
Note: See TracBrowser for help on using the repository browser.