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

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