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

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

Strengthened typings of get_ and set_index in Vector file.

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