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

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

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

File size: 7.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "Cartesian.ma".
7include "Nat.ma".
8include "Util.ma".
9include "List.ma".
10
11include "logic/pts.ma".
12include "Plogic/equality.ma".
13
14(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
15(* The datatype.                                                              *)
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17
18ninductive Vector (A: Type[0]): Nat → Type[0] ≝
19  Empty: Vector A Z
20| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
21
22notation "hvbox(hd break :: tl)"
23  right associative with precedence 52
24  for @{ 'Cons $hd $tl }.
25 
26interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
27
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29(* Lookup.                                                                    *)
30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
31   
32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
33(* Folds and builds.                                                          *)
34(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
35   
36nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
37                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
38  match v with
39    [ Empty ⇒ x
40    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
41    ].
42   
43nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
44                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
45  match v with
46    [ Empty ⇒ x
47    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
48    ].
49   
50(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
51(* Maps and zips.                                                             *)
52(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
53
54nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
55             (f: A → B) (v: Vector A n) on v ≝
56  match v with
57    [ Empty ⇒ Empty B
58    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
59    ].
60
61(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
62   currently in there.
63*)
64nlemma eq_rect_Type0_r :
65  ∀A: Type[0].
66  ∀a:A.
67  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
68  #A a P H x p.
69  ngeneralize in match H.
70  ngeneralize in match P.
71  ncases p.
72  //.
73nqed.
74
75nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
76             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
77  (match v return (λx.λr. x = n → Vector C x) with
78    [ Empty ⇒ λ_. Empty C
79    | Cons n hd tl ⇒
80      match q return (λy.λr. S n = y → Vector C (S n)) with
81        [ Empty ⇒ ?
82        | Cons m hd' tl' ⇒
83            λe: S n = S m.
84              (f hd hd') :: (zip A B C n f tl ?)
85        ]
86    ])
87    (refl ? n).
88      ##
89        [ #e;
90          ndestruct(e);
91          ##
92        | ndestruct(e);
93          napply tl'
94          ##
95        ]
96nqed.
97
98(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
99(* Building vectors from scratch                                              *)
100(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
101
102nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
103  match n return λn. Vector A n with
104    [ Z ⇒ Empty A
105    | S m ⇒ h :: (replicate A m h)
106    ].
107
108nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
109                (v: Vector A n) (q: Vector A m) on v ≝
110  match v return (λn.λv. Vector A (n + m)) with
111    [ Empty ⇒ q
112    | Cons o hd tl ⇒ hd :: (append A o m tl q)
113    ].
114   
115notation "v break @ q"
116  right associative with precedence 47
117  for @{ 'append $v $q }.
118 
119interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
120   
121nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
122                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
123  a ::
124    (match v with
125       [ Empty ⇒ Empty A
126       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
127       ]).
128
129nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
130                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
131  match v with
132    [ Empty ⇒ ?
133    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
134    ].
135    //.
136nqed.
137   
138(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
139(* Other manipulations.                                                       *)
140(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
141   
142nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
143  match v with
144    [ Empty ⇒ Z
145    | Cons n hd tl ⇒ S $ length A n tl
146    ].
147
148nlet rec reverse (A: Type[0]) (n: Nat)
149                 (v: Vector A n) on v ≝
150  match v return (λm.λv. Vector A m) with
151    [ Empty ⇒ Empty A
152    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
153    ].
154    //.
155nqed.
156
157(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
158(* Conversions to and from lists.                                             *)
159(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
160
161nlet rec to_list (A: Type[0]) (n: Nat)
162                 (v: Vector A n) on v ≝
163  match v with
164    [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A
165    | Cons o hd tl ⇒ hd :: (to_list A o tl)
166    ].
167
168(*
169nlet rec from_list (A: Type[0]) (l: List A) on l ≝
170  match l return λl. Vector A (length A l) with
171    [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
172    | Cons hd tl ⇒ ? (hd :: (from_list A tl))
173    ].
174    //.
175nqed.
176*)
177
178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
179(* Rotates and shifts.                                                        *)
180(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
181   
182nlet rec rotate_left (A: Type[0]) (n: Nat)
183                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
184  match m with
185    [ Z ⇒ v
186    | S o ⇒
187        match v with
188          [ Empty ⇒ Empty A
189          | Cons p hd tl ⇒
190             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
191          ]
192    ].
193    //.
194nqed.
195
196ndefinition rotate_right ≝
197  λA: Type[0].
198  λn, m: Nat.
199  λv: Vector A n.
200    reverse A n (rotate_left A n m (reverse A n v)).
201   
202(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
203(* Lemmas.                                                                    *)
204(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
205   
206nlemma map_fusion:
207  ∀A, B, C: Type[0].
208  ∀n: Nat.
209  ∀v: Vector A n.
210  ∀f: A → B.
211  ∀g: B → C.
212    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
213  #A B C n v f g.
214  nelim v.
215  nnormalize.
216  @.
217  #N H V H2.
218  nnormalize.
219  nrewrite > H2.
220  @.
221nqed.
222
223nlemma length_correct:
224  ∀A: Type[0].
225  ∀n: Nat.
226  ∀v: Vector A n.
227    length A n v = n.
228  #A n v.
229  nelim v.
230  nnormalize.
231  @.
232  #N H V H2.
233  nnormalize.
234  nrewrite > H2.
235  @.
236nqed.
237
238nlemma map_length:
239  ∀A, B: Type[0].
240  ∀n: Nat.
241  ∀v: Vector A n.
242  ∀f: A → B.
243    length A n v = length B n (map A B n f v).
244  #A B n v f.
245  nelim v.
246  nnormalize.
247  @.
248  #N H V H2.
249  nnormalize.
250  nrewrite > H2.
251  @.
252nqed.
Note: See TracBrowser for help on using the repository browser.