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

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

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

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