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

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

Work on ASM.ma file.

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