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

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

Need stronger set_ and get_index functions on vectors (current ones return a Maybe type).

File size: 10.4 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "Util.ma".
7
8include "Universes.ma".
9
10include "Nat.ma".
11include "List.ma".
12include "Cartesian.ma".
13include "Maybe.ma".
14include "Equality.ma".
15
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17(* The datatype.                                                              *)
18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19
20ninductive Vector (A: Type[0]): Nat → Type[0] ≝
21  Empty: Vector A Z
22| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
23
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25(* Syntax.                                                                    *)
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27
28interpretation "Vector nil" 'nil = (Empty ?).
29interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
30
31notation "hvbox (v break !! n)"
32  non associative with precedence 90
33  for @{ 'get_index $v $n }.
34
35(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
36(* Lookup.                                                                    *)
37(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
38
39nlet rec get_index (A: Type[0]) (n: Nat)
40                   (v: Vector A n) (m: Nat) on m ≝
41  match m with
42    [ Z ⇒
43      match v with
44        [ Empty ⇒ Nothing A
45        | Cons p hd tl ⇒ Just A hd
46        ]
47    | S o ⇒
48      match v with
49        [ Empty ⇒ Nothing A
50        | Cons p hd tl ⇒ get_index A p tl o
51        ]
52    ].
53   
54interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
55   
56nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m ≝
57  match m return (λx. x < n → A) with
58    [ Z ⇒
59      match v with
60        [ Empty ⇒ λ_.?
61        | Cons p hd tl ⇒ λ_.hd
62        ]
63    | S o ⇒
64      match v with
65        [ Empty ⇒ λ_.?
66        | Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a
67        ]
68    ].
69   
70nlet rec set_index_weak (A: Type[0]) (n: Nat)
71                        (v: Vector A n) (m: Nat) (a: A) on m ≝
72  match m with
73    [ Z ⇒
74      match v with
75        [ Empty ⇒ Nothing (Vector A n)
76        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
77        ]
78    | S o ⇒
79      match v with
80        [ Empty ⇒ Nothing (Vector A n)
81        | Cons p hd tl ⇒
82            let settail ≝ set_index_weak A p tl o a in
83              match settail with
84                [ Nothing ⇒ Nothing (Vector A n)
85                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
86                ]
87        ]
88    ].
89    //.
90nqed.
91
92nlet rec drop (A: Type[0]) (n: Nat)
93              (v: Vector A n) (m: Nat) on m ≝
94  match m with
95    [ Z ⇒ Just (Vector A n) v
96    | S o ⇒
97      match v with
98        [ Empty ⇒ Nothing (Vector A n)
99        | Cons p hd tl ⇒ ? (drop A p tl o)
100        ]
101    ].
102    //.
103nqed.
104   
105(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
106(* Folds and builds.                                                          *)
107(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
108   
109nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
110                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
111  match v with
112    [ Empty ⇒ x
113    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
114    ].
115   
116nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
117                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
118  match v with
119    [ Empty ⇒ x
120    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
121    ].
122   
123(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
124(* Maps and zips.                                                             *)
125(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
126
127nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
128             (f: A → B) (v: Vector A n) on v ≝
129  match v with
130    [ Empty ⇒ Empty B
131    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
132    ].
133
134(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
135   currently in there.
136*)
137nlemma eq_rect_Type0_r :
138  ∀A: Type[0].
139  ∀a:A.
140  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
141  #A a P H x p.
142  ngeneralize in match H.
143  ngeneralize in match P.
144  ncases p.
145  //.
146nqed.
147
148nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
149             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
150  (match v return (λx.λr. x = n → Vector C x) with
151    [ Empty ⇒ λ_. Empty C
152    | Cons n hd tl ⇒
153      match q return (λy.λr. S n = y → Vector C (S n)) with
154        [ Empty ⇒ ?
155        | Cons m hd' tl' ⇒
156            λe: S n = S m.
157              (f hd hd') :: (zip_with A B C n f tl ?)
158        ]
159    ])
160    (refl ? n).
161      ##
162        [ #e;
163          ndestruct(e);
164          ##
165        | ndestruct(e);
166          napply tl'
167          ##
168        ]
169nqed.
170
171ndefinition zip ≝
172  λA, B: Type[0].
173  λn: Nat.
174  λv: Vector A n.
175  λq: Vector B n.
176    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
177
178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
179(* Building vectors from scratch                                              *)
180(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
181
182nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
183  match n return λn. Vector A n with
184    [ Z ⇒ Empty A
185    | S m ⇒ h :: (replicate A m h)
186    ].
187
188nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
189                (v: Vector A n) (q: Vector A m) on v ≝
190  match v return (λn.λv. Vector A (n + m)) with
191    [ Empty ⇒ q
192    | Cons o hd tl ⇒ hd :: (append A o m tl q)
193    ].
194   
195notation "v break @ q"
196  right associative with precedence 47
197  for @{ 'append $v $q }.
198 
199interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
200   
201nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
202                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
203  a ::
204    (match v with
205       [ Empty ⇒ Empty A
206       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
207       ]).
208
209nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
210                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
211  match v with
212    [ Empty ⇒ ?
213    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
214    ].
215    //.
216nqed.
217   
218(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
219(* Other manipulations.                                                       *)
220(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
221   
222nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
223  match v with
224    [ Empty ⇒ Z
225    | Cons n hd tl ⇒ S $ length A n tl
226    ].
227
228nlet rec reverse (A: Type[0]) (n: Nat)
229                 (v: Vector A n) on v ≝
230  match v return (λm.λv. Vector A m) with
231    [ Empty ⇒ Empty A
232    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
233    ].
234    nrewrite < (succ_plus ? ?).
235    nrewrite > (plus_zero ?).
236    //.
237nqed.
238
239(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
240(* Conversions to and from lists.                                             *)
241(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
242
243nlet rec list_of_vector (A: Type[0]) (n: Nat)
244                        (v: Vector A n) on v ≝
245  match v return λn.λv. List A with
246    [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
247    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
248    ].
249    //.
250nqed.
251
252nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
253  match l return λl. Vector A (length A l) with
254    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
255    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
256    ].
257    nnormalize.
258    //.
259    //.
260nqed.
261
262(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
263(* Rotates and shifts.                                                        *)
264(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
265   
266nlet rec rotate_left (A: Type[0]) (n: Nat)
267                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
268  match m with
269    [ Z ⇒ v
270    | S o ⇒
271        match v with
272          [ Empty ⇒ Empty A
273          | Cons p hd tl ⇒
274             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
275          ]
276    ].
277    nrewrite < (succ_plus ? ?).
278    nrewrite > (plus_zero ?).
279    //.
280nqed.
281
282ndefinition rotate_right ≝
283  λA: Type[0].
284  λn, m: Nat.
285  λv: Vector A n.
286    reverse A n (rotate_left A n m (reverse A n v)).
287   
288ndefinition shift_left_1 ≝
289  λA: Type[0].
290  λn: Nat.
291  λv: Vector A n.
292  λa: A.
293    match v with
294      [ Empty ⇒ ?
295      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
296      ].
297      //.
298nqed.
299
300ndefinition shift_right_1 ≝
301  λA: Type[0].
302  λn: Nat.
303  λv: Vector A n.
304  λa: A.
305    reverse A n (shift_left_1 A n (reverse A n v) a).
306   
307ndefinition shift_left ≝
308  λA: Type[0].
309  λn, m: Nat.
310  λv: Vector A n.
311  λa: A.
312    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
313   
314ndefinition shift_right ≝
315  λA: Type[0].
316  λn, m: Nat.
317  λv: Vector A n.
318  λa: A.
319    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
320   
321(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
322(* Lemmas.                                                                    *)
323(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
324   
325nlemma map_fusion:
326  ∀A, B, C: Type[0].
327  ∀n: Nat.
328  ∀v: Vector A n.
329  ∀f: A → B.
330  ∀g: B → C.
331    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
332  #A B C n v f g.
333  nelim v.
334  nnormalize.
335  @.
336  #N H V H2.
337  nnormalize.
338  nrewrite > H2.
339  @.
340nqed.
341
342nlemma length_correct:
343  ∀A: Type[0].
344  ∀n: Nat.
345  ∀v: Vector A n.
346    length A n v = n.
347  #A n v.
348  nelim v.
349  nnormalize.
350  @.
351  #N H V H2.
352  nnormalize.
353  nrewrite > H2.
354  @.
355nqed.
356
357nlemma map_length:
358  ∀A, B: Type[0].
359  ∀n: Nat.
360  ∀v: Vector A n.
361  ∀f: A → B.
362    length A n v = length B n (map A B n f v).
363  #A B n v f.
364  nelim v.
365  nnormalize.
366  @.
367  #N H V H2.
368  nnormalize.
369  nrewrite > H2.
370  @.
371nqed.
Note: See TracBrowser for help on using the repository browser.