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

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