source: Deliverables/D4.1/Matita/BitVector.ma @ 287

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

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File size: 6.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
3(*               Most functions are specialised versions of those found in    *)
4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
5(*               BitVector variants.                                          *)
6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
7
8include "Universes.ma".
9
10include "Vector.ma".
11include "List.ma".
12include "Nat.ma".
13include "Bool.ma".
14
15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* Common synonyms.                                                           *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
19ndefinition BitVector ≝ λn: Nat. Vector Bool n.
20ndefinition Bit ≝ Bool.
21ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
22ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
23ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
24ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
25ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
26
27(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
28(* Lookup.                                                                    *)
29(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
30
31ndefinition get_index ≝
32  λn: Nat.
33  λb: BitVector n.
34  λm: Nat.
35  λp: m < n.
36    get_index Bool n b m p.
37   
38interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
39   
40ndefinition set_index ≝
41  λn: Nat.
42  λb: BitVector n.
43  λm: Nat.
44  λp: m < n.
45  λc: Bool.
46    set_index_weak Bool n b m c.
47   
48ndefinition drop ≝
49  λn: Nat.
50  λb: BitVector n.
51  λm: Nat.
52    drop Bool n b m.
53
54(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
55(* Creating bitvectors from scratch.                                          *)
56(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
57
58ndefinition zero ≝
59  λn: Nat.
60    ((replicate Bool n false): BitVector n).
61   
62ndefinition max ≝
63  λn: Nat.
64    ((replicate Bool n true): BitVector n).
65   
66ndefinition append ≝
67  λm, n: Nat.
68  λb: BitVector m.
69  λc: BitVector n.
70    append Bool m n b c.
71   
72ndefinition pad ≝
73  λm, n: Nat.
74  λb: BitVector n.
75    let padding ≝ replicate Bool m false in
76      append Bool m n padding b.
77     
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79(* Other manipulations.                                                       *)
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81
82ndefinition reverse ≝
83  λn: Nat.
84  λb: BitVector n.
85    reverse Bool n b.
86
87ndefinition length ≝
88  λn: Nat.
89  λb: BitVector n.
90    length Bool n b.
91
92(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
93(* Logical operations.                                                        *)
94(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
95   
96ndefinition conjunction ≝
97  λn: Nat.
98  λb: BitVector n.
99  λc: BitVector n.
100    zip_with Bool Bool Bool n conjunction b c.
101   
102interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
103   
104ndefinition inclusive_disjunction ≝
105  λn: Nat.
106  λb: BitVector n.
107  λc: BitVector n.
108    zip_with Bool Bool Bool n inclusive_disjunction b c.
109   
110interpretation "BitVector inclusive disjunction"
111  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
112         
113ndefinition exclusive_disjunction ≝
114  λn: Nat.
115  λb: BitVector n.
116  λc: BitVector n.
117    zip_with Bool Bool Bool n exclusive_disjunction b c.
118   
119interpretation "BitVector exclusive disjunction"
120  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
121   
122ndefinition negation ≝
123  λn: Nat.
124  λb: BitVector n.
125    map Bool Bool n (negation) b.
126   
127interpretation "BitVector negation" 'negation b c = (negation ? b c).
128
129(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
130(* Rotates and shifts.                                                        *)
131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
132
133ndefinition rotate_left ≝
134  λm, n: Nat.
135  λb: BitVector n.
136    rotate_left Bool n m b.
137
138ndefinition rotate_right ≝
139  λm, n: Nat.
140  λb: BitVector n.
141    rotate_right Bool n m b.
142   
143ndefinition shift_left ≝
144  λm, n: Nat.
145  λb: BitVector n.
146  λc: Bool.
147    shift_left Bool n m b c.
148   
149ndefinition shift_right ≝
150  λm, n: Nat.
151  λb: BitVector n.
152  λc: Bool.
153    shift_right Bool n m b c.
154   
155(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
156(* Conversions to and from lists and natural numbers.                         *)
157(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
158
159ndefinition list_of_bitvector ≝
160  λn: Nat.
161  λb: BitVector n.
162    list_of_vector Bool n b.
163   
164ndefinition bitvector_of_list ≝
165  λl: List Bool.
166    vector_of_list Bool l.
167
168nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
169  let divrem ≝ divide_with_remainder n (S (S Z)) in
170  let div ≝ first Nat Nat divrem in
171  let rem ≝ second Nat Nat divrem in
172    match div with
173      [ Z ⇒
174        match rem with
175          [ Z ⇒ Empty Bool
176          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
177          ]
178      | S d ⇒
179        match rem with
180          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
181          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
182          ]
183      ].
184      //.
185nqed.
186
187naxiom plus_minus_inverse_left:
188  ∀m, n: Nat.
189    (m + n) - n = m.
190   
191naxiom plus_minus_inverse_right:
192  ∀m, n: Nat.
193    (m - n) + n = m.
194
195naxiom greater_than_b: Nat → Nat → Bool.
196
197nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
198  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
199  let size ≝ length ? biglist in
200  let bitvector ≝ bitvector_of_list biglist in
201  let difference ≝ n - size in
202    match greater_than_b size n with
203      [ true ⇒ max n
204      | false ⇒ ? (pad difference size bitvector)
205      ].
206      nnormalize.
207      nrewrite > (plus_minus_inverse_right n ?).
208      #H.
209      nassumption.
210nqed.
211
212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
213  match b with
214    [ Empty ⇒ Z
215    | Cons o hd tl ⇒
216      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
218    ].
Note: See TracBrowser for help on using the repository browser.