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

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

Updated Util.ma too.

File size: 10.1 KB
RevLine 
[222]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[234]2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
[222]4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
[229]6include "Util.ma".
[224]7
[241]8include "logic/pts.ma".
[240]9
[241]10include "Nat.ma".
[240]11
[241]12include "List.ma".
[240]13
[241]14include "Cartesian.ma".
[240]15
[228]16include "Plogic/equality.ma".
[222]17
[231]18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19(* The datatype.                                                              *)
20(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
21
[228]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).
[222]25
[240]26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27(* Syntax.                                                                    *)
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29
[228]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
[240]36notation "hvbox (v break !! n)"
37  non associative with precedence 90
38  for @{ 'get_index $v $n }.
39
[231]40(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
41(* Lookup.                                                                    *)
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[240]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    ].
[222]58   
[240]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   
[231]96(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
97(* Folds and builds.                                                          *)
98(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
99   
[228]100nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
[222]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   
[228]107nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
[222]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   
[231]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 ≝
[222]120  match v with
[231]121    [ Empty ⇒ Empty B
122    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
[222]123    ].
124
[231]125(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
126   currently in there.
127*)
[228]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.
[230]132  #A a P H x p.
133  ngeneralize in match H.
134  ngeneralize in match P.
135  ncases p.
136  //.
[228]137nqed.
138
[240]139nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
[228]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 ⇒ ?
[229]146        | Cons m hd' tl' ⇒
[228]147            λe: S n = S m.
[240]148              (f hd hd') :: (zip_with A B C n f tl ?)
[228]149        ]
150    ])
151    (refl ? n).
152      ##
153        [ #e;
[229]154          ndestruct(e);
[228]155          ##
[229]156        | ndestruct(e);
157          napply tl'
[228]158          ##
159        ]
[230]160nqed.
161
[240]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
[231]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
[230]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    ].
[231]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       ]).
[230]199
[231]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
[230]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
[231]228(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
229(* Conversions to and from lists.                                             *)
230(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
231
[236]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
[240]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)
[230]237    ].
[240]238    //.
239nqed.
[231]240
[236]241nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
[231]242  match l return λl. Vector A (length A l) with
[240]243    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)
[237]244    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
[231]245    ].
[237]246    nnormalize.
[231]247    //.
[237]248    //.
[231]249nqed.
250
251(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
252(* Rotates and shifts.                                                        *)
253(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[230]254   
[231]255nlet rec rotate_left (A: Type[0]) (n: Nat)
256                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
[230]257  match m with
258    [ Z ⇒ v
259    | S o ⇒
260        match v with
261          [ Empty ⇒ Empty A
262          | Cons p hd tl ⇒
[231]263             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
[230]264          ]
265    ].
266    //.
267nqed.
[231]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)).
[230]274   
[240]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   
[243]294ncheck Nat.
295   
[240]296ndefinition shift_left ≝
297  λA: Type[0].
298  λn, m: Nat.
299  λv: Vector A n.
300  λa: A.
301    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
302   
303ndefinition shift_right ≝
304  λA: Type[0].
305  λn, m: Nat.
306  λv: Vector A n.
307  λa: A.
308    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
309   
[231]310(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
311(* Lemmas.                                                                    *)
312(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
313   
[230]314nlemma map_fusion:
315  ∀A, B, C: Type[0].
316  ∀n: Nat.
317  ∀v: Vector A n.
318  ∀f: A → B.
319  ∀g: B → C.
320    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
321  #A B C n v f g.
322  nelim v.
323  nnormalize.
324  @.
325  #N H V H2.
326  nnormalize.
327  nrewrite > H2.
328  @.
329nqed.
330
331nlemma length_correct:
332  ∀A: Type[0].
333  ∀n: Nat.
334  ∀v: Vector A n.
335    length A n v = n.
336  #A n v.
337  nelim v.
338  nnormalize.
339  @.
340  #N H V H2.
341  nnormalize.
342  nrewrite > H2.
343  @.
344nqed.
345
346nlemma map_length:
347  ∀A, B: Type[0].
348  ∀n: Nat.
349  ∀v: Vector A n.
350  ∀f: A → B.
351    length A n v = length B n (map A B n f v).
352  #A B n v f.
353  nelim v.
354  nnormalize.
355  @.
356  #N H V H2.
357  nnormalize.
358  nrewrite > H2.
359  @.
[240]360nqed.
Note: See TracBrowser for help on using the repository browser.