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

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

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File size: 7.5 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
167nlet rec from_list (A: Type[0]) (l: List A) on l ≝
168  match l return λl. Vector A (length A l) with
169    [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
170    | Cons hd tl ⇒ ? (hd :: (from_list A tl))
171    ].
172    //.
173nqed.
174
175(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
176(* Rotates and shifts.                                                        *)
177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
178   
179nlet rec rotate_left (A: Type[0]) (n: Nat)
180                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
181  match m with
182    [ Z ⇒ v
183    | S o ⇒
184        match v with
185          [ Empty ⇒ Empty A
186          | Cons p hd tl ⇒
187             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
188          ]
189    ].
190    //.
191nqed.
192
193ndefinition rotate_right ≝
194  λA: Type[0].
195  λn, m: Nat.
196  λv: Vector A n.
197    reverse A n (rotate_left A n m (reverse A n v)).
198   
199(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
200(* Lemmas.                                                                    *)
201(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
202   
203nlemma map_fusion:
204  ∀A, B, C: Type[0].
205  ∀n: Nat.
206  ∀v: Vector A n.
207  ∀f: A → B.
208  ∀g: B → C.
209    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
210  #A B C n v f g.
211  nelim v.
212  nnormalize.
213  @.
214  #N H V H2.
215  nnormalize.
216  nrewrite > H2.
217  @.
218nqed.
219
220nlemma length_correct:
221  ∀A: Type[0].
222  ∀n: Nat.
223  ∀v: Vector A n.
224    length A n v = n.
225  #A n v.
226  nelim v.
227  nnormalize.
228  @.
229  #N H V H2.
230  nnormalize.
231  nrewrite > H2.
232  @.
233nqed.
234
235nlemma map_length:
236  ∀A, B: Type[0].
237  ∀n: Nat.
238  ∀v: Vector A n.
239  ∀f: A → B.
240    length A n v = length B n (map A B n f v).
241  #A B n v f.
242  nelim v.
243  nnormalize.
244  @.
245  #N H V H2.
246  nnormalize.
247  nrewrite > H2.
248  @.
249nqed.
250
251nlemma from_list_to_list_left_inverse:
252  ∀A: Type[0].
253  ∀l: List A.
254    to_list A (length A l) (from_list A l) = l.
Note: See TracBrowser for help on using the repository browser.