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

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

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