source: src/ASM/BitVector.ma @ 2700

Last change on this file since 2700 was 2645, checked in by sacerdot, 8 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 7.6 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(* jpb: we already have bitvector_of_nat and friends in the library, maybe
62 * we should unify this in some way *) 
63let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
64  match n with
65  [ O ⇒ VEmpty ?
66  | S n' ⇒
67    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
68  ].
69 
70let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
71  match b with
72  [ VEmpty ⇒ 0
73  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
74
75(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
76(* Other manipulations.                                                       *)
77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
78
79(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
80(* Logical operations.                                                        *)
81(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
82   
83definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
84  λn: nat.
85  λb: BitVector n.
86  λc: BitVector n.
87    zip_with ? ? ? n (andb) b c.
88   
89interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
90   
91definition inclusive_disjunction_bv ≝
92  λn: nat.
93  λb: BitVector n.
94  λc: BitVector n.
95    zip_with ? ? ? n (orb) b c.
96   
97interpretation "BitVector inclusive disjunction"
98  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
99         
100definition exclusive_disjunction_bv ≝
101  λn: nat.
102  λb: BitVector n.
103  λc: BitVector n.
104    zip_with ? ? ? n xorb b c.
105   
106interpretation "BitVector exclusive disjunction"
107  'exclusive_disjunction b c = (xorb b c).
108   
109definition negation_bv ≝
110  λn: nat.
111  λb: BitVector n.
112    map bool bool n (notb) b.
113   
114interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
115
116(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
117(* Rotates and shifts.                                                        *)
118(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
119 
120(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
121(* Conversions to and from lists and natural numbers.                         *)
122(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
123
124definition eq_b ≝
125  λb, c: bool.
126    if b then
127      c
128    else
129      notb c.
130
131lemma eq_b_refl:
132  ∀b.
133    eq_b b b = true.
134  #b cases b //
135qed.
136
137lemma eq_b_eq:
138  ∀b, c.
139    eq_b b c = true → b = c.
140  #b #c
141  cases b
142  cases c
143  normalize //
144qed.
145
146definition eq_bv ≝
147  λn: nat.
148  λb, c: BitVector n.
149    eq_v bool n eq_b b c.
150
151lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
152  (x = y → P true) →
153  (x ≠ y → P false) →
154  P (eq_bv n x y).
155#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
156#Q * *; normalize /3/
157qed.
158
159lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
160@eq_v_true * @refl
161qed.
162
163lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
164#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
165qed.
166
167lemma eq_bv_refl:
168  ∀n,v. eq_bv n v v = true.
169  #n #v
170  elim v
171  [ //
172  | #n #hd #tl #ih
173    normalize
174    cases hd
175    [ normalize
176      @ ih
177    | normalize
178      @ ih
179    ]
180  ]
181qed.
182
183lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
184 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
185qed.
186
187lemma eq_eq_bv:
188  ∀n, v, q.
189    v = q → eq_bv n v q = true.
190  #n #v
191  elim v
192  [ #q #h <h normalize %
193  | #n #hd #tl #ih #q #h >h //
194  ]
195qed.
196
197lemma eq_bv_eq:
198  ∀n, v, q.
199    eq_bv n v q = true → v = q.
200  #n #v #q generalize in match v;
201  elim q
202  [ #v #h @BitVector_O
203  | #n #hd #tl #ih #v' #h
204    cases (BitVector_Sn ? v')
205    #hd' * #tl' #jmeq >jmeq in h;
206    #new_h
207    change with ((andb ? ?) = ?) in new_h;
208    cases(conjunction_true … new_h)
209    #eq_heads #eq_tails
210    whd in eq_heads:(??(??(%))?);
211    cases(eq_b_eq … eq_heads)
212    whd in eq_tails:(??(?????(%))?);
213    change with (eq_bv ??? = ?) in eq_tails;
214    <(ih tl') //
215  ]
216qed.
217
218corollary refl_iff_eq_bv_true:
219  ∀n: nat.
220  ∀x: BitVector n.
221  ∀y: BitVector n.
222    eq_bv n x y = true ↔ x = y.
223  #n #x #y whd in match iff; normalize nodelta
224  @conj /2/
225qed.
226
227lemma bitvector_3_cases:
228  ∀w: BitVector 3.
229   ∃b0,b1,b2: bool.
230    w ≃ [[b0;b1;b2]].
231  #w
232 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
233 >(BitVector_O … w) %
234qed.
235
236lemma bitvector_11_cases:
237  ∀w: BitVector 11.
238    ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool.
239      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]].
240 #w
241 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
242 >(BitVector_O … w) %
243qed.
244
245lemma bitvector_3_elim_prop:
246  ∀P: BitVector 3 → Prop.
247    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
248    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
249    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
250  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
251  cases (bitvector_3_cases … H9) #l #assm cases assm
252  -assm #c #assm cases assm
253  -assm #r #assm cases assm destruct
254  cases l cases c cases r assumption
255qed.
Note: See TracBrowser for help on using the repository browser.