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

Last change on this file since 234 was 234, checked in by mulligan, 9 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.