source: src/ASM/BitVector.ma @ 2782

Last change on this file since 2782 was 2782, checked in by sacerdot, 7 years ago
  1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the wrong indianess! removed
  2. Dominic's nat_of_bitvector/bitvector_of_nat in Arithmetic.ma are inefficient. For the time being I have pasted there Paolo's code in a comment.
File size: 7.1 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 "arithmetics/nat.ma".
9
10include "ASM/FoldStuff.ma".
11include "ASM/Vector.ma".
12
13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
14(* Common synonyms.                                                           *)
15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16
17definition BitVector ≝ λn: nat. Vector bool n.
18definition Bit ≝ bool.
19definition Nibble ≝ BitVector 4.
20definition Byte7 ≝ BitVector 7.
21definition Byte ≝ BitVector 8.
22definition Word ≝ BitVector 16.
23definition Word11 ≝ BitVector 11.
24
25(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
26(* Inversion                                                                  *)
27(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
28
29lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
30 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); //
31 #n #hd #tl #abs @⊥ destruct (abs)
32qed.
33
34lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
35 ∃hd.∃tl.v ≃ VCons bool n hd tl.
36 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
37 [ #abs @⊥ destruct (abs)
38 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
39qed.
40
41(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
42(* Lookup.                                                                    *)
43(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
44
45(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
46(* Creating bitvectors from scratch.                                          *)
47(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
48
49definition zero: ∀n:nat. BitVector n ≝
50  λn: nat. replicate bool n false.
51
52alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
53
54definition maximum: ∀n:nat. BitVector n ≝
55  λn: nat. replicate bool n true.
56 
57definition pad ≝
58  λm, n: nat.
59  λb: BitVector n. pad_vector ? false m n b.
60
61(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
62(* Other manipulations.                                                       *)
63(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
64
65(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
66(* Logical operations.                                                        *)
67(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
68   
69definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
70  λn: nat.
71  λb: BitVector n.
72  λc: BitVector n.
73    zip_with ? ? ? n (andb) b c.
74   
75interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
76   
77definition inclusive_disjunction_bv ≝
78  λn: nat.
79  λb: BitVector n.
80  λc: BitVector n.
81    zip_with ? ? ? n (orb) b c.
82   
83interpretation "BitVector inclusive disjunction"
84  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
85         
86definition exclusive_disjunction_bv ≝
87  λn: nat.
88  λb: BitVector n.
89  λc: BitVector n.
90    zip_with ? ? ? n xorb b c.
91   
92interpretation "BitVector exclusive disjunction"
93  'exclusive_disjunction b c = (xorb b c).
94   
95definition negation_bv ≝
96  λn: nat.
97  λb: BitVector n.
98    map bool bool n (notb) b.
99   
100interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
101
102(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
103(* Rotates and shifts.                                                        *)
104(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
105 
106(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
107(* Conversions to and from lists and natural numbers.                         *)
108(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
109
110definition eq_b ≝
111  λb, c: bool.
112    if b then
113      c
114    else
115      notb c.
116
117lemma eq_b_refl:
118  ∀b.
119    eq_b b b = true.
120  #b cases b //
121qed.
122
123lemma eq_b_eq:
124  ∀b, c.
125    eq_b b c = true → b = c.
126  #b #c
127  cases b
128  cases c
129  normalize //
130qed.
131
132definition eq_bv ≝
133  λn: nat.
134  λb, c: BitVector n.
135    eq_v bool n eq_b b c.
136
137lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
138  (x = y → P true) →
139  (x ≠ y → P false) →
140  P (eq_bv n x y).
141#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
142#Q * *; normalize /3/
143qed.
144
145lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
146@eq_v_true * @refl
147qed.
148
149lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
150#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
151qed.
152
153lemma eq_bv_refl:
154  ∀n,v. eq_bv n v v = true.
155  #n #v
156  elim v
157  [ //
158  | #n #hd #tl #ih
159    normalize
160    cases hd
161    [ normalize
162      @ ih
163    | normalize
164      @ ih
165    ]
166  ]
167qed.
168
169lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
170 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
171qed.
172
173lemma eq_eq_bv:
174  ∀n, v, q.
175    v = q → eq_bv n v q = true.
176  #n #v
177  elim v
178  [ #q #h <h normalize %
179  | #n #hd #tl #ih #q #h >h //
180  ]
181qed.
182
183lemma eq_bv_eq:
184  ∀n, v, q.
185    eq_bv n v q = true → v = q.
186  #n #v #q generalize in match v;
187  elim q
188  [ #v #h @BitVector_O
189  | #n #hd #tl #ih #v' #h
190    cases (BitVector_Sn ? v')
191    #hd' * #tl' #jmeq >jmeq in h;
192    #new_h
193    change with ((andb ? ?) = ?) in new_h;
194    cases(conjunction_true … new_h)
195    #eq_heads #eq_tails
196    whd in eq_heads:(??(??(%))?);
197    cases(eq_b_eq … eq_heads)
198    whd in eq_tails:(??(?????(%))?);
199    change with (eq_bv ??? = ?) in eq_tails;
200    <(ih tl') //
201  ]
202qed.
203
204corollary refl_iff_eq_bv_true:
205  ∀n: nat.
206  ∀x: BitVector n.
207  ∀y: BitVector n.
208    eq_bv n x y = true ↔ x = y.
209  #n #x #y whd in match iff; normalize nodelta
210  @conj /2/
211qed.
212
213lemma bitvector_3_cases:
214  ∀w: BitVector 3.
215   ∃b0,b1,b2: bool.
216    w ≃ [[b0;b1;b2]].
217  #w
218 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
219 >(BitVector_O … w) %
220qed.
221
222lemma bitvector_11_cases:
223  ∀w: BitVector 11.
224    ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool.
225      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]].
226 #w
227 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
228 >(BitVector_O … w) %
229qed.
230
231lemma bitvector_3_elim_prop:
232  ∀P: BitVector 3 → Prop.
233    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
234    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
235    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
236  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
237  cases (bitvector_3_cases … H9) #l #assm cases assm
238  -assm #c #assm cases assm
239  -assm #r #assm cases assm destruct
240  cases l cases c cases r assumption
241qed.
Note: See TracBrowser for help on using the repository browser.