source: src/ASM/BitVector.ma @ 2006

Last change on this file since 2006 was 2006, checked in by boender, 8 years ago
  • added alias for bitvector zero
  • changed extralib bounded forall/exists to use le instead of lt
File size: 6.7 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".
12include "ASM/String.ma".
13
14(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
15(* Common synonyms.                                                           *)
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17
18definition BitVector ≝ λn: nat. Vector bool n.
19definition Bit ≝ bool.
20definition Nibble ≝ BitVector 4.
21definition Byte7 ≝ BitVector 7.
22definition Byte ≝ BitVector 8.
23definition Word ≝ BitVector 16.
24definition Word11 ≝ BitVector 11.
25
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27(* Inversion                                                                  *)
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29
30lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
31 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); //
32 #n #hd #tl #abs @⊥ destruct (abs)
33qed.
34
35lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
36 ∃hd.∃tl.v ≃ VCons bool n hd tl.
37 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
38 [ #abs @⊥ destruct (abs)
39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
40qed.
41
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45
46(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47(* Creating bitvectors from scratch.                                          *)
48(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
49
50definition zero: ∀n:nat. BitVector n ≝
51  λn: nat. replicate bool n false.
52
53alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
54
55definition maximum: ∀n:nat. BitVector n ≝
56  λn: nat. replicate bool n true.
57 
58definition pad ≝
59  λm, n: nat.
60  λb: BitVector n. pad_vector ? false m n b.
61
62(* jpb: we already have bitvector_of_nat and friends in the library, maybe
63 * we should unify this in some way *) 
64let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
65  match n with
66  [ O ⇒ VEmpty ?
67  | S n' ⇒
68    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
69  ].
70 
71let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
72  match b with
73  [ VEmpty ⇒ 0
74  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
75
76(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
77(* Other manipulations.                                                       *)
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81(* Logical operations.                                                        *)
82(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
83   
84definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
85  λn: nat.
86  λb: BitVector n.
87  λc: BitVector n.
88    zip_with ? ? ? n (andb) b c.
89   
90interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
91   
92definition inclusive_disjunction_bv ≝
93  λn: nat.
94  λb: BitVector n.
95  λc: BitVector n.
96    zip_with ? ? ? n (orb) b c.
97   
98interpretation "BitVector inclusive disjunction"
99  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
100         
101definition exclusive_disjunction_bv ≝
102  λn: nat.
103  λb: BitVector n.
104  λc: BitVector n.
105    zip_with ? ? ? n xorb b c.
106   
107interpretation "BitVector exclusive disjunction"
108  'exclusive_disjunction b c = (xorb b c).
109   
110definition negation_bv ≝
111  λn: nat.
112  λb: BitVector n.
113    map bool bool n (notb) b.
114   
115interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
116
117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
118(* Rotates and shifts.                                                        *)
119(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
120 
121(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
122(* Conversions to and from lists and natural numbers.                         *)
123(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
124
125definition eq_b ≝
126  λb, c: bool.
127    if b then
128      c
129    else
130      notb c.
131
132lemma eq_b_eq:
133  ∀b, c.
134    eq_b b c = true → b = c.
135  #b #c
136  cases b
137  cases c
138  normalize //
139qed.
140
141definition eq_bv ≝
142  λn: nat.
143  λb, c: BitVector n.
144    eq_v bool n eq_b b c.
145
146lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
147  (x = y → P true) →
148  (x ≠ y → P false) →
149  P (eq_bv n x y).
150#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
151#Q * *; normalize /3/
152qed.
153
154lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
155@eq_v_true * @refl
156qed.
157
158lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
159#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
160qed.
161
162lemma eq_bv_refl:
163  ∀n,v. eq_bv n v v = true.
164  #n #v
165  elim v
166  [ //
167  | #n #hd #tl #ih
168    normalize
169    cases hd
170    [ normalize
171      @ ih
172    | normalize
173      @ ih
174    ]
175  ]
176qed.
177
178lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
179 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
180qed.
181
182lemma eq_eq_bv:
183  ∀n, v, q.
184    v = q → eq_bv n v q = true.
185  #n #v
186  elim v
187  [ #q #h <h normalize %
188  | #n #hd #tl #ih #q #h >h //
189  ]
190qed.
191
192lemma eq_bv_eq:
193  ∀n, v, q.
194    eq_bv n v q = true → v = q.
195  #n #v #q generalize in match v;
196  elim q
197  [ #v #h @BitVector_O
198  | #n #hd #tl #ih #v' #h
199    cases (BitVector_Sn ? v')
200    #hd' * #tl' #jmeq >jmeq in h;
201    #new_h
202    change with ((andb ? ?) = ?) in new_h;
203    cases(conjunction_true … new_h)
204    #eq_heads #eq_tails
205    whd in eq_heads:(??(??(%))?);
206    cases(eq_b_eq … eq_heads)
207    whd in eq_tails:(??(?????(%))?);
208    change with (eq_bv ??? = ?) in eq_tails;
209    <(ih tl') //
210  ]
211qed.
212
213corollary refl_iff_eq_bv_true:
214  ∀n: nat.
215  ∀x: BitVector n.
216  ∀y: BitVector n.
217    eq_bv n x y = true ↔ x = y.
218  #n #x #y whd in match iff; normalize nodelta
219  @conj /2/
220qed.
221
222axiom bitvector_of_string:
223  ∀n: nat.
224  ∀s: String.
225    BitVector n.
226   
227axiom string_of_bitvector:
228  ∀n: nat.
229  ∀b: BitVector n.
230    String.
Note: See TracBrowser for help on using the repository browser.